Injective type families for GHC

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Injective type families for GHC

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.
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [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.
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: [Haskell-cafe] Injective type families for GHC

Adam Vogt
On Tue, Feb 10, 2015 at 6:38 AM, Jan Stolarek <[hidden email]> wrote:
>> 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?

I agree it's not injective. But my impression is that injective TFs
pretty much allow ghc to replace a constraint

 TF a b ~ result

with

 (TF_getResult a b ~ result, TF_getB result a ~ b)

Where instances of:

type family TF a b | result a -> b, a b -> result -- or whatever the
notation actually is

define instances of ordinary type families TF_getB and TF_getResult.

So it's a move in the same direction to replace (HLength x ~ HLength
y) with SameLength x y. While I don't know how the code for SameLength
might be derived from the definition of HLength, that substitution
seems safe so long as (HLength x ~ HLength y) is still checked. I can
see that substitution happening in a type checker plugin, but it would
be nice if it was part of the language.

Regards,
Adam
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users