[Haskell-cafe] Injective type families for GHC

[Jan Stolarek]

Thank you Adam.

> One example is https://github.com/haskell/vector/issues/34
Yes, this looks like an example where injectivity will work. One question here: how does one build 
vector with GHC HEAD? I tried but failed because of dependencies.

> 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
Bad news: my current implementation won't allow to declare HZipR as injective. That's because my 
implementation is conservative and does not permit calling type families by injective type 
family.

> 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.
I'm not sure if I understand that part. HLength is not injective. How would injectivity help here?

Janek

---
Politechnika Łódzka
Lodz University of Technology

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.

This email contains information intended solely for the use of the individual to whom it is addressed.
If you are not the intended recipient or if you have received this message in error,
please notify the sender and delete it from your system.