On Feb 13, 2014, at 4:28 AM, José Pedro Magalhães <j...@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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
