Różnice między Agdą a Idrisem

165

Zaczynam zagłębiać się w programowanie zależne i odkryłem, że języki Agda i Idris są najbliższe Haskellowi, więc zacząłem tam.

Moje pytanie brzmi: jakie są główne różnice między nimi? Czy systemy typów są jednakowo ekspresyjne w obu z nich? Byłoby wspaniale mieć kompleksowe porównanie i dyskusję na temat korzyści.

Udało mi się dostrzec kilka:

  • Idris ma klasy typów à la Haskell, podczas gdy Agda używa argumentów instancji
  • Idris zawiera notację monadyczną i aplikacyjną
  • Oba wydają się mieć jakąś składnię możliwą do ponownego przypisania, chociaż nie jestem pewien, czy są takie same.

Edycja : na stronie Reddit jest więcej odpowiedzi na to pytanie: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

serras
źródło
1
Możesz rzucić okiem na coq aswel, składnia nie jest oddalona o milion mil od haskell i ma łatwe w użyciu klasy typów :)
4
Dla przypomnienia: Agda ma obecnie również notacje monadyczne i aplikacyjne.
gallais

Odpowiedzi:

190

Może nie jestem najlepszą osobą, która odpowie na to pytanie, ponieważ po wdrożeniu Idris jestem prawdopodobnie nieco stronniczy! Często zadawane pytania - http://docs.idris-lang.org/en/latest/faq/faq.html - ma coś do powiedzenia na ten temat, ale aby to trochę rozwinąć:

Idris został zaprojektowany od podstaw do obsługi programowania ogólnego przeznaczenia przed dowodzeniem twierdzeń i jako taki ma funkcje wysokiego poziomu, takie jak klasy typów, notacja, nawiasy idiomowe, rozumienie list, przeciążanie i tak dalej. Idris stawia programowanie na wysokim poziomie przed interaktywnym dowodem, chociaż ponieważ Idris jest zbudowany na taktycznym elaboratorze, istnieje interfejs do interaktywnego dowodu twierdzenia opartego na taktyce (trochę jak Coq, ale nie tak zaawansowany, przynajmniej jeszcze nie teraz).

Inną rzeczą, którą Idris ma dobrze wspierać, jest implementacja wbudowanego DSL. Z Haskellem możesz przejść długą drogę z notacją, i możesz to zrobić z Idrisem, ale możesz także zmienić inne konstrukcje, takie jak aplikacja i zmienne wiązanie, jeśli zajdzie taka potrzeba. Więcej szczegółów na ten temat można znaleźć w samouczku lub pełne informacje w tym artykule: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

Kolejna różnica dotyczy kompilacji. Agda płynie głównie przez Haskell, Idris przez C. Istnieje eksperymentalny back-end dla Agdy, który używa tego samego zaplecza co Idris, przez C. Nie wiem, jak dobrze jest utrzymany. Głównym celem Idris zawsze będzie generowanie wydajnego kodu - możemy zrobić dużo lepiej niż obecnie, ale pracujemy nad tym.

Systemy czcionek w Agdzie i Idrisie są bardzo podobne pod wieloma ważnymi względami. Myślę, że główna różnica polega na obsłudze wszechświatów. Agda ma polimorfizm wszechświatowy, Idris ma kumulatywność (i możesz mieć Set : Setw obu, jeśli uznasz to za zbyt restrykcyjne i nie przejmuj się, że twoje dowody mogą być błędne).

Edwin Brady
źródło
49
Co masz na myśli, mówiąc: „... nie jest najlepszą osobą do odpowiedzi ...”? Jesteś jedną z najlepszych osób, które odpowiedzą, skoro dobrze znasz Idris. Teraz potrzebujemy tylko NAD, aby odpowiedzieć i mamy cały obraz :) Dziękujemy za poświęcenie czasu na odpowiedź.
Alex R
9
Czy jest miejsce, w którym mogę przeczytać więcej o kumulatywności? Nigdy wcześniej o tym nie słyszałem ...
serras
13
Książka Adama Chlipali jest prawdopodobnie najlepszym miejscem:
Edwin Brady
8
Pierwszy rozdział książki HoTT również opisuje to dość jasno, choć zwięźle.
David Christiansen
50

Inną różnicą między Idrisem i Agdą jest to, że propozycjonalna równość Idrisa jest heterogeniczna, podczas gdy Agda jest jednorodna.

Innymi słowy, domniemana definicja równości w Idrisie brzmiałaby:

data (=) : {a, b : Type} -> a -> b -> Type where
  refl : x = x

podczas gdy w Agdzie jest

data _≡_ {l} {A : Set l} (x : A) : A → Set a where
    refl : x ≡ x

L w definicji Agdy można zignorować, ponieważ ma ono związek z polimorfizmem wszechświata, o którym wspomina Edwin w swojej odpowiedzi.

Ważną różnicą jest to, że typ równości w Agdzie przyjmuje dwa elementy A jako argumenty, podczas gdy w Idrisie może przyjmować dwie wartości o potencjalnie różnych typach.

Innymi słowy, w Idrisie można twierdzić, że dwie rzeczy o różnych typach są sobie równe (nawet jeśli okaże się to twierdzeniem nie do udowodnienia), podczas gdy u Agdy samo stwierdzenie jest nonsensem.

Ma to ważne i szeroko zakrojone konsekwencje dla teorii typów, zwłaszcza w odniesieniu do wykonalności pracy z teorią typów homotopii. W tym celu heterogeniczna równość po prostu nie zadziała, ponieważ wymaga aksjomatu, który jest niespójny z HoTT. Z drugiej strony możliwe jest sformułowanie użytecznych twierdzeń o niejednorodnej równości, której nie można w prosty sposób stwierdzić przy jednorodnej równości.

Być może najłatwiejszym przykładem jest asocjatywność konkatenacji wektorów. Biorąc pod uwagę listy indeksowane długością zwane wektorami zdefiniowanymi w ten sposób:

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a 

i konkatenacja z następującym typem:

(++) : Vect n a -> Vect m a -> Vect (n + m) a

możemy chcieć udowodnić, że:

concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
              xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

To stwierdzenie jest nonsensowne w warunkach jednorodnej równości, ponieważ lewa strona równości ma typ, Vect (n + (m + o)) aa prawa strona ma typ Vect ((n + m) + o) a. To całkowicie rozsądne stwierdzenie z heterogeniczną równością.

David Christiansen
źródło
26
Wydaje się, że bardziej komentujesz standardową bibliotekę Agdy niż podstawową teorię Agdy , ale nawet standardowa biblioteka zawiera zarówno jednorodną, ​​jak i heterogeniczną równość ( cse.chalmers.se/~nad/listings/lib/… ). Ludzie po prostu używają tego pierwszego częściej, jeśli to możliwe. To ostatnie jest równoważne stwierdzeniu, że typy są równe, po którym następuje jeden dotyczący wartości. W świecie, w którym równość typów jest dziwna (HoTT), heteq jest dziwniejszym stwierdzeniem.
Tajemniczy Dan,
6
Nie rozumiem, dlaczego to stwierdzenie jest nonsensowne w warunkach jednorodnej równości. Chyba że się mylę (n + (m + o))i ((n + m) + o)są one osądowo równe przez łączność +on (wyprowadzone z zasady indukcji). W związku z tym każda strona równości ma ten sam typ. Różnica między typami równości jest ważna, ale nie widzę, jak to jest przykładem.
5
@Abhishek czy równość osądów nie jest tym samym, co równość definicyjna? Myślę, że chcesz powiedzieć, że (n + (m + o)) i ((n + m) + o) są propozycyjnie równe, ale nie są równe definicji / osądu.
Tom Crockett
3
dobrze. Kiedy mówiłem o równości osądów, miałem na myśli równość zdań. Przepraszam. Oto poprawiony komentarz: (n + (m + o)) i ((n + m) + o) są propozycyjnie równe, ale nie są równe definicji. Jeśli masz: A, a: B zachowuje się tylko wtedy, gdy A i B są definicjami równymi typami. Dla rozstrzygalności sprawdzania typów, równość definicji musi być rozstrzygalna. W teoriach typu ekstensjonalnego równość definicyjna zbiega się z równością zdań, a zatem sprawdzanie typów jest nierozstrzygalne.W Coq równość definicji obejmuje tylko obliczenia, równość alfa, rozwinięcie definicji.
Abhishek Anand