Functional dependencies can "return" kinds, type families cannot

[Richard Eisenberg]

On Feb 13, 2014, at 4:28 AM, José Pedro Magalhães <jpm at cs.uu.nl> wrote:

> 
> The most interesting part here is the functional dependency fs -> k, where k is a kind variable!
> If this is not a bug (and it does seem to work as I expect it to), then could we have type families
> return kinds too?...

Yes, I ran into this a while ago. A function dependency on a kind seems to work remarkably well.

Can we have type families that return kinds? No. Well, not yet. Functional dependencies inform type inference but don't produce any evidence in Core -- a dependency is only ever used to eliminate ambiguity. On the other hand, a type family does produce evidence (in the form of a type coercion) in Core, and kind coercions turn out to be challenging. How challenging? See "System FC with Explicit Kind Equality", ICFP '13 (http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf)

How does this difference between fundeps and type families manifest itself? Type families work much better with GADTs. I don't have an example to hand, but if you're doing GADT programming, using fundeps won't get you very far. That's because the GADTs use the Core coercions internally... and the fundeps don't produce them.

Nevertheless, having done the theory behind a Core language with explicit kind coercions, I'm now in the midst of implementing (on a branch -- don't expect anything soon!) type inference for that Core language. In effect, it would be the resolution of GHC bug #7961 (https://ghc.haskell.org/trac/ghc/ticket/7961), but with fairly far-reaching consequences in the implementation. So, if all goes well, we'll have type families returning kinds at some point in the not-too-distant future.

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140213/c2ffbccb/attachment.html>