65

When I was experimenting with Haskell kinds, and trying to get the kind of ->, and this showed up:

$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude> 

Instead of the expected * -> * -> *. What are the ?? and ? things? Do they mean concrete types or "kind variables"? Or something else?

1
  • 1
    This question is now historical. Since around GHC 7.4, the kind of (->) is now just * -> * -> *, even with PolyKinds enabled. Commented Nov 23, 2014 at 21:06

1 Answer 1

95

These are GHC-specific extensions of the Haskell kind system. The Haskell 98 report specifies only a simple kind system:

... type expressions are classified into different kinds, which take one of two possible forms:

The symbol * represents the kind of all nullary type constructors. If k1 and k2 are kinds, then k1->k2 is the kind of types that take a type of kind k1 and return a type of kind k2.

GHC extends this system with a form of kind subtyping, to allow unboxed types, and to allow the function construtor to be polymorphic over kinds. The kind lattice GHC supports is:

             ?
             /\
            /  \
          ??   (#)
          / \     
         *   #     

Where:       *   [LiftedTypeKind]   means boxed type
             #   [UnliftedTypeKind] means unboxed type
            (#)  [UbxTupleKind]     means unboxed tuple
            ??   [ArgTypeKind]      is the lub of {*, #}
            ?    [OpenTypeKind]     means any type at all

Defined in ghc/compiler/types/Type.lhs

In particular:

> error :: forall a:?. String -> a
> (->)  :: ?? -> ? -> *
> (\\(x::t) -> ...)

Where in the last example t :: ?? (i.e. is not an unboxed tuple). So, to quote GHC, "there is a little subtyping at the kind level".

For interested souls, GHC also supports coercion types and kinds ("type-level terms which act as evidence for type equalities", as needed by System Fc) used in GADTs, newtypes and type families.

4
  • 9
    Exciting as this all is - are there any cases where a user (as opposed to a compiler implementer) might care about / need to explicitly take advantage of these boxed/unboxed kind distinctions? At a superficial glance they seem like a bit of an abstraction leak of some internal inference mechanism used for optimisation within the compiler?
    – Matt
    Commented Jun 14, 2010 at 14:08
  • 6
    You'll care if you try to write functions that use types of kind other than '*' -- as they have various restrictions on how you can compose. Commented Jun 14, 2010 at 16:14
  • 1
    To me this looks like an abstraction leak as well. Programming languages are about exposing the right level of abstraction to the developer. I think here this is one level down to deep.
    – J Fritsch
    Commented Dec 4, 2011 at 0:09
  • 7
    In new GHC, (?) and (??) were renamed to OpenKind and ArgKind, and now (->) :: * -> * -> *. haskell.org/pipermail/glasgow-haskell-users/2012-June/…
    – sdcvvc
    Commented Jun 9, 2012 at 13:28

Not the answer you're looking for? Browse other questions tagged or ask your own question.