亲切的签名

Question

我正在浏览Haskell维基书籍GADTS

https://en.wikibooks.org/wiki/Haskell/GADT指南.

我一直很好地跟踪,直到添加了一个Kind签名,它概括了Cons构造函数的约束类型.

data Safe
data NotSafe

data MarkedList             ::  * -> * -> * where
  Nil                       ::  MarkedList t NotSafe
  Cons                      ::  a -> MarkedList a b -> MarkedList a c

safeHead                    ::  MarkedList a Safe -> a
safeHead (Cons x _)          =  x


silly 0                      =  Nil
silly 1                      =  Cons () Nil
silly n                      =  Cons () $ silly (n-1)

使用Kind Signature,我可以使用Cons构造函数来构造和模式匹配安全和不安全的MarkedLists.虽然我明白发生了什么,但遗憾的是我难以建立任何关于Kind Signature如何允许这种情况的直觉.为什么我需要种类签名？Kind Signature做什么？

Answer 1

类型签名与值相同的方式,类型签名适用于类型.

f :: Int -> Int -> Bool
f x y = x < y

这里,f获取两个参数值并生成结果值.类型的等价物可以是:

data D a b = D a b

该类型D采用两种参数类型并生成结果类型(它是* -> * -> *).例如,D Int String是一种类型(有种类*).部分应用程序D Int具有类型* -> *,与部分应用程序的f 15类型相同Int -> Bool.

所以我们可以将上面的内容重写为:

data D :: * -> * -> * where
  D :: a -> b -> D a b

在GHCi中,您可以查询类型和种类:

> :type f
f :: Int -> Int -> Bool
> :kind D
D :: * -> * -> *