[Haskell-cafe] DataKinds + KindSignatures question

[Roman Cheplyaka]

On 27/11/14 12:04, Wojtek Narczyński wrote:
> I must stop thinking of '*' as some of wildcard. 

Totally.

> Oh, so Proxy can be understood as a type level function from 'CmdKind'
> to '*'?

Sure. In fact, any type constructor can be seen as a (possibly nullary)
type function:

Prelude> :k Maybe
Maybe :: * -> *

Maybe is a type function from types (*) to types (*).

Prelude Control.Monad.State> :k StateT
StateT :: * -> (* -> *) -> * -> *

StateT (not to be confused with StateT on the value level that has type
(s -> m (a, s)) -> StateT s m a) is a type function of three arguments,
two of them of kind * and one of kind (* -> *).

Now let's look at Proxy:

Prelude Data.Proxy> :k Proxy
Proxy :: k -> *

Proxy is declared as a kind-polymorphic type (see PolyKinds). Here k is
actually a "wildcard" (a kind variable that can be instantiated with any
kind). Thus, you can specialize Proxy to be of kind * -> *, or (* -> *)
-> *, or MyKind -> *. However, since the type Proxy k has a value (also
called Proxy), the return kind of the Proxy type function is necessarily *.

You can't build a type function returning a non-* kind using a data or
newtype declaration. You can do it, however, using type families.

Roman
Roman