值（value/term）可以通过类型（type）进行分类，那么什么对类型进行分类呢？那就是 Kind！¹

      Kind
   ----------
      Type
   ----------
      Term

基础

Kind的基本文法：

k ::= *
      | k -> k

这个定义说一个kind可以是*，或者通过->和两个kind构造出一个新的kind。例子：

Int    :: *
Bool   :: *
Maybe  :: * -> *
Either :: * -> * -> *

*表示一个值的类型的kind，->就像函数类型，可以用来表示类型构造子的kind。

Kind描述了类型和类型构造子的结构，规范他们的组合：

Maybe Bool :: * -- ok
Maybe Either    -- kind mismatch

instance Functor Maybe  -- ok
instance Functor Either -- kind mismatch

Kind polymorphism

我们看一下几个Typeable：

class Typeable (t :: *) where
    typeOf :: t -> TypeRep

class Typeable1 (t :: * -> *) where
    typeOf1 :: t a -> TypeRep

class Typeable2 (t :: * -> * -> *) where
    typeOf2 :: t a b -> TypeRep

Typeable的作用是为每一个类型（kind为*）定义一个TypeRep，用做运行时的类型信息。类似的，Typeable1和Typeable2的实例可以为kind为* -> *和 * -> * -> *的类型构造子提供类型信息。typeOfN的第一个参数都是没用的，因为我们只需要类型信息，不需要值。

要定义这么多（实际上是一直到7）相似的type class的原因是没有多态的kind，每一个type class需要的kind都是固定的。如果能像参数化多态一样，有个kind参数来表示kind多态就好了，于是就有了 PolyKinds扩展。

有了多态的kind之后，Typeable就可以这样定义：

{-# LANGUAGE PolyKinds #-}           -- for Proxy, Typeable
{-# LANGUAGE ScopedTypeVariables #-} -- for typeOf, typeOf1 ...

data Proxy t = Proxy

class Typeable t where
  typeRep :: Proxy t -> TypeRep

typeOf :: forall a. Typeable a => a -> TypeRep
typeOf _ = typeRep (Proxy :: Proxy a)

typeOf1 :: forall a t. Typeable t => t a -> TypeRep
typeOf1 _ = typeRep (Proxy :: Proxy t)

开启PolyKinds之后，GHC把Proxy的kind推导为k -> *，Typeable的kind为k -> Constraint（手写也行），这里的k就像是类型参数一样，表示任意的kind。

直接这样定义是不行的：

class Typeable (t :: k) where
    typeRep :: t -> String

因为typeRep是个函数，函数参数的是值，值的类型的kind必须是*，那么t的kind就固定成*了，和手写的k是矛盾的，所以通过一个Proxy :: k -> *，我们就能让typeRep :: Proxy t -> String的参数的类型的kind为*，而t的kind是任意的。

Constraint Kinds

在上一节，Typeable的kind是k -> Constraint，Constraint是一个特殊的kind，用来表示约束。所谓约束基本上就是函数签名里写在=>前的东西，这是很好理解的：

(==) :: Eq a => a -> a -> Bool   --  约束：a必须是Eq的实例
print :: Show a => a -> IO ()    --  约束：a必须是Show的实例

Show a、Eq a这样做为一个整体，它们的kind是Constraint，而Show和Eq的kind就是* -> Constraint。

因为有了kind来表示约束，约束就表现得更像类型，可以通过原有的约束构建新的约束。在Expression Problem简介的最后，我正烦恼那个约束列表会越来越长，有了ConstraintKinds之后，我就可以为那长长约束写个type constraint synonyms：

{--
data ExprBox = forall a . (Evaluable a, PrettyPrintable a)
             => MkExpr {unBox :: a}
--}

type ExprConstraint a = (Evaluable a, PrettyPrintable a)

data ExprBox = forall a . ExprConstraint a => MkExpr {unBox :: a}

除了能简写之外，约束还能作为参数（type-level的），我们就可以把约束抽象出来：

data ExprBox c = forall a . c a => MkExpr {unBox :: a}

ExprBox c里的c的kind是* -> Constraint，我们就能为不同的ExprBox使用不同的约束。

例如可以这样用ExprBox，type class是可以部分调用（partially applied）的：

strs :: [ExprBox Show]
strs = [MkExpr "S", MkExpr (2::Int)]

nums :: [ExprBox Num]
nums = [MkExpr (1::Double), MkExpr (2::Int)]

但是还不能这样²：

type ShowNum a = (Show a, Num a)

fail :: ExprBox ShowNum
fail = undefined

因为ShowNum是个synonym，要完全展开，所以还没到类型检测就拒绝了³。一个解决方法是把ShowNum定义成type class⁴。

Datatype promotion

最后一个扩展就是DataKinds，简单来说就是把类型提升成kind，把数据构造子提升成类型构造子，配合GADT和type familiy的时候可以更精确地表达类型。

用GADT可以实现一些简单的依赖类型，例如常见的向量：

data Zero
data Succ a

data Vec :: * -> * -> * where
    Nil  :: Vec Zero a
    Cons :: a -> Vec len a -> Vec (Succ len) a

但是，Vec :: * -> * -> *和Succ :: * -> *的kind要求太宽松了，甚至可以构造出Vec (Succ Bool) a，我们想把Succ和Vec的第一个参数限制在Zero和用Succ构造的其他值，这时就可以用DataKinds。

data Nat = Zero | Succ Nat

data Vec :: Nat -> * -> * where
    Nil  :: Vec Zero a
    Cons :: a -> Vec len a -> Vec (Succ len) a

safeHead :: Vec (Succ n) a -> a
safeHead (Cons x xs) = x

这里Vec第一个参数的kind变成了Nat，也就是说原来作为类型的Nat被提升成了kind，同样的Succ和Zero都被提升到了类型构造子，kind分别是Nat -> Nat，Nat。

把列表提升到kind，然后就能实现个简单的异质列表⁵：

data List a = Nil | Cons a (List a)

data HList :: List * -> * where
  HNil  :: HList Nil
  HCons :: a -> HList t -> HList (Cons a t)

GHC.TypeLits提供了type-level的字面量，支持自然数和字符串，可以把他们当类型用。

参考

1. GHC User’s Guide 7.6.3, Chapter 7. GHC Language Features
2. Constraint Kinds for GHC
3. Kind-polymorphic Typeable
4. Adding kind Constraint