亲切的签名 [英] 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屋!