![plus]( "plus")
本文介绍了玩DataKinds - 种类不匹配错误的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
我一直在教自己关于类型级编程，并想写一个简单的自然数加法类型函数。我的第一个版本工作如下：
pre code $ Z
data S
类型One = SZ
类型Two = S（SZ）
类型系列Plus mn :: *
类型实例Plus Z n = n
类型实例Plus（S m）n = S（Plus mn）
所以在GHCi中我可以这样做：
ghci> ：t undefined :: Plus One Two
undefined :: Plus One Two :: S *（S *（S * Z））
其中按预期工作。然后我决定通过修改 Z 和 S 类型来试用DataKinds扩展：
数据Nat = Z | S Nat
Plus系列现在返回一个 Nat kind：
type family Plus mn :: Nat
修改后的代码会编译，但问题是我现在在测试时遇到错误：
种类不匹配
预期种类`OpenKind'，但是`Plus One Two'种类'Nat'
在表达式类型签名中：Plus One Two
在表达式中：undefined :: Plus One Two
我已经在寻找解决方案，但Google让我失望了。解决方案是否存在或者我是否遇到了一些语言限制？
解决方案 我认为你测试的方式是不正确的。 undefined 可以是任何类型的类型 * （我可能在这里错了）。
在ghci中试试这个
ghci>：t（undefined： ：'Z）
<互动>：1：15：
种类不匹配
预期种类'OpenKind'，但'Z'种类'Nat'
在表达式类型签名中：Z
在表达式中：（undefined :: Z）
通过在ghci中使用：kind！，你仍然可以获得 Plus One Two 类型
ghci>：kind！ Plus One Two
Plus One Two :: Nat
= S（S（S'Z））
I've been teaching myself about type-level programming and wanted to write a simple natural number addition type function. My first version which works is as follows:
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)
So in GHCi I can do:
ghci> :t undefined :: Plus One Two
undefined :: Plus One Two :: S * (S * (S * Z))
Which works as expected. I then decided to try out the DataKinds extension by modifying the Z and S types to:
data Nat = Z | S Nat
And the Plus family now returns a Nat kind:
type family Plus m n :: Nat
The modified code compiles but the problem is I now get an error when testing it:
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
I've searched for a solution but Google has failed me. Does a solution exist or have I hit some limit of the language?
解决方案
I think way you are testing is not correct. undefined can be of any type of kind * (I maybe wrong here).
Try this in 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)
You can still get the type of Plus One Two by using :kind! in ghci
ghci>:kind! Plus One Two
Plus One Two :: Nat
= S (S (S 'Z))
这篇关于玩DataKinds - 种类不匹配错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！