以前忘了总结了。。正好在这里总结一下 Type, Type Constructor 与 Kind 这几个概念，结合Haskell和Scala。

TODO(2016.12): GHC 8.0的kind system(TypeInType); Dependent Type; Lambda Cube

Type, Type Constructor 与 Kind (Haskell)

Types and Programming Languages 里的一张图非常直观地表现了Kind与Type的意义：

其中，上图的Term就是值(Value)的意思，比如1、"haha"之类的，都是Term。

而Type，则是 Value的类型，比如1的Type是Num(Haskell)，"haha"的Type是String。然后我们引入Type Constructor的概念，它接受一个或多个类型参数(type parameter)并构造出一个新Type，比如Maybe是一个Unary Type Constructor，它接受一个类型参数，可以构造出Maybe Int和Maybe String等等的不同的Type。再比如Either的定义为data Either a b = Left a | Right b，它接受两个类型参数，可以构造出像Either Bool和Either Int Bool这样的Type Constructor。其实，我们也可以把这些Primitive Type看作是一种特殊的Type Constructor，即接受零个类型参数(Nullary Type Constructor)。

有了Type和Type Constructor的概念以后，我们就可以定义Kind了。Kind表示 Type Constructor的类型 ，在Haskell中有以下定义：

• Nullary Type Constructor（即普通的Type）的kind为*
• 如果k1和k2是kind，那么k1 -> k2代表一个Type constructor的kind，这个Constructor接受kind为k1的类型参数，返回kind为k2的类型参数。
  比如Either String的kind为* -> *

这样，从Value到Type、Type Constructor，再到Kind，每上一个层次都是一个抽象。Type Constructor是Value的类型，Kind又是Type Constructor的类型。

Kind Polymorphism (Haskell)

默认情况下，Haskell不允许kind具有多态性(Kind polymorphism)。比如我们的Either的定义如下:

1

data Either a b = Left a | Right b 	-- Defined in ‘Data.Either’

a和b的kind是任意的，可以是*，也可以是* -> *。Haskell默认将它们的kind都推导为*，因此下面的定义是不允许的：

1
2
3
4
5
6
7
8

Prelude> data T1 = Either []
<interactive>:123:18:
    Expecting one more argument to ‘[]’
    Expected a type, but ‘[]’ has kind ‘* -> *’
    In the type ‘[]’
    In the definition of data constructor ‘Either’
    In the data declaration for ‘T1’

当然有些时候Haskell也是可以推导出来某些Higher-order kind的，比如：

1

data A t k p = A { s1 :: p, s2 :: t k }

由于s2 :: t k，而k默认被推导为*，因此t的kind就会被推导为* -> *，那么A的kind最终被推导为(* -> *) -> * -> * -> *。

如果要使Haskell支持 polymorphic kinds ，可以利用GHC的扩展-XPolyKinds，就不再展开总结了，详情可以参考这里。

Data Kinds/Datatype promotion (Haskell)

Datatype promotion是GHC的一个扩展(-XDataKinds)，可以将部分的Datatype给自动promote成kind。比如：

1
2
3
4
5
6
7
8

Prelude> :k Left
Left :: k -> Either k k1
Prelude> :k 3
3 :: GHC.TypeLits.Nat
Prelude> :k ""
"" :: GHC.TypeLits.Symbol
Prelude> :k Just
Just :: k -> Maybe k

具体的应用还没实践过，等实践过再来总结。。

Scala中的Type和Kind

Scala中的Type和Kind用一张图总结：

我觉得Scala中的Kind比较混乱，至少每次试的时候出的结果总与想象的不对应，或许还没有理解吧。。。举几个例子：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

scala> class Functor[M[_]]
defined class Functor
scala> :k -v Functor
<console>:11: error: not found: value Functor
       Functor
       ^
scala> :k -v new Functor
Functor's kind is X[F[A]]
(* -> *) -> *
This is a type constructor that takes type constructor(s): a higher-kinded type.
scala> :k -v List
scala.collection.immutable.List's kind is F[+A]
* -(+)-> *
This is a type constructor: a 1st-order-kinded type.
scala> :k -v List[Int]
scala.collection.immutable.List's kind is F[+A]
* -(+)-> *
This is a type constructor: a 1st-order-kinded type.
scala> :k -v List(1, 2)
scala.collection.immutable.List's kind is A
*
This is a proper type.
scala> :k -v Either
scala.util.Either's kind is F[+A1,+A2]
* -(+)-> * -(+)-> *
This is a type constructor: a 1st-order-kinded type.
scala> :k -v (Int, String) => Option[_]
scala.Function2's kind is F[-A1,-A2,+A3]
* -(-)-> * -(-)-> * -(+)-> *
This is a type constructor: a 1st-order-kinded type.

感觉Scala REPL中的:kind是针对value的而不是type的，非常蛋疼，估计是让JVM的泛型类型擦除搞得Parametric Polymorphism都不爽了。。另外Scala中也分 1st-order-kinded type 和 higher-kinded type 。所谓higher-kinded type就是类似于A[B[_]]这样的type constructor，比如下面的这个例子：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

scala> class T3[Q[A], P[B]]
defined class T3
scala> :k -v new T3
T3's kind is X[F1[A1],F2[A2]]
(* -> *) -> (* -> *) -> *
This is a type constructor that takes type constructor(s): a higher-kinded type.
scala> class T4[Tuple2[A, B], P[Option[C]], D, E]
defined class T4
scala> :k -v new T4
T4's kind is Y[F1[A1,A2],X[F2[A3]],A4,A5]
(* -> * -> *) -> ((* -> *) -> *) -> * -> * -> *
This is a type constructor that takes type constructor(s): a higher-kinded type.

参考资料

• Types and Programming Languages
• Generics of a Higher Kind, Martin Odersky
• Kind - HaskellWiki
• What is a higher kinded type in Scala?