5

我一直在自学类型级编程，并想编写一个简单的自然数加法类型函数。我的第一个版本如下：

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

我一直在寻找解决方案，但谷歌让我失望了。是否存在解决方案或者我是否达到了语言的某些限制？

4

1 回答 1

8

我认为您测试的方式不正确。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))
于 2012-10-15T12:38:16.270 回答