Perbedaan antara Agda dan Idris

165

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/

serras
sumber
1
Anda mungkin ingin melihat coq aswel, sintaksnya tidak satu juta mil jauhnya dari haskell dan memiliki tipe kelas yang mudah digunakan :)
4
Sebagai catatan: Agda juga memiliki notasi monadik dan aplikatif saat ini.
gallais

Jawaban:

190

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

Edwin Brady
sumber
49
Apa maksudmu, "... bukan orang terbaik untuk dijawab ..."? Anda adalah salah satu orang terbaik untuk menjawab, karena Anda mengenal Idris secara intim. Sekarang kami hanya perlu NAD untuk membalas, dan kami memiliki seluruh gambar :) Terima kasih telah meluangkan waktu untuk membalas.
Alex R
9
Apakah ada tempat di mana saya dapat membaca lebih lanjut tentang kumulatif? Saya belum pernah mendengar tentang itu sebelumnya ...
serras
13
Buku Adam Chlipala mungkin adalah tempat terbaik:
Edwin Brady
8
Bab pertama buku HoTT juga menggambarkannya dengan cukup jelas, jika singkat.
David Christiansen
50

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.

David Christiansen
sumber
26
Anda tampaknya lebih banyak mengomentari tentang perpustakaan standar Agda daripada teori yang mendasari Agda, tetapi bahkan perpustakaan standar berisi kesetaraan homogen dan heterogen ( cse.chalmers.se/~nad/listings/lib/… ). Orang cenderung menggunakan yang pertama lebih sering jika memungkinkan. Yang terakhir ini setara dengan pernyataan bahwa jenisnya sama diikuti oleh satu tentang nilai. Di dunia di mana jenis kesetaraan aneh (HoTT) maka heteq adalah pernyataan yang lebih aneh.
Misterius Dan
6
Saya tidak mengerti bagaimana pernyataan itu omong kosong di bawah kesetaraan homogen. Kecuali saya salah, (n + (m + o))dan ((n + m) + o)secara hukum sama dengan asosiatif +on (berasal dari prinsip induksi). Dengan demikian masing-masing sisi kesetaraan memang memiliki tipe yang sama. Perbedaan antara jenis-jenis kesetaraan itu penting, tetapi saya tidak melihat bagaimana ini adalah contohnya.
5
@Abhishek bukankah kesetaraan menghakimi sama dengan kesetaraan definisi? Saya pikir Anda bermaksud mengatakan (n + (m + o)) dan ((n + m) + o) secara proporsional sama tetapi tidak secara definisi / menghakimi sama.
Tom Crockett
3
Baik. Saya berarti kesetaraan proposisional ketika saya mengatakan kesetaraan menghakimi. Maaf. Berikut adalah komentar yang dikoreksi: (n + (m + o)) dan ((n + m) + o) secara proporsional sama tetapi tidak secara definisi sama. Jika Anda memiliki: A, a: B hanya berlaku jika A dan B secara tipikal sama. Untuk decidability dari typechecking, kesetaraan definisi harus dapat ditentukan. Dalam teori tipe ekstensional, kesetaraan definisi bertepatan dengan kesetaraan proposisional dan karenanya pemeriksaan huruf tidak dapat ditentukan. Dalam Coq, kesetaraan definisi hanya mencakup perhitungan, kesetaraan alfa, pembukaan definisi.
Abhishek Anand