亲切的签名 [英] Kind Signatures

问题描述

我正在阅读 Haskell wiki 书籍 GADTS

I am going through the Haskell wiki books GADTS

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

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

I was tracking pretty well until a Kind signature was added which generalizes the constrained type of the Cons constructor.

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 构造函数来构造和模式匹配安全和不安全的 MarkedList.虽然我明白发生了什么，但不幸的是，我无法建立关于 Kind 签名如何允许这一点的任何直觉.为什么我需要 Kind 签名?Kind 签名在做什么?

With the Kind Signature I can use the Cons constructor to construct and pattern match against both Safe and Unsafe MarkedLists. While I understand what going on I am unfortunately having trouble building any intuition as to how the Kind Signature is allowing this. Why do I need the Kind Signature? What is the Kind Signature doing?

推荐答案

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

The same way a type signature works for values, a kind signature works for types.

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

这里，f 接受两个参数值并产生一个结果值.类型的等价物可能是:

Here, f takes two argument values and produces a result value. The equivalent for types could be:

data D a b = D a b

类型 D 接受两个参数类型并产生一个结果类型(它是 * -> * -> *).例如，D Int String 是一种类型(其种类为 *).部分应用程序 D Int 的类型为 * ->*，就像部分应用程序 f 15 的类型 Int ->布尔.

The type D takes two argument types and produces a result type (it is * -> * -> *). For example, D Int String is a type (which has kind *). The partial application D Int has kind * -> *, just the same way the partial application f 15 has type Int -> Bool.

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

So we could rewrite the above as:

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

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

In GHCi, you can query types and kinds:

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

这篇关于亲切的签名的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！