6

haskellに2つの型レベルの自然数を追加することは不可能だと思います。これは本当ですか？

自然数が次のように定義されているとします。

class HNat a

data HZero
instance HNat HZero

data HSucc n
instance (HNat n) => HNat (HSucc n)

次のような方法でHAddを定義することは可能ですか？

class (HNat n1, HNat n2, HNat ne) => HAdd n1 n2 ne | n1 n2 -> ne
instance             HAdd HZero HZero HZero
instance (HNat x) => HAdd HZero x     x
instance (HNat n1 
         ,HNat x) => HAdd (HSucc n1)  x (HAdd n1 (HSucc x) (???))
4

2 に答える 2

20

HZeroとを追加する場合は必要ありませんHZero。これはすでに2番目のケースでカバーされています。最初の引数の帰納法によって、用語レベルでPeanoナチュラルを追加する方法を考えてください。

 data Nat = Zero | Succ Nat

 add :: Nat -> Nat -> Nat
 add Zero     y = y
 add (Succ x) y = Succ (add x y)

関数従属性を使用している場合は、ロジックプログラムを作成しています。したがって、右側で再帰呼び出しを行う代わりに、左側で再帰呼び出しの結果に制約を追加します。

 class (HNat x, HNat y, HNat r) => HAdd x y r | x y -> r
 instance (HNat y)     => HAdd HZero     y y
 instance (HAdd x y r) => HAdd (HSucc x) y (HSucc r)

HNat2番目のインスタンスでは制約は必要ありません。それらは、クラスのスーパークラス制約によって暗示されます。

DataKinds最近では、この種の型レベルのプログラミングを行う最も良い方法は、とを使用することだと思いますTypeFamilies。用語レベルと同じように定義します。

 data Nat = Zero | Succ Nat

Natこれにより、タイプとしてだけでなく、種類としても使用できます。次に、次のように2つの自然数に加算する型族を定義できます。

 type family Add (x :: Nat) (y :: Nat) :: Nat
 type instance Add Zero     y = y
 type instance Add (Succ x) y = Succ (Add x y)

これは、加算の用語レベルの定義にはるかに近いものです。また、「プロモート」の種類Natを使用すると、などのクラスを定義する必要がなくなりますHNat。

于 2013-01-28T13:10:14.317 に答える
3

可能です。パッケージtype-level-natural-numberとを見てください`type-level-natural-number-operations。どちらも少し古いですが、使いやすく、後者はPlus型族を定義しています。

とにかく、私はあなたの最後の行をこのようなものに変更します（これがコンパイルされるかどうかはテストしませんでした）。

instance (HNat n1, HNat x, HAdd n1 x y) => HAdd (HSucc n1) x (HAdd n1 x (HSucc y))

基本的に、あなたがすることは帰納的に加算を定義することであり、追加HAdd n1 x yの制約は必要な帰納的なケースを追加します。

于 2013-01-28T12:00:28.980 に答える