Question regarding the GHC users manual
Hi all, Just wondering if there could be a typo in section 7.7.2.1 of the GHC manual (type family declarations) http://www.haskell.org/ghc/docs/latest/html/users_guide/type-families.html Specifically, it says type family F a b :: * -> * -- F's arity is 2, -- although its overall kind is * -> * -> * -> * along with F Char [Int] -- OK! Kind: * -> * F Char [Int] Bool -- OK! Kind: * F IO Bool -- WRONG: kind mismatch in the first argument F Bool -- WRONG: unsaturated application and I'm wondering about the overall kind. Shouldn't that be * -> * -> *, or am I not understanding something? Thanks! -Tyson
Hi Tyson, I don't think this is a bug.
type family F a b :: * -> * -- F's arity is 2, -- although its overall kind is * -> * -> * -> *
F Char [Int] -- OK! Kind: * -> *
Char :: * [Int] :: * So we can "fill" in the first two * in the kind * -> * -> * -> * to get * -> *, as reported.
F Char [Int] Bool -- OK! Kind: *
Char :: * [Int] :: * Bool :: * As before, except that we can now fill in another * to get *.
F IO Bool -- WRONG: kind mismatch in the first argument
IO :: * -> * Bool :: * Uh-oh! F has kind: * -> (* -> (* -> *)) And we are trying to do the application: F IO But IO :: * -> * /= * (the kind on the left of the arrow)! So we get a kind error.
F Bool -- WRONG: unsaturated application
This is disallowed by the rules of type families. If unsaturated applications were allowed it would be well-kinded though, since Bool :: *.
and I'm wondering about the overall kind. Shouldn't that be * -> * -> *, or am I not understanding something?
I'm not sure what you think has gone wrong. * -> * -> * is the kind of something with two type arguments, but F clearly has 3 (two indexed ones, one parametric one). The inference rule you need to think of is something like: t1 :: k1 -> k2 t2 :: k1 -------------- t1 t2 :: k2 With axioms like (glossing over issues of saturation): ------------ Bool :: * --------------- IO :: * -> * -------------------------- F :: * -> * -> * -> * GHC's kind system is actually even more complicated than this due to subkinding, but you usually don't have to worry about that. Cheers, Max
type family F a b :: * -> * -- F's arity is 2, -- although its overall kind is * -> * -> * -> *
I believe what you're missing is that with the definition F a b :: * -> *, F needs three arguments (of kind *) in order to become kind *. If F a b :: * -> * as stated, then F a :: * -> * -> * and F :: * -> * -> * -> *, just like reported. Cheers, /Niklas
Hi Max and Niklas, Thank you both for your answers. I get it now. I didn't read carefully enough to note that the explicit type on F a b was the type of F and the type of F (although, in retrospect, this last interpretation wouldn't have worked as we would have need at least * -> * -> *). Thanks again. Cheers! -Tyson
participants (3)
-
Max Bolingbroke -
Niklas Broberg -
Tyson Whitehead