Haskell 的 Kind 系统入门

Haskell 的 Kind 系统入门

本文是对这篇文章的翻译,文章通过与 type 的对比帮助读者入门 kind 理论。

文中所有的代码基于 GHC 8.4.3

Types 和 Kinds

简单来说

正如表达式 (values/terms) 都有类型 (types),types 也有自己对应的 kinds。

例如 "hello""world" 都属于 String 类型,TrueFalse 都属于 Bool 类型。相似地,String 类型和 Bool 类型都属于 *(读作 "star")kind。 State type

GHCi 中可以使用 :t:type 来查看某个表达式的类型,用 :k:kind 可以查看某个类型对应的 kind。

1
2
3
4
5
λ> :t True
True :: Bool

λ> :k Bool
Bool :: *

在标准的 Haskell 中所有的原始 (inhabited) 类型 (即至少有一个取值的类型) 都属于 * 的 kind。因此 IntInt -> String[Int]Maybe IntEither Int Int 这些至少拥有一个取值的类型都属于 * 的 kind。

一个明显无法构造的例外是 data Void,这种类型没有取值,其只能由无法成功完成的语句来产生,例如 undefined 或无限循环 f x = f x

不是所有的类型都是原始类型,例如 MaybeEither 就不属于,对于 Maybe 来说,没有任何值可以取,即没有任何表达式 (或值) 属于 Maybe 类型,不同于 Just True 属于 Maybe Bool 类型,Just 'C' 属于 Maybe Char 类型,我们无法构造一个属于 Maybe 的表达式。

1
2
3
4
5
6
7
λ> x = undefined :: Maybe
<interactive>:9:18: error
Expecting one more argument to ‘Maybe

λ> f x = f x :: Maybe
<interactive>:10:14: error:
Expecting one more argument to ‘Maybe

那么 MaybeEither 属于什么呢?它们实际是类型构造器 (type constructor)。

Data constructors 和 Type constructors

正如可以利用数据构造器 (data constructor) 来构造一个 data,我们也可以利用类型构造器 (type constructor) 来创建 types。

1
2
3
4
λ> data Person = MkPerson { name :: String, age :: Int }

λ> :t MkPerson
MkPerson :: String -> Int -> Person

如上面的代码所示,MkPerson 是一个数据构造器,通过接受类型为 Stringname 和类型为 Intage 来构造一个 Person 类型的值,换句话说,MkPerson 具有 String -> Int -> Person 的类型。

1
2
3
4
λ> data Either a b = Left a | Right b

λ> :k Either
Either :: * -> * -> *

相似地,Either 是一个接受两个 kind 为 * 的类型来构造一个新的类型为 * 的类型构造器,即 Either 是一个具有 * -> * -> * 的 kind 的类型。

这里要注意,Either 接受类型 a 和类型 b 来构造一个新的类型,Left 接受一个具有 a 类型的值来构造一个新的值。

数据构造器可以科里化 (currying),类型构造器同样也可以。

1
2
3
4
5
6
λ> :t MkPerson
MkPerson :: String -> Int -> Person
λ> :t MkPerson "Diogo"
MkPerson "Diogo" :: Int -> Person
λ> :t MkPerson "Diogo" 29
MkPerson "Diogo" 29 :: Person

1
2
3
4
5
6
λ> :k Either
Either :: * -> * -> *
λ> :k Either String
Either String :: * -> *
λ> :k Either String Int
Either String Int :: *

Type signatures 和 Kind signatures

GHC 不仅可以正确推断出一个表达式的类型,也可以推断出一个类型对应的 kind。

1
2
3
4
5
-- `x` 被推断为`Bool` 类型
x = True

-- `y` 被推断为 `String -> IO ()` 类型
y = putStrLn
1
2
3
4
5
6
7
-- `a` 被推断为 `*` kind
data List a = Cons a (List a) | Nil

-- `f` 被推断为 `* -> *` kind
-- `a` 和 `b` 被推断为 `*` kind
class Functor f where
fmap :: (a -> b) -> (f a -> f b)

正如我们可以手动标明某个值的类型,我们也可以开启 KindSignatures 扩展来手动标明某个类型的 kind。

1
2
3
4
5
x :: Bool
x = True

y :: String -> IO ()
y = putStrLn
1
2
3
4
5
6
7
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExplicitForAll #-}

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

class Functor (f :: * -> *) where
fmap :: forall (a :: *) (b :: *). (a -> b) -> (f a -> f b)

这里启用了 ExplicitForAll 扩展来显示地标明每个类型的 kind。

HOFs 和 HKTs

正如我们拥有高阶函数 (higher-order functions, HOFs) 这种可以接受其他函数作为参数的函数,我们也可以拥有高阶类型 (higher-kinded types, HKTs) 这种接受其他类型构造器作为参数的类型构造器。

1
2
λ> :t map
map :: (a -> b) -> [a] -> [b]

这里 map 是接受两个参数的函数,这两个参数分别是一个 a -> b 类型的函数和一个 a 类型的 list。

1
2
3
4
λ> data NonEmpty f a = MkNonEmpty { head :: a, tail :: f a }

λ> :k NonEmpty
NonEmpty :: (* -> *) -> * -> *

相似地,NonEmpty 是接受两个参数的类型构造器,这两个参数分别是一个具有 * -> * 的 kind 的类型构造器和一个具有 * 的 kind 的类型。

当给 NonEmpty 应用 []Bool 两个类型时,可以得到 NonEmpty [] Bool 类型,即一个保证至少有一个元素存在的 Bool 类型的 list。

1
2
λ> :t MkNonEmpty True [False, True]
MkNonEmpty True [False, True] :: NonEmpty [] Bool

我们可以将任何满足 kind 约束的类型应用在 NonEmpty 上构造我们需要的类型,例如:NonEmpty [] IntNonEmpty Tree StringNonEmpty Vector Char

kind 的其他内容

Unboxed/unlifted types

在文章的开头说过所有的原始类型都具有 kind *,更标准的表达应该是:在标准 Haskell 中,* 是所有装箱的 (boxed) [或升格 (lifted)] 的原始类型的 kind。然而,在 GHC 对 Haskell 的实现中,有一些原始类型是未装箱 (unboxed) [或未升格 (unlifted)] 的。它们是 ghc-prim 包 (package) 中的 GHC.Prim 模块 (module)。为了方便起见,所有的未升格的类型都用 # 结尾,它们被称为 magic hash,需要开启 MagicHash 扩展。例如 Char#Int#,甚至可以拥有未装箱的 tuple (# a, b #) 和未装箱的 (# a | b #)

每一个未升格的类型都拥有一个描述其运行时状态的 kind。这个状态标明该类型是否是一个指向某个堆的指针、是否是一个有符号的 word-size 值。编译器随后会利用类型的 kind 信息来确定生成对应的机器码,这一过程叫做类型指向的编译 (kind-directed compilation)。

下图是一个具体的例子: Unboxed types and kinds

后面会对 TYPE 做介绍。

Constraint

Constraint kind 是用来描述所有需要受到约束的类型的 kind,它通常出现在 \(\Rightarrow\) 的左边,包括 typeclass 的限制、多个 typeclass tuple 组成的限制等。

1
2
3
4
5
λ> :t show
show :: Show a => a -> String

λ> :t fmap
fmap :: Functor f => (a -> b) -> f a -> f b

如上所示,show 函数接受的 a 类型的参数需要是 Show 类型的实例,即 Show 一个具有 Constraint kind 的类型,fmap 同理。

1
2
3
4
5
6
7
8
9
10
11
λ> :k Show
Show :: * -> Constraint

λ> :k Show Int
Show Int :: Constraint

λ> :k Functor
Functor :: (* -> *) -> Constraint

λ> :k Functor IO
Functor IO :: Constraint

利用 ConstraintKinds 扩展可以将约束作为一等公民使用达到令人惊奇的效果。例如 Set 不是 Functor 的实例,原因是 Set.map 拥有 Ord 的约束,而 fmap :: (a -> b) -> f a -> f b 并不满足。

1
2
λ> :t Data.Set.map
Data.Set.map :: Ord b => (a -> b) -> Set a -> Set b

可以看到 Set.map 需要 bOrd 的实例。

通过 ConstraintKinds 我们可以实现一个既可以拥有约束也可以没有约束的 Functor typeclass。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}

import Data.Kind (Constraint)
import qualified Data.Set as Set
import qualified Data.List as List

class GFunctor (c :: * -> Constraint) (f :: * -> *) | f -> c where
gfmap :: c b => (a -> b) -> (f a -> f b)

instance GFunctor Ord Set.Set where
gfmap = Set.map

instance GFunctor EmptyConstraint [] where
gfmap = List.map

其中 EmptyConstraint 是一个满足所有类型的约束。

1
2
3
4
{-# LANGUAGE FlexibleInstances #-}

class EmptyConstraint a
instance EmptyConstraint a

Datatype promotion

在标准 Haskell 中,可以利用 data 关键字定义由一个或多个数据构造器定义的类型或类型构造器。

1
data ConnectionStatus = Open | Closed

ConnectionStatus type 当开启 GHC 的 DataKinds 扩展后,data 关键字会在原有的基础上增加一个自定义的 kind 和满足该 kind 的类型或类型构造器。

1
2
3
{-# LANGUAGE DataKinds #-}

data ConnectionStatus = Open | Closed

上述代码会创建一个新的 ConnectionStatus kind,该 kind 拥有两个非原始的类型,分别是 'Open'CloseConnectionStatus kind

此时,我们说 ConnectionStatus 已经被提升 (promoted) 为了拥有 OpenClose 两个类型的 kind,注意到这里 OpenClose 都省略了 '前缀,该前缀在大多数情况下可以省略,只有在极少数情况下需要写明以避免歧义。

通过利用新生成的 kind,我们可以定义接受被实例化为 OpenClosed 的类型变量。

1
2
3
4
5
6
7
8
{-# LANGUAGE KindSignatures #-}

data Connection (s :: ConnectionStatus) = MkConnection ...

newConnection :: Address -> Connection Closed
openConnection :: Connection Closed -> Connection Open
closeConnection :: Connection Open -> Connection Closed
connectionAddress :: Connection s -> Address
1
2
3
λ> :k Connection Int
<interactive>:1:12: error:
Expected kind ‘ConnectionStatus’, but ‘Int’ has kind ‘*’

通过连接状态,我们可以在编译期实现例如 closeConnection 只能在开启的连接中被调用,而不能在关闭的连接中被调用的限制。

这种功能并不仅限于我们自定义的 data,例如在开启 DataKinds 扩展后,Bool 类型也可以被提升为 kind。

1
2
3
4
5
6
7
8
9
10
11
λ> data F (b :: Bool) = MkF deriving Show

λ> MkF :: F 'True
MkF

λ> MkF :: F 'False
MkF

λ> MkF :: F 'Open
<interactive>:30:10: error:
Expected kind ‘Bool’, but ‘ 'Open’ has kind ‘ConnectionStatus

GHC.TypeLits

GHC 还提供了两个方便的未装箱的 kind, 它们被定义在 base 中的 GCH.TypeLits 模块下。

第一个是 SymbolSymbol 是类型层面 (type-level) 的字符串表示的 kind。例如我们可以将 "hello" 字符串作为一种类型使用,这时 "Hello" 就拥有 Symbol 的 kind。 Symbol kind

这样我们就可以用字符串字面量来表示一种类型了。

1
2
3
4
5
6
7
8
9
10
11
12
{-# LANGUAGE KindSignatures, DataKinds #-}

import GHC.TypeLits (Symbol)
import Data.Ratio ((%))

newtype Money (currency :: Symbol) = Money Rational

fivePence :: Money "GBP"
fivePence = Money (5 % 100)

twoEuros :: Money "EUR"
twoEuros = Money 2

将货币在类型层面表示,而不是在表达式层面 (term-level) 上表示 (例如 data Money = Money String Rational) 可以静态地有效避免将不同货币弄混,犯下例如将英镑和欧元直接相加这样的错误。

1
2
add :: Money c -> Money c -> Money c
add (Money x) (Money y) = Money (x + y)
1
2
3
4
5
6
λ> add fivePence fivePence
Money (1 % 10)

λ> add fivePence twoEuros
<interactive>:8:15: error:
Couldn't match type ‘"EUR"’ with ‘"GBP"’

如果只在表达式层面进行定义,那么在相加货币时必须对货币的类型进行运行时检查,相关的函数也要添加类似 MaybeEitherMonadError e m 这种表示失败的返回结果。

一个有趣的事实:上面的例子不是仅仅只为演示而虚构的,这是真实存在的 safe-money 库的表示方式

此外,如果我们不需要对金钱进行数学运算的话,将货币值用 Rational 保存显得过于浪费了一点。因此 safe-money 库还提供了另一种对 Integer 简单包装的 Discrete 类型来满足不需要进行运算的场景。要注意的是,根据 safe-money 库官方的解释,用 Integer 表示货币值时仅仅保存货币值本身还不够,还应该记录货币的单位间的换算关系。例如表示美元时,这种关系就是 1 比 1,而表示美分时,这种关系就变成了 100 比 1 (100 美分换 1 美元)。

为了在类型层面表示这种换算关系,需要用到在 GHC.TypeLits 里定义的另一个在类型层面表示自然数的 kind Nat。它的用法和 Symbol 相似,只需要将字符串字面量换成数字就可以了。

1
2
3
4
5
6
7
8
9
10
11
12
{-# LANGUAGE KindSignatures, DataKinds #-}

import GHC.TypeLits (Symbol, Nat)

newtype Discrete (currency :: Symbol) (scale :: (Nat, Nat))
= Discrete Integer

oneDollar :: Discrete "USD" '(1, 1)
oneDollar = Discrete 1

oneDollarThirtyCents :: Discrete "USD" '(100, 1)
oneDollarThirtyCents = Discrete 130

其中 scale :: (Nat, Nat) 中的 tuple (,) 是通过 DataKinds 提升为 kind 的,同时 '(,) 这一类型构造器也是由原始的数据构造器提升来的。

Kind polymorphism

参数多态性 (parametric polymorphism) 广泛存在于 Haskell 中,它可以帮助我们对类型进行抽象。通过开启 PolyKinds 扩展可以达到对 kind 更高程度的抽象。

让我们来看一个例子:

1
data Proxy a = MkProxy

这里 Proxy 是接受一个类型变量的类型构造器,它拥有一个不带参数的数据构造器。在我们手边没有任何数据时,使用 Proxy 传递类型十分方便。

Proxy 已经被定义在 base 中的 Data.Proxy 模块中,本文中的实现是为了演示 kind 的逻辑,要更深入地了解 Data.Proxy 及其使用的例子,可以阅读 Kwang Seo 的这篇博客。

1
2
3
λ> intRepresentative = MkProxy :: Proxy Int

λ> stringRepresentative = MkProxy :: Proxy String

有一个问题是默认情况下,GHC 会假设 a 具有 * 的 kind,这意味着 Proxy 仅适用于具有 * 的 kind 的类型,无法适用于所有的类型。

1
2
3
4
5
6
7
λ> :k Proxy
Proxy :: * -> *

λ> maybeRepresentative = MkProxy :: Proxy Maybe
<interactive>:9:38: error:
Expecting one more argument to ‘Maybe
Expected a type, but ‘Maybe’ has kind ‘* -> *’

正常情况下,我们需要应该为所有可能的 kind 创建下面这样属于其的 Proxy 类型。

1
2
3
4
5
6
7
8
9
data Proxy a = MkProxy
data Proxy1 (a :: * -> *) = MkProxy1
data Proxy2 (a :: * -> * -> *) = MkProxy2
data HKProxy1 (a :: (* -> *) -> * -> *) = MkHKProxy1

stringRepresentative = MkProxy :: Proxy String
maybeRepresentative = MkProxy1 :: Proxy1 Maybe
eitherRepresentative = MkProxy2 :: Proxy2 Either
nonEmptyRepresentative = MkHKProxy1 :: HKProxy1 NonEmpty

很明显上面这种写法不具有扩展性,但是在开启 PolyKinds 扩展后我们可以创建适用于所有具有 k 的 kind 类型 的 Proxy

1
2
3
4
5
6
7
8
9
10
11
12
13
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

data Proxy (a :: k) = MkProxy

-- Now `a` can be anything at all
maybeRepresentative = MkProxy :: Proxy Maybe
nonEmptyRepresentative = MkProxy :: Proxy NonEmpty
functionRepresentative = MkProxy :: Proxy (->)
helloRepresentative = MkProxy :: Proxy "hello"
showRepresentative = MkProxy :: Proxy Show
functorRepresentative = MkProxy :: Proxy Functor
openRepresentative = MkProxy :: Proxy 'Open

事实上,我们可以省略 a :: k 由 GHC 自动推断。

1
2
3
4
5
λ> :set -XPolyKinds
λ> data Proxy a = MkProxy

λ> :k Proxy
Proxy :: k -> *

Servant 是另一个使用 kind polymorphism 的例子,Servant 用于编写类型安全的 web APIs。其中有一个名为 :> 的类型用于将一个 API 的各个组件 (component) 组合成一个拥有完整类型信息的用例。这些组件可能拥有不同的类型和不同的 kind。

1
2
3
4
5
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}

data (:>) (a :: k) (b :: *)
infixr 4 :>

通过这样可以描述请求的响应,例如 POST /books,通过使用 :>"books" :: SymbolReqBody '[JSON] Book :: *Post '[JSON] () :: * 结合在一起。

1
type BooksAPI = "books" :> ReqBody '[JSON] Book :> Post '[JSON] ()

Levity polymorphism

在一些情况下,我们可能需要对升格的类型和未升格的类型做统一的抽象。例如 error 函数接受一个错误信息并抛出异常:

1
2
3
{-# LANGUAGE ExplicitForAll #-}

error :: forall a. String -> a

由于 error 的返回值具有多态性,它可以应用于大多数的场景:

1
2
increment :: Int -> Int
increment x = error "oops"

但是因为 a 会被默认推断为具有 * 的 kind,因此我们无法将其应用于未升格的类型:

1
2
incrementUnlifted :: Int# -> Int#
incrementUnlifted x = error "oops"
1
2
<interactive>:22-40: error
Couldn't match a lifted type with an unlifted type

在现有的知识下,我们可能会想到开启 PolyKinds 并引入 kind 变量 k 来实现上面的目的,但是这并不能成功:

1
error :: forall k (a :: k). String -> a
1
2
3
/Playground.hs:15:40: error:
Expected a type, but ‘a’ has kind ‘k’
In the type signature: error :: forall k (a :: k). String -> a

原因是 a :: k 对原始类型以外的其他类型没有意义。例如 kSymbola"hello",当 "hello" 不是原始类型时,error 应该返回什么呢?

为了让 error 可以适用于所有的原始类型 (升格的和未升格的),我们需要 levity polymorphism

秘诀在于我们之前提到的 TYPE r kind。这种 kind 是 r :: RuntimeRep 的参数化的结果,描述了类型的运行时状态,其取值可以为下列之一:

1
2
3
4
5
6
7
8
9
10
11
12
data RuntimeRep = VecRep VecCount VecElem   -- ^ a SIMD vector type
| TupleRep [RuntimeRep] -- ^ An unboxed tuple of the given reps
| SumRep [RuntimeRep] -- ^ An unboxed sum of the given reps
| LiftedRep -- ^ lifted; represented by a pointer
| UnliftedRep -- ^ unlifted; represented by a pointer
| IntRep -- ^ signed, word-sized value
| WordRep -- ^ unsigned, word-sized value
| Int64Rep -- ^ signed, 64-bit value (on 32-bit only)
| Word64Rep -- ^ unsigned, 64-bit value (on 32-bit only)
| AddrRep -- ^ A pointer, but /not/ to a Haskell value
| FloatRep -- ^ a 32-bit floating point number
| DoubleRep -- ^ a 64-bit floating point number

我们之前已经见过 TYPE 'IntRep 是未升格的 integer 的 kind,TYPE 'FloatRep 是未升格的 float 的kind。对于 TYPE 'LiftRep 则是所有升格的类型的 kind,事实上,* 就是 TYPE 'LiftRep同义词

所以,实际上我们可以用 TYPE r 表示未升格的类型和已经升格的类型。

1
2
3
4
5
6
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExplicitForAll #-}

import GHC.Exts (TYPE, RuntimeRep)

error :: forall (r :: RuntimeRep) (a :: TYPE r). String -> a

此时,error 就可以同时被应用于 incrementincrementUnlifted 了。

levity polymorphism 也有其自身的限制,有些地方并不能使用,这里可以了解到具体不能使用的地方和不能使用的原因。

总结

到目前为止读者可能会好奇:上面的这些东西有什么意义?为什么要有 kind 系统?为什么我们会关心 kind?实际上,在 Java 或 C# 等语言中所有的泛型类型 <T> 都属于 * 的 kind,我们无法得到例如 Functor<List> 的这种拥有 * -> * 的 kind 的类型。如果没有 kind 系统,我们无法定义 functor 和 monad,甚至之前提到的 NonEmpty f a 都无法做到。更进一步,利用 levity polymorphism,我们可以实现同时适用于升格类型和未升格类型的抽象,而 Java 只能实现适用于升格类型的泛型变量。

同时,kind 系统打开了通向类型层面编程的大门,类似于 Connection sMoney c 等可扩展的记录 (record)、Servant 的类型层面的 web API都可以通过 kind 实现。Simon Peyton Jones 整合前沿研究,讨论了在 Haskell 中的 practical linearity,通过这种方式可以给函数类型 (->) a b 一个额外的拥有 Linearity 的 kind 类型变量 l ,这里 Linearity 是类型 OmegaOne 的整合。

另一个读者可能会问的问题是:如果所有的表达式都有类型、所有的类型都有 kind,那么所有的 kind 会有什么?在 GHC 7 及其之前的版本中,kind 拥有的是 sorts,所有的 kind 都有一个唯一的 sort Box,这些 sort 仅存在与 GHC 的内部,对于我们开发人员来说是不可见的。

在 GHC 8 中,情况有了一点变化。读者可能注意到,本文尝试比较类型和 kind 之间的相似程度:包括都可以实现高阶、都可以有多态性、都可以被推断、都可以进行科里化。这并不是巧合!随着 GHC 8 中 TypeInType 扩展的到来,类型 (type) 和 kind (包括 sort) 都称为了同一个东西。如之前类型属于 kind,现在类型可以属于其他的类型。3 属于类型 IntInt 属于类型 ** 属于类型 *。这种统一为 Haskell 实现完全类型依赖铺平了道路。

在最近的论文中,读者可能会看到 kind * 被认为是 Type (和前文的 TYPE r 不是同一个东西),目前 (2018 年) 这两个词是同义词,(2021 年已取消) ,已逐步过渡为 Type

如果想要了解更多关于类型依赖的知识,可以阅读 Type-Driven Development with Idris 这本书 或最新发布的 The Little Typer 这本书