Easy Syntactic Equality in Idris

Question

Esiste un modo semplice per scrivere le istanze di uguaglianza (DecEq) per i tipi di dati? Ad esempio, mi piacerebbe le linee di seguito per avere O (n) nella sua dichiarazione DecEq, dove ?p è qualcosa di semplice:

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 

Answer 1

David Christiansen sta lavorando a qualcosa per automatizzare questo, in generale, e lui è essenzialmente finito; può essere trovato in his GitHub repository. Nel frattempo, ecco un approccio che può portarti da casi O (n^2) a casi O (n) in questa situazione. Innanzitutto, alcuni preliminari. Se avete qualcosa con l'uguaglianza decidibile, e si dispone di un'iniezione dal tipo di vostra scelta per quel tipo, allora si può fare una procedura di decisione per quel tipo:

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)) 

Purtroppo, direttamente dimostrando che la funzione è un iniezione si torna a O (n^2) casi, ma è generalmente il caso che ogni funzione con una ritrattazione è iniettiva:

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) 

Quindi se avete una funzione dal tipo di vostra scelta per uno con decidibile uguaglianza e un ritiro per esso, quindi avete uguaglianza decidibile per il vostro tipo:

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 

Infine, è possibile scrivere i casi per quello che hai scelto:

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 

notare che, mentre la funzione natToFoo ha un po 'di grandi modelli, non c'è davvero molto succedendo lì. Probabilmente dovrebbe essere possibile rendere i disegni piccoli annidandoli, anche se potrebbe essere brutto.

Generalizzazione: all'inizio pensavo che avrebbe funzionato solo per casi speciali, ma ora penso che potrebbe essere un po 'meglio di così. In particolare, se si dispone di un tipo di dati algebrico contenente tipi con uguaglianza decidibile, si dovrebbe essere in grado di convertirlo in un nidificato Either di nidificato Pair, che vi porterà lì. Per esempio (usando Maybe per accorciare 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