与DataKinds玩 - 种不匹配错误(Playing with DataKinds - Kind

我一直在自学有关的类型级编程和想写一个简单的自然数加法型的功能。 我这工作的第一个版本如下：

data Z
data S n

type One = S Z
type Two = S (S Z)

type family Plus m n :: *
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

因此，在GHCI我可以这样做：

ghci> :t undefined :: Plus One Two
undefined :: Plus One Two :: S * (S * (S * Z))

其按预期工作。 于是我决定通过修改来尝试一下DataKinds扩展Z和S类型：

data Nat = Z | S Nat

而Plus系列现在返回一个Nat类型：

type family Plus m n :: Nat

修改后的代码编译，但问题是测试时它现在我得到一个错误：

Kind mis-match
Expected kind `OpenKind', but `Plus One Two' has kind `Nat'
In an expression type signature: Plus One Two
In the expression: undefined :: Plus One Two

我搜索的解决方案，但谷歌已经让我失望。 是否解决存在或有我打了语言的一些限制？

Answer 1:

我认为你正在测试的方法是不正确的。 undefined可以是任何类型有种* （我这里可能是错误的）。

在ghci中尝试这个

ghci>:t (undefined :: 'Z)

<interactive>:1:15:
    Kind mis-match
    Expected kind `OpenKind', but `Z' has kind `Nat'
    In an expression type signature: Z
    In the expression: (undefined :: Z)

你仍然可以使用的类型Plus One Two用:kind! 在ghci中

ghci>:kind! Plus One Two
Plus One Two :: Nat
= S (S (S 'Z))

文章来源: Playing with DataKinds - Kind mis-match errors