Apa jenis teori dependen paling intuitif yang bisa saya pelajari?

Saya tertarik untuk mendapatkan pemahaman yang benar-benar solid tentang pengetikan yang tergantung. Saya telah membaca sebagian besar TaPL dan membaca (jika tidak sepenuhnya diserap) 'Jenis Ketergantungan' di ATTaPL . Saya juga membaca dan membaca sekilas banyak artikel tentang pengetikan yang tergantung.

Banyak diskusi tipe teori tampaknya fokus pada penambahan fitur tambahan ke sistem tipe sebelumnya, bukan "apa generalisasi besar berikutnya dari tipe sistem X?". Tipe dependen tampaknya menjadi generalisasi besar berikutnya dari Sistem F, tapi saya belum menemukan bahasa yang diketik secara kanonis dan intuitif. Banyak referensi untuk kalkulus dari konstruksi (induktif) membuat saya berpikir CoC adalah bahasa itu, tetapi penjelasan bahasa yang saya lihat tampaknya tidak begitu jelas atau intuitif bagi saya.

Saya mengharapkan / menebak bahasa seperti itu akan memiliki fitur-fitur seperti: (dan tolong beri tahu saya jika ada sesuatu yang membingungkan atau tidak realistis)

• Abstraksi umum (dapat memiliki fungsi dari domain apa pun dalam hierarki tipe ke yang lain, jenis -> istilah, istilah-> tipe '' 'dll.)
• Memiliki hierarki pengetikan yang tidak terbatas (istilah: jenis: jenis ': jenis' ': ...)
• Jumlah minimum elemen dasar. Saya membayangkan bahwa bahasa hanya menegaskan satu elemen untuk setiap level. Sebagai contoh, ini mungkin menyatakan bahwa ((): Unit: Jenis: Jenis ': ...). Elemen-elemen lain dibangun dari elemen-elemen ini.
• Jumlah dan jenis produk dapat diturunkan.

Saya juga mencari penjelasan bahasa yang idealnya akan dibahas:

• Hubungan antara abstraksi dan kuantifikasi dalam bahasa itu. Jika mereka tidak bersatu, maka jelaskan mengapa mereka tidak bersatu.
• Hirarki tipe tak terbatas secara eksplisit

Saya mengajukan pertanyaan ini karena saya ingin belajar teori tipe dependen tetapi juga karena saya ingin menyusun panduan yang, dengan asumsi latar belakang CS kecil, mengajarkan penggunaan dan bagaimana memahami asisten bukti dan bahasa yang diketik dengan dependen.

(Cross diposting ke Reddit)

Ada beberapa cara berbeda untuk mendekati ini:

1. Teori Tipe Ketergantungan . Ini mungkin bukan cara termudah untuk belajar tentang tipe dependen, tetapi Anda bisa melihat makalah Kalkulus Konstruksi dan variannya, Pure Type Systems, dan artikel Martin Hofmann tentang Sintaks dan Semantik dari Tipe Dependent, misalnya.

2. Teorema membuktikan . Pertama, lihat jawaban saya untuk pertanyaan terkait: Bagaimana saya bisa mempelajari teori yang mendasari asisten bukti Coq? .

3. Pemrograman dengan tipe dependen . Melihat bahasa-bahasa terkini dengan tipe-tipe dependen seperti Epigram atau Agda atau yang kurang mutakhir seperti Dependent ML dan menulis beberapa program akan membantu memperkuat ide. Epigram, misalnya, sangat bersih dalam desain. Sudut lain adalah untuk melihat bagaimana tipe dependen diimplementasikan . Salah satu teori tipe dependen praktis adalah : Jenis Dependen tanpa gula. Beberapa tesis PhD dikhususkan untuk pemrograman dengan teori tipe dependen: Dan Danata , Nils Anders Danielsson , Ulf Norrel , Susmit Sarkar$\Pi\Sigma$, diantara yang lain. Dan tentu saja ada buku Adam Chlipala, yang diberikan dalam jawaban Marc Hamann.

Saya akan cenderung memulai dengan pemrograman, sebelum beralih menggunakan pembuktian teorema, kemudian mulai mengeksplorasi masalah yang lebih teoretis.

The kalkulus -yang pada dasarnya inti dari LF, pada gilirannya pendekatan yang paling banyak reimplemented ke tingkat tinggi logic- adalah jauh paling sederhana sistem ketergantungan diketik Anda bisa belajar, karena terdiri hanya dari perpanjangan dari jenis sistem kalkulus lambda yang diketik secara sederhana dengan penjumlahan yang diketik secara dependen. Jadi intuisi kunci yang diperlukan untuk menguasai LF adalah intuisi yang perlu Anda kuasai dengan teori apa pun dengan tipe dependen.$\lambda\pi$

Twelf adalah sistem pembuktian teorema yang baik berdasarkan LF. Melihat catatan kursus lanjutan yang ditawarkan oleh Frank Pfenning adalah pengantar yang baik untuk teori dan praktik LF.

Yang mengatakan, itu mungkin bukan sistem pertama yang terbaik untuk belajar jika minat Anda lebih pada matematika konstruktif daripada esensi teori tipe: LF berarti kerangka kerja logis dan itu adalah sistem yang digunakan untuk membuat teori aksioma, dan tidak begitu sering bekerja sebagai sistem target secara langsung. Menggunakan sistem yang didasarkan pada teori tipe Martin-Loef mungkin adalah pengantar terbaik -Disebutkan Agda, antara lain- mungkin merupakan titik awal yang lebih baik jika ini adalah tujuan Anda, karena Anda dapat menggunakan aritmatika dan tipe induktif lebih cepat dalam sistem seperti itu. kerangka.

Kemungkinan besar CoC adalah jalan yang harus ditempuh. Hanya menyelam ke Coq dan bekerja melalui tutorial bagus seperti Yayasan Perangkat Lunak (yang Pierce dari TaPL dan ATTaPL terlibat dalam).

Setelah Anda merasakan aspek praktis dari pengetikan dependen, kembali ke sumber teoritis: mereka akan jauh lebih masuk akal.

Daftar fitur Anda pada dasarnya terdengar benar, tetapi melihat bagaimana mereka bermain dalam praktek bernilai seribu poin fitur.

(Lain, sedikit lebih maju tutorial adalah Pemrograman Bersertifikat Adam Chlipala dengan Jenis Ketergantungan )

Saya pikir artikel ini membantu menghilangkan konsep di tingkat dasar: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html

Lihatlah http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf dan sistem PiSigma lama yang disebutkan di sana.