玩DataKinds - 种类不匹配错误

Question

我一直在教我自己关于类型级编程，并想写一个简单的自然数加法类型的函数。我这工作的第一个版本如下：

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)) 

预期其中一期工程。于是我决定通过修改Z和S类型尝试的DataKinds扩展：

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 

我已经搜索了解决方案，但Google已经失败了我。解决方案是否存在或我是否遇到了一些语言限制？

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) 

试试这个你仍然可以通过在ghci中使用:kind!

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