6

采取以下代码：

{-# LANGUAGE KindSignatures, DataKinds #-}

data Nat = O | S Nat

class NatToInt (n :: Nat) where
    natToInt :: n -> Int

instance NatToInt O where
    natToInt _ = 0

instance (NatToInt n) => NatToInt (S n) where
    natToInt _ = 1 + natToInt (undefined :: n)

GHC 告诉我们它OpenKind在类型规范中期望natToInt​​ a 而不是 a Nat，因此拒绝编译。这可以通过某种类型的转换来解决：

data NatToOpen :: Nat -> *

然后用nin NatToOpen nt替换natToInt-s。

*问题 1：除了在任何函数中不使用类型级包装器之外，还有其他方法可以指定种类吗？

问题 2：在我看来，非类函数很乐意与任何类型的类型一起工作，例如：

foo :: (a :: *) -> (a :: *)
foo = id

bar = foo (S O)

但是在类内部，编译器会抱怨种类不匹配，如上所述。这是为什么？似乎非类函数在种类上不是适当的多态，因为上面我实际上指定 *了 ，它仍然可以与Nat-s 一起使用，就好像这些种类被简单地忽略了一样。

4

1 回答 1

6

值总是有种类的类型*（可能有一些涉及拆箱的奇怪例外？），所以没有什么可以应用函数或作为具有其他种类的参数。

在你的最后一个例子中，你申请foo的是未提升的版本Nat：值是Sand O，它们的类型是Nat，它有 kind *。在类定义中，您Nat使用签名作为一种类型，这意味着提升的版本， whereS和Oare types。

该NatToOpen类型只是以通常的方式使用幻像类型，但带有非*种类的幻像类型参数。

这种区别对 来说也不新鲜DataKinds。例如，没有类型为 的值，Maybe :: * -> *与 type 不同forall a. Maybe a :: *，后者是 的类型Nothing。

于 2013-05-03T12:49:14.170 回答