Perbedaan antara Agda dan Idris

Saya mulai terjun ke pemrograman yang diketik secara dependen dan telah menemukan bahwa bahasa Agda dan Idris adalah yang paling dekat dengan Haskell, jadi saya mulai di sana.

Pertanyaan saya adalah: manakah perbedaan utama di antara mereka? Apakah sistem jenisnya sama-sama ekspresif pada keduanya? Alangkah baiknya memiliki komparatif yang komprehensif dan diskusi tentang manfaat.

Saya dapat menemukan beberapa:

• Idris memiliki kelas tipe à la Haskell, sedangkan Agda menggunakan argumen instan
• Idris termasuk notasi monadik dan aplikatif
• Keduanya tampaknya memiliki semacam sintaks yang dapat di-rebindable, walaupun tidak terlalu yakin apakah keduanya sama.

Sunting : ada beberapa jawaban lagi di halaman Reddit dari pertanyaan ini: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Saya mungkin bukan orang terbaik untuk menjawab ini, karena setelah menerapkan Idris, saya mungkin sedikit bias! FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - memiliki sesuatu untuk dikatakan, tetapi untuk sedikit memperluas:

Idris telah dirancang dari bawah ke atas untuk mendukung pemrograman tujuan umum sebelum pembuktian teorema, dan karena itu memiliki fitur tingkat tinggi seperti kelas tipe, notasi, kurung idiom, daftar pemahaman, kelebihan beban dan sebagainya. Idris menempatkan pemrograman tingkat tinggi di atas bukti interaktif, meskipun karena Idris dibangun di atas elaborator berbasis taktik, ada antarmuka untuk pepatah teorema interaktif berbasis taktik (sedikit seperti Coq, tetapi tidak se-maju, setidaknya belum).

Hal lain yang Idris ingin dukung dengan baik adalah implementasi DSL Tertanam. Dengan Haskell Anda bisa mendapatkan banyak hal dengan notasi, dan Anda bisa dengan Idris juga, tetapi Anda juga dapat memutar ulang konstruk lain seperti aplikasi dan pengikatan variabel jika Anda perlu. Anda dapat menemukan rincian lebih lanjut tentang ini di tutorial, atau rincian lengkap di makalah ini: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

Perbedaan lainnya adalah dalam kompilasi. Agda berjalan melalui Haskell, Idris via C. Ada back end eksperimental untuk Agda yang menggunakan back end yang sama dengan Idris, via C. Saya tidak tahu seberapa baik mempertahankannya. Tujuan utama Idris akan selalu menghasilkan kode yang efisien - kami dapat melakukan jauh lebih baik daripada yang kami lakukan saat ini, tetapi kami sedang mengusahakannya.

Sistem tipe di Agda dan Idris sangat mirip dalam banyak hal penting. Saya pikir perbedaan utamanya adalah dalam penanganan alam semesta. Agda memiliki polimorfisme semesta, Idris memiliki kumulatif (dan Anda dapat memiliki Set : Setkeduanya jika Anda menemukan ini terlalu ketat dan tidak keberatan bahwa bukti Anda mungkin tidak sehat).

Satu perbedaan lain antara Idris dan Agda adalah bahwa kesetaraan proposisional Idris heterogen, sedangkan Agda adalah homogen.

Dengan kata lain, definisi diduga kesetaraan dalam Idris adalah:

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

sementara di Agda, itu

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

Aku dalam definisi Agda dapat diabaikan, karena ada hubungannya dengan polimorfisme alam semesta yang Edwin sebutkan dalam jawabannya.

Perbedaan penting adalah bahwa tipe kesetaraan dalam Agda mengambil dua elemen A sebagai argumen, sementara di Idris dapat mengambil dua nilai dengan tipe yang berpotensi berbeda .

Dengan kata lain, di Idris kita dapat mengklaim bahwa dua hal dengan tipe yang berbeda adalah sama (bahkan jika itu berakhir dengan klaim yang tidak dapat dibuktikan), sedangkan di Agda, pernyataan itu sama sekali tidak masuk akal.

Ini memiliki konsekuensi penting dan jangkauan luas untuk teori tipe, terutama mengenai kelayakan bekerja dengan teori tipe homotopy. Untuk ini, kesetaraan heterogen tidak akan berfungsi karena memerlukan aksioma yang tidak konsisten dengan HoTT. Di sisi lain, dimungkinkan untuk menyatakan teorema yang berguna dengan kesetaraan heterogen yang tidak dapat secara langsung dinyatakan dengan kesetaraan homogen.

Mungkin contoh termudah adalah asosiatif penggabungan vektor. Diberikan daftar panjang-diindeks yang disebut vektor yang didefinisikan demikian:

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

dan rangkaian dengan tipe berikut:

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

kami mungkin ingin membuktikan bahwa:

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

Pernyataan ini omong kosong di bawah kesetaraan homogen, karena sisi kiri kesetaraan memiliki tipe Vect (n + (m + o)) adan sisi kanan memiliki tipe Vect ((n + m) + o) a. Ini adalah pernyataan yang sangat masuk akal dengan kesetaraan heterogen.