Deskripsi matematika (kategorikal) dari kelas tipe

14

Bahasa fungsional dapat dilihat sebagai kategori di mana objeknya adalah tipe dan fungsi morfisme di antara mereka.

Bagaimana kelas tipe cocok dengan model ini?

Saya berasumsi bahwa kita hanya harus mempertimbangkan implementasi yang memenuhi batasan yang dimiliki sebagian besar tipe-kelas, tetapi tidak diungkapkan dalam Haskell. Sebagai contoh, kita hanya harus mempertimbangkan implementasi Functoryang fmap id ≡ iddan fmap f . fmap g ≡ fmap (f . g).

Atau apakah ada dasar teoretis lain untuk kelas tipe (misalnya berdasarkan pada kalkulasi lambda yang diketik)?

lo.logic functional-programming ct.category-theory denotational-semantics type-systems Petr Pudlák
sumber
1
Anda mungkin ingin lebih eksplisit tentang model yang Anda inginkan. Jika Anda menginginkan sesuatu yang dapat dengan ketat menggambarkan asumsi dunia terbuka, perilaku resolusi instance, interaksi berbagai ekstensi GHC, & c., Itu agak lebih rumit daripada versi ideal. Demikian pula, perhatikan bahwa pantat sering diabaikan ketika membahas Hask.
CA McCann
4
Tipe kelas dapat dianggap sebagai tanda tangan (dalam arti aljabar universal). Koleksi semua entitas berbagi tanda tangan yang sama (elemen dari kelas tipe yang sama) adalah variasi .
Dave Clarke
1
@DaveClarke: Tidak segera jelas bagi saya bagaimana menjelaskan kelas tipe pada jenis yang lebih tinggi seperti itu, tapi saya tidak terlalu akrab dengan aljabar universal dan mungkin salah paham tentang korespondensi yang ada dalam pikiran ...
CA McCann
1
@camccann: Saya tidak yakin seberapa jauh korespondensi berjalan. Jelas itu tampak seperti titik awal yang baik.
Dave Clarke
2
@camccann: Cukup ubah kategori dasar yang mendefinisi aljabar Anda: kelas tipe dasar seperti num adalah tanda tangan di atas kategori tipe haskell (atau objek dari kategori Hsk), kelas tipe atas konstruktor tipe adalah aljabar di atas kategori functors dari Hask ke Hask. Perhatikan bahwa aljabar universal sepenuhnya dimasukkan oleh gagasan aljabar dalam teori kategori. Juga: Dave: Anda harus mengubah komentar Anda menjadi jawaban.
cody

Jawaban:

18

Bagaimana kelas tipe cocok dengan model ini?

Jawaban singkatnya adalah: tidak.

Setiap kali Anda memperkenalkan paksaan, mengetik kelas, atau mekanisme lain untuk polimorfisme ad-hoc ke dalam bahasa, masalah desain utama yang Anda hadapi adalah koherensi .

Pada dasarnya, Anda perlu memastikan bahwa resolusi typeclass adalah deterministik, sehingga program yang diketik dengan baik memiliki interpretasi tunggal. Misalnya, jika Anda bisa memberikan beberapa instance untuk tipe yang sama dalam cakupan yang sama, Anda berpotensi menulis program ambigu seperti ini:

class Blah a where
   blah : a -> String 

instance Blah T where
   blah _ = "Hello"

instance Blah T where
   blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?

Bergantung pada pilihan contoh yang dibuat oleh kompiler, blah vdapat sama dengan "Hello"atau "Goodbye". Oleh karena itu, arti dari suatu program tidak akan sepenuhnya ditentukan oleh sintaks program, tetapi lebih dapat dipengaruhi oleh pilihan sewenang-wenang yang dibuat oleh kompiler.

Solusi Haskell untuk masalah ini adalah mengharuskan setiap tipe memiliki paling banyak satu instance untuk setiap typeclass. Untuk memastikan hal ini, ia mengizinkan deklarasi instance hanya di tingkat atas, dan selanjutnya membuat semua deklarasi terlihat secara global. Dengan begitu, kompiler selalu dapat memberi sinyal kesalahan jika deklarasi instance ambigu dibuat.

Namun, membuat deklarasi terlihat secara global merusak komposisionalitas semantik. Apa yang dapat Anda lakukan untuk memulihkan adalah memberikan semantik elaborasi untuk bahasa pemrograman - yaitu, Anda dapat menunjukkan cara menerjemahkan program Haskell ke dalam bahasa yang berperilaku lebih baik, lebih komposisional.

Ini sebenarnya memberi Anda cara untuk mengkompilasi kacamata ketik - juga biasanya disebut "terjemahan bukti" atau "transformasi kamus-lewat" di lingkaran Haskell, dan merupakan salah satu tahap awal dari kebanyakan kompiler Haskell.

Typeclasses juga merupakan contoh yang baik tentang bagaimana desain bahasa pemrograman berbeda dari teori tipe murni. Typeclasses adalah fitur bahasa yang benar-benar luar biasa, tetapi mereka cukup berperilaku buruk dari sudut pandang teori bukti. (Inilah sebabnya mengapa Agda tidak memiliki kacamata ketik sama sekali, dan mengapa Coq menjadikannya bagian dari infrastruktur inferensi heuristiknya.)

Neel Krishnaswami
sumber
apa runner up calon yang tidak memiliki semantik denotational iyswim?
Ohad Kammar
1
Saya tidak tahu, sayang.
Neel Krishnaswami
Apakah ini pantas untuk pertanyaan tambahan?
Ohad Kammar
@NeelKrishnaswami: Apakah Anda tahu bagaimana modul ML cocok dengan ini? Dan bagaimana dengan modul Agda (yang seseorang sebutkan kepada saya adalah "kelas satu")?
Lii
1
@ Lii: Modul ML dan catatan Agda jauh lebih baik, tetapi terlalu rumit untuk dijelaskan dalam komentar - ajukan pertanyaan tentang mereka, dan saya (atau orang lain) akan menjelaskan.
Neel Krishnaswami