[Haskell-cafe] Injective type families for GHC

[adam vogt]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe