## Injective type families for Haskell

For the last few months I have been working on extending Glasgow Haskell Compiler with injective type families. At first this seemed like a fairly simple project but in the end it turned out to be much more interesting than initially thought. (I suppose that’s how research mostly turns out.) There are still some rough edges in the implementation and it will take a few more weeks before my branch gets merged into the master development branch of GHC. But for now there is a draft paper “Injective type families for Haskell” written by me, Simon Peyton Jones, and Richard Eisenberg, that we submitted for this year’s Haskell Symposium. This is not yet the final version of the paper so any feedback will be appreciated.

The idea behind injective type families is to infer the arguments of a type family from the result. For example, given a definition:

type family F a = r | r -> a where F Char = Bool F Bool = Char F a = a |

if we know `(F a ~ Bool)`

^{1} then we want to infer `(a ~ Char)`

. And if we know `(F a ~ Double)`

then we want to infer `(a ~ Double)`

. Going one step further from this, if we know `(F a ~ F b)`

then – knowing that `F`

is injective – we want to infer `(a ~ b)`

.

Notice that in order to declare `F`

as injective I used new syntax. Firstly, I used “`= r`

” to introduce a name for the result returned by the type family. Secondly, I used syntax borrowed from functional dependencies to declare injectivity. For multi-argument type families this syntax allows to declare injectivity in only some of the arguments, e.g.:

type family G a b c = r | r -> a c |

Actually, you can even have kind injectivity, assuming that type arguments have polymorphic kinds.

Obviously, to make use of injectivity declared by the user GHC needs to check that the injectivity annotation is true. And that’s the really tricky part that the paper focuses on. Here’s an example:

type family T a = r | r -> a where T [a] = a |

This type family returns the type of elements stored in a list. It certainly looks injective. Surprisingly, it is not. Say we have `(T [T Int])`

. By the only equation of `T`

this gives us `(T [T Int] ~ T Int)`

. And by injectivity we have `([T Int] ~ Int)`

. We just proved that lists and integers are equal, which is a disaster.

The above is only a short teaser. The paper covers much more: more corner cases, our algorithm for verifying user’s injectivity annotations, details of exploiting knowledge of injectivity inside the compiler and relationship of injective type families to functional dependencies. Extended version of the paper also comes with proofs of soundness and completeness of our algorithm.

`~`

means unification. Think of “`~`

” as “having a proof that two types are equal”. [↩]

Intuitively, the problem with your T family is caused by Int not being in T’s domain. So perhaps T should generate some kind of constraint that would disallow applying it to Int? I know that’s not how type families work right now, but that has always bothered me. (I haven’t read the paper yet; apologies if my question is addressed there.)

Yes, your intuition here is correct – the problem arises from the partiality of

`T`

combined with the RHS being a bare type variable. If`T`

were total it would be OK to have a bare type variable in the RHS. If the RHS was not a bare type variable then partiality of`T`

would not be a problem.I think it would be nice if T [a] = a could be accepted. Some reasons here: http://lpaste.net/4801928193189609472

Maybe a solution is that when applying T a ~ T b a ~ b, a constraint Tinv (T a) ~ a should then be solved.

It seems like you can make the inverse type families+instances mechanically: http://lpaste.net/7568722674751373312, and the compiler accepts/rejectes the same examples/counterexamples.

I can’t question the statement that “Having a single

`instance W [a] = a`

is useful”. But, as the awkard case 2 in the paper demonstrates, accepting it leads to unsoundness and that’s something we can’t allow to happen. Notice that situation with type classes (in your example) and type families (awkard case 2 in the paper) is very different. While`instance C Int`

is rejected by the compiler,`W Int`

is not! See also #9636.Yes,

`M`

is injective according to our rules. But youriffdoes not hold in a world of partial functions (notice that`W`

is partial, while`M`

is total). I believe this would hold for bijective functions.Nice work! I don’t like the surface syntax, though. The notation you borrowed from functional dependencies fits well with the relational style of MPTCs, but for the functional style of type families I think an annotation on the arguments would be better. This would also obviate the need to name the result. Why not, for instance, overload “!” (once more) to mark injective arguments like in “type family T !a !b where …”.

How would you extend that notation to express:

?

Good question. I had not considered that your plan is to support the whole set of functional dependencies. In that case you are better of with the notation you chose, I guess.

Can you give a use case for this??

Here’s a use case: https://github.com/haskell/vector/issues/34