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

解決策を探しましたが、Google は失敗しました。解決策はありますか、それとも言語の制限に達しましたか?

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)

ghciPlus One Twoで使用して の型を取得できます:kind!

ghci>:kind! Plus One Two
Plus One Two :: Nat
= S (S (S 'Z))
于 2012-10-15T12:38:16.270 に答える