Hi Jan,
One example is https://github.com/haskell/vector/issues/34
I see lots of potential uses in HList. For example in HZip.hs there's
a Zip using type families:
type family HZipR (x::[*]) (y::[*]) :: [*]
type instance HZipR '[] '[] = '[]
type instance HZipR (x ': xs) (y ': ys) = (x,y) ': HZipR xs ys
If there was no need to write some additional type families that tell
ghc how to find x and y given HZipR x y, then the version using TFs
might be as good as the version using FDs (defined in HList.hs)
I don't know how realistic this is but a constraint (HLength x ~
HLength y) would ideally have the same result as SameLength x y.
Copy-paste into ghci:
:set +t -XDataKinds -XFlexibleContexts -XTypeFamilies
import Data.HList
let desired = Proxy :: SameLength x '[(),()] => Proxy x
let current = Proxy :: (HLength y ~ HLength '[(),()]) => Proxy y
Prints
desired :: Proxy '[y, y1]
current :: HLength y ~ 'HSucc ('HSucc 'HZero) => Proxy y
Regards,
Adam
On Mon, Feb 9, 2015 at 10:58 AM, Jan Stolarek
Haskellers,
I am finishing work on adding injective type families to GHC. I know that in the past many people have asked for this feature. If you have use cases for injective type families I would appreciate if you could show them to me. My implementation has some restrictions and I want to see how severe these restrictions are from a practical point of view.
Janek
--- Politechnika Łódzka
Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe