fa Idris ha un equivalente di Agda ↔

Question

Agda si avvale dei seguenti all'operatore di mostrare inverse tra le serie:

_↔_ : ∀ {f t} → Set f → Set t → Set _ 

Esiste un equivalente in Idris? Sto cercando di definire l'uguaglianza borsa sulle liste

data Elem : a -> List a -> Type where 
    Here : {xs : List a} -> Elem x (x :: xs) 
    There : {xs : List a} -> Elem x xs -> Elem x (y :: xs) 

(~~) : List a -> List a -> Type 
xs ~~ ys {a} = Elem a xs <-> Elem a ys 

In modo che possiamo costruire l1 ~~ l2 quando l1 e l2 hanno gli stessi elementi in qualsiasi ordine.

Il Agda definition of ↔ sembra essere molto complicato e non sono sicuro se c'è qualcosa di equivalente nella libreria standard di Idris.

Answer 1

L'idea alla base Agda di ↔ è di confezionare due funzioni con due prove di roundtripping, il che è abbastanza facile da fare in Idris così:

infix 7 ~~ 
data (~~) : Type -> Type -> Type where 
    MkIso : {A : Type} -> {B : Type} -> 
      (to : A -> B) -> (from : B -> A) -> 
      (fromTo : (x : A) -> from (to x) = x) -> 
      (toFrom : (y : B) -> to (from y) = y) -> 
      A ~~ B 

è possibile utilizzarlo come nel seguente esempio minimo:

notNot : Bool ~~ Bool 
notNot = MkIso not not prf prf 
    where 
    prf : (x : Bool) -> not (not x) = x 
    prf True = Refl 
    prf False = Refl 

la ragione la versione Agda è più complicato è perché è parametrizzato sulla scelta di uguaglianza pure, quindi non deve essere il proposizionale uno (che è il più rigoroso/migliore che ci sia). La parametrizzazione della definizione di Idris di ~~ da = a PA : A -> A -> Type e PB : B -> B -> Type arbitrari è lasciata come esercizio al lettore.