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 <jan.stolarek@p.lodz.pl> wrote:
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