haskell - 不寻常的种类和数据构造函数

Question

我不知道我怎么没有注意到这一点，但是数据构造函数和函数定义都不能使用类型以外的类型*和它的变体* -> *等，因为(->)'s kind 签名，即使在-XPolyKinds.

这是我尝试过的代码：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Nat = S Nat | Z

data Foo where
  Foo :: 'Z -> Foo -- Fails

foo :: 'Z -> Int -- Fails
foo _ = 1

我得到的错误如下：

<interactive>:8:12:
    Expected a type, but ‘Z’ has kind ‘Nat’
    In the type signature for ‘foo’: foo :: 'Z -> Int

为什么我们不应该允许非传统类型的模式匹配？

Answer 1

没有“类型以外的类型”之类的^东西*。kind*是类型的kind，很像机器大小的数字的Inttype ；其他类型可能包含类似于类型的东西，或者可以转换为类型或用于索引类型或其他东西——但不是类型本身，仅仅是“类型级别的实体”。

---

¹_{像往常一样，我在这里忽略 unbox-kinds。}