问题亲切的签名

我正在浏览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做什么？

6605

2018-03-25 02:52

起源

答案:

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

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 :: * -> * -> *

2018-03-25 02:57

我还是很困惑 MarkedList a b where ... 似乎也适用于GHC 7.4.1。我不确定签名提供的是什么。 - ExternalReality

这看起来像对我说同样的事情的另一种方式。 - Dietrich Epp

是的，但Kind Signature需要语言编译，而后者不需要。为什么，如果两种方式都相同？ Kind Signature提供多少额外服务？ - ExternalReality

在其他情况下，您可能希望指定其他类型。例如， data X a = X。这里， X 善良 * -> * 并且它的参数必须是nullary。您可以为其参数指定一元类型 data X (a :: * -> *) = X所以 X 会有所帮助 (* -> *) -> *，所以你可以，例如参数 X 在仿函数或monad或不是nullary的东西。我认为在你说的例子中没有必要。 - Dietrich Epp

@ExternalReality :(重新说：“Kind Signature提供了什么额外的东西？”，除了Dietrich Epp所说的）人们可以考虑 MarkedList a b where ... 语法有点误导，因为它看起来像名字 a 和 b 必须在体内使用（之后） where）实际上，它们根本没有效果（每个构造函数都绑定自己的名字）。写作 MarkedList :: * -> * -> * 避免这种情况。不过只是品味问题。 - FunctorSalad

答案: