On Sat, Feb 06, 2016 at 12:12:47PM -0500, Edward Kmett wrote:
The primitives that GHC uses to implement arrays, references and the like live in #. We then wrap them in something in * before exposing them to the user, but you can shave a level of indirection by knowing what lives in # and what doesn't.
But even if you never care about #, Int, Double, etc. are of kind *, Functors are of kind * -> *, etc. so to talk about the type of types at all you need to be able to talk about these concepts at all with any rigor, and to understand why Maybe Maybe isn't a thing.
(This question is for my own edification and is not meant to be a point in the current debate) If we were inventing a language from the beginning, would it be strictly necessary to have two kinds? Could we have just an unboxed kind #, and have a box be an explicit type constructor? If the type constructor were called 'P' (standing for pointer) then we could have id :: P a -> P a data [a] = (P a) : [a] | [] etc. Does this thing seem remotely plausible to people who know clever type theory? Tom