Jim Apple <[EMAIL PROTECTED]> wrote in article <[EMAIL PROTECTED]> in gmane.comp.lang.haskell.cafe: > > (forall (f :: * -> *) . f) Int. > > What values inhabit this type? > The same ones that inhabit (forall (f :: * -> *) . f Int); that is, > none (or _|_). I don't see the uninhabitability of a type as reason > why the type itself should be ill-formed, even in a domain without > lifted types.
I'm sorry I wasn't clear; I did not mean to argue that a type should be ill-formed just because it is not inhabited. Let me try to say something else. The kind system should be to types as the type system is to terms; in particular, if a type is well-kinded (i.e., well-formed) then it should either be a "value type" (such as "[Int]" and "forall a. a") or contain a redex (such as "(\a -> a) Int"). The proposed type above is neither; it is stuck just as the program "1 + \x->x" is stuck. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
