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