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

Question

我不知道我怎么没有注意到这一点，但是数据构造函数和函数定义都不能使用除 * 以外的类型的类型。它的变体 * -> *等等，由于(->)善意的签名，即使在 -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

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

1像往常一样，我在这里不理会 unbox-kinds。