9

データ型の等価 ( DecEq) インスタンスを記述する簡単な方法はありますか? たとえば、次のDecEq宣言には O(n) 行が必要です。ここで、?pは単純なものです。

data Foo = A | B | C | D

instance [syntactic] DecEq Foo where
   decEq A A = Yes Refl
   decEq B B = Yes Refl
   decEq C C = Yes Refl
   decEq D D = Yes Refl
   decEq _ _ = No ?p
4

1 に答える 1

8

David Christiansen は、これを一般的に自動化するための作業を行っており、基本的には完成しています。彼の GitHub リポジトリにあります。それまでの間、この状況で O(n^2) ケースから O(n) ケースに移行できるアプローチを次に示します。まず、いくつかの予備。決定可能な等価性を持つものがあり、選択した型からその型への注入がある場合、その型の決定手順を作成できます。

IsInjection : (a -> b) -> Type
IsInjection {a} f = (x,y : a) -> f x = f y -> x = y

decEqInj : DecEq d => (tToDec : t -> d) ->
                      (isInj : IsInjection tToDec) ->
                      (p, q : t) -> Dec (p = q)
decEqInj tToDec isInj p q with (decEq (tToDec p) (tToDec q))
  | (Yes prf) = Yes (isInj p q prf) 
  | (No contra) = No (\pq => contra (cong pq))

残念ながら、関数が注入であることを直接証明すると、O(n^2) のケースに戻りますが、一般に、リトラクションを伴う関数はすべて単射です。

retrInj : (f : d -> t) -> (g : t -> d) ->
          ((x : t) -> f (g x) = x) ->
          IsInjection g
retrInj f g prf x y gxgy =
  let fgxfgy = cong {f} gxgy
      foo = sym $ prf x
      bar = prf y
  in trans foo (trans fgxfgy bar)

したがって、選択した型から決定可能な等値とそれに対する撤回を持つ関数がある場合、その型には決定可能な等値があります。

decEqRet : DecEq d => (decToT : d -> t) ->
           (tToDec : t -> d) ->
           (isRet : (x : t) -> decToT (tToDec x) = x) ->
           (p, q : t) -> Dec (p = q)
decEqRet decToT tToDec isRet p q =
  decEqInj tToDec (retrInj decToT tToDec isRet) p q

最後に、選択したもののケースを記述できます。

data Foo = A | B | C | D

natToFoo : Nat -> Foo
natToFoo Z = A
natToFoo (S Z) = B
natToFoo (S (S Z)) = C
natToFoo _ = D

fooToNat : Foo -> Nat 
fooToNat A = 0
fooToNat B = 1
fooToNat C = 2
fooToNat D = 3

fooNatFoo : (x : Foo) -> natToFoo (fooToNat x) = x
fooNatFoo A = Refl
fooNatFoo B = Refl
fooNatFoo C = Refl
fooNatFoo D = Refl

instance DecEq Foo where
  decEq x y = decEqRet natToFoo fooToNat fooNatFoo x y

このnatToFoo関数には多少大きなパターンがありますが、実際にはあまり行われていないことに注意してください。醜いかもしれませんが、パターンを入れ子にすることでパターンを小さくすることはおそらく可能なはずです。

一般化: 最初は、これは特殊な場合にしか機能しないと思っていましたが、今ではそれよりも少し良いかもしれないと考えています. Either特に、決定可能な等価性を持つ型を保持する代数的データ型がある場合、それを入れ子の入れ子に変換できるはずPairです。たとえば ( をMaybe短縮するために使用Either (Bool, Nat) ()):

data Fish = Cod Int | Trout Bool Nat | Flounder

watToFish : Either Int (Maybe (Bool, Nat)) -> Fish
watToFish (Left x) = Cod x
watToFish (Right Nothing) = Flounder
watToFish (Right (Just (a, b))) = Trout a b

fishToWat : Fish -> Either Int (Maybe (Bool, Nat))
fishToWat (Cod x) = Left x
fishToWat (Trout x k) = Right (Just (x, k))
fishToWat Flounder = Right Nothing

fishWatFish : (x : Fish) -> watToFish (fishToWat x) = x
fishWatFish (Cod x) = Refl
fishWatFish (Trout x k) = Refl
fishWatFish Flounder = Refl

instance DecEq Fish where
  decEq x y = decEqRet watToFish fishToWat fishWatFish x y
于 2015-05-19T20:39:39.347 に答える