Apakah Tipe Diri membuat Kalkulus Konstruksi Induktif menjadi usang?

10

Self Type adalah perpanjangan dari Calculus of Constructions [1] yang memungkinkan bahasa untuk mengekspresikan tipe data aljabar yang dikodekan melalui Scott Encoding. Scott Encoding memberikan satu kemampuan untuk mencocokkan pola O(1), yang merupakan salah satu motivator utama untuk dimasukkannya definisi induktif pada CC. Namun, Tipe Diri membuat teori dasar yang jauh lebih sederhana dan elegan, dan tampaknya tidak kalah kuat.

Apakah Tipe Diri, berdasarkan sudut pandang teoretis, membuat CIC usang, atau apakah masih ada beberapa aspek yang menguntungkan CIC dalam kaitannya dengan Self Tyes?

[1] http://staff.computing.dundee.ac.uk/pengfu/document/talks/mvd-2012.pdf

lambda-calculus type-theory functional-programming inductive-datatypes Viktor Maia
sumber
2
Mungkin saya kehilangan sesuatu tetapi mengapa tipe diri tidak hanya tipe rekursif umum (mis. Tidak sehat?) Ini bukan tujuan untuk semua hal yang diketik secara dependen tetapi tentu impor ke CiC menjadi sehat. Presentasi yang ditautkan memiliki tipe juga, tapi saya rasa itu tidak berhubungan / perlu.
Daniel Gratzer
@jozefg Memang: "Akan menjadi inkonsistensi sebagai logika, tetapi tidak ada masalah untuk program." Anda harus memposting ini sebagai jawaban.
Gilles 'SANGAT berhenti menjadi jahat'
Bukankah itu ditujukan untuk komentar * : *, @GIlles, bukan untuk Self?
MaiaVictor
@ srvm dengan aturan mengetik yang mereka tulis, keduanya merupakan sumber ketidakberesan. Apakah Anda memiliki tautan ke koran?
Daniel Gratzer
@ jozefg Saya kira ini yang ini: staff.computing.dundee.ac.uk/pengfu/document/papers/…
gallais

Jawaban:

5

Saya bukan ahli dalam pekerjaan ini, tetapi bagi saya tampaknya masalah utama saat ini adalah kurangnya bukti SN, bahkan dengan pembatasan. Bukti-bukti ini terkenal rumit, bahkan ketika kalkulusnya benar, jadi saya akan memberikan sedikit waktu. Pekerjaannya tentu sangat menjanjikan.

Satu hal yang perlu diperhatikan adalah bahwa pembatasan ini sebenarnya cukup non-sepele untuk diungkapkan, yang merupakan bagian besar dari kerumitan perumusan keluarga induktif di CIC. Titik penjualan nyata dari pendekatan seperti ini adalah merumuskan kondisi ini secara ringkas.

Sudah merupakan masalah terbuka yang agak lama untuk memiliki bahasa yang diketik secara dependen

  • Konsisten / Normalisasi
  • Dapat mengekspresikan semua tipe keluarga dari Coq (atau bahkan Agda)
  • Memungkinkan ekspresi rekursi sederhana atas keluarga-keluarga ini
  • Sederhana atau memiliki sejumlah kecil konstruksi inti ( ).Π,Σ,μ

Salah satu upaya yang saya ketahui adalah bahasa Altenkirch & al , yang juga tidak memiliki studi meta-teoretis lengkap (dan juga tidak konsisten tanpa batasan lebih lanjut).ΠΣ

cody
sumber