Notes (TLPH 02/15): Terms, Types and Kinds
2.1 The Kind System
A kind is a type of types. Compile-time is runtime for the compiler, and values the compiler runs computation on are types.
2.1.1 The Kind of “Types”
Roughly, a “type” are type-level terms, a subset of which are “value types”, which can be inhabited by runtime values and correspond to the Haskell kind * or Type. For example Maybe is a type, but not a Type, because it has kind Type -> Type.
2.1.2 Arrow Kinds
Higher-kinded types are type constructors. Maybe is an HKT, because its kind is Type -> Type.
2.1.3 Constraint Kinds
Exercise 2.1.3 (i)
Show has kind Type -> Constraint
Exercise 2.1.3 (ii)
Functor has kind (Type -> Type) -> Constraint, since it operates on unary type constructors (like [], Maybe etc.).
Exercise 2.1.3 (iii)
Monad has kind (Type -> Type) -> Constraint
Exercise 2.1.3 (iv)
The definition of MonadTrans is:
class MonadTrans t where
lift :: Monad m => m a -> t m aFrom the class declaration, which must be a Constraint, we can see that MonadTrans has kind T -> Constraint, where T is the kind of the t type variable.
We can expand the kind of T by noticing that in the type signature for lift, t is a type constructor that takes two arguments m and a, therefore it’s kind must be M -> A -> Type, where M is the kind of m and A is the kind of A. Only Type kinds can appear in type signatures.
In the constraint on lift, the type variable m is an argument to Monad, which has kind (Type -> Type) -> Constraint.
Therefore kind M is Type -> Type, and since m a has kind Type, the kind of a is Type.
Therefore the kind of t is (Type -> Type) -> Type -> Type, and the kind of MonadTrans is
(Type -> Type) -> Type -> Type -> Constraint2.2 Data Kinds
-XDataKinds allows lifting of data constructors into type constructors.
Seems like there are some bugs with the UserType example given in the text if naively copied into a source file, but perhaps that wasn’t the author’s intent. Regardless, was a simple fix:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data UserType = UserK | AdminK
data Proxy (a :: UserType) = Proxy
data User = User { userAdminToken :: Maybe (Proxy 'AdminK) }
doSensitiveThings :: Proxy 'AdminK -> IO ()
doSensitiveThings = undefinedWhich kind-errors on doSensitveThings (a :: Proxy 'UserK)
2.4 Type-Level Functions
For exercise solutions, see 02/TypeLevelFunctions.hs