私は型レベルのプログラミングについて独学しており、単純な自然数加算型関数を書きたいと思っていました。動作する私の最初のバージョンは次のとおりです。
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 は失敗しました。解決策はありますか、それとも言語の制限に達しましたか?