Różnice między Agdą a Idrisem

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/

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

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ą.