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. 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
    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. 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
    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
    Jun 9, 2012 at 13:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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