Apakah tipe proposisi? (Apa jenis sebenarnya?)

Saya sudah banyak membaca tentang sistem tipe dan semacamnya dan saya mengerti kira-kira mengapa mereka diperkenalkan (untuk menyelesaikan paradoks Russel). Saya juga memahami kira-kira relevansi praktis mereka dalam bahasa pemrograman dan sistem bukti. Namun, saya tidak sepenuhnya yakin bahwa gagasan intuitif saya tentang apa jenis itu, benar.

Pertanyaan saya adalah, apakah valid untuk mengklaim bahwa jenis adalah proposisi?

Dengan kata lain pernyataan "n adalah bilangan asli" sesuai dengan pernyataan "n memiliki jenis 'bilangan alami'" yang berarti bahwa semua aturan aljabar yang melibatkan bilangan asli berlaku untuk n. (Yaitu dengan kata lain, aturan aljabar adalah pernyataan. Pernyataan yang berlaku untuk bilangan asli juga berlaku untuk n.)

Lalu apakah ini berarti bahwa objek matematika dapat memiliki lebih dari satu jenis?

Selain itu, saya tahu bahwa set tidak sama dengan tipe karena Anda tidak dapat memiliki set semua set. Bisakah saya mengklaim bahwa jika himpunan adalah objek matematika yang mirip dengan angka atau fungsi , tipe adalah semacam objek meta-matematika dan dengan logika yang sama, jenisnya adalah objek meta-meta-matematika? (dalam arti bahwa setiap "meta" menunjukkan tingkat abstraksi yang lebih tinggi ...)

Apakah ini memiliki semacam tautan ke teori kategori?

Peran kunci tipe adalah untuk membagi objek-objek yang diminati ke dalam jagat yang berbeda, daripada mempertimbangkan segala sesuatu yang ada di satu jagat raya. Awalnya, jenis dirancang untuk menghindari paradoks, tetapi seperti yang Anda tahu, mereka memiliki banyak aplikasi lain. Jenis memberi cara untuk mengklasifikasikan atau mengelompokkan objek (lihat entri blog ).

Beberapa bekerja dengan slogan bahwa proposisi adalah tipe , jadi intuisi Anda pasti akan membantu Anda dengan baik, meskipun ada karya seperti Proposisi sebagai [Jenis] oleh Steve Awodey dan Andrej Bauer yang berpendapat sebaliknya, yaitu bahwa setiap jenis memiliki proposisi yang terkait. Perbedaan dibuat karena tipe memiliki konten komputasi, sedangkan proposisi tidak.

Suatu objek dapat memiliki lebih dari satu jenis karena subtyping dan melalui paksaan tipe .

Jenis umumnya diatur dalam hierarki, di mana jenis memainkan peran dari jenis jenis, tapi saya tidak akan sejauh mengatakan bahwa jenis adalah meta-matematika. Semuanya berjalan pada level yang sama - ini terutama terjadi ketika berhadapan dengan tipe dependen .

Ada hubungan yang sangat kuat antara jenis dan teori kategori. Memang, Bob Harper (mengutip Lambek) mengatakan bahwa Logika, Bahasa (di mana jenis berada), dan Kategori membentuk trinitas suci . Mengutip:

Tiga aspek ini memunculkan tiga sekte ibadah: Logika, yang memberi keunggulan pada bukti dan proposisi; Bahasa, yang memberi keunggulan pada program dan tipe; Kategori, yang memberi keunggulan pada pemetaan dan struktur.

Anda harus melihat Korespondensi Curry-Howard untuk melihat hubungan antara Bahasa Logika dan Bahasa Pemrograman (jenisnya adalah proposisi), dan Kategori Tertutup Cartesian , untuk melihat hubungan antara Teori Kategori dengan.