Does Idris miał odpowiednik Agda za ↔

Question

Agda korzysta z następujących operatora pokazać odwrotności między seriami:

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

Czy istnieje odpowiednik w Idris? Próbuję zdefiniować równość torbę na listach

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 

Tak, że możemy skonstruować l1 ~~ l2 gdy l1 i l2 mają te same elementy w dowolnej kolejności.

Wydaje się, że Agda definition of ↔ jest bardzo skomplikowany i nie jestem pewien, czy istnieje odpowiednik w standardowej bibliotece Idris.

Answer 1

Podstawową ideą Agda na ↔ jest pakowanie się dwie funkcje z dwóch dowodów roundtripping, co jest dość łatwe do zrobienia w Idris także:

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 

Można go używać jak w następujący minimalny przykład:

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

powodem wersja Agda jest bardziej skomplikowana, ponieważ jest parametryzowane nad wyborem równości, tak więc to nie musi być zdaniowa jeden (który jest najściślejszy/najlepszy). Parametryzacja definicji Idris z ~~ powyżej z do arbitralnego PA : A -> A -> Type i PB : B -> B -> Type jest pozostawiona jako ćwiczenie dla czytnika.