Teori Domain dan Polimorfisme

Teori domain memberikan teori komputabilitas yang menakjubkan dengan adanya tipe-tipe sederhana. Tetapi ketika polimorfisme parametrik ditambahkan, tampaknya tidak ada teori yang bagus yang menjelaskan apa yang terjadi dengan sebaik teori domain menjelaskan perhitungan dari tipe sederhana. Tentu saja saya tidak akan mengharapkan hal seperti itu ada untuk System-F karena tidak ada model teori set dari System-F ada. Bagaimana dengan pembatasan Sistem-F yang memiliki prediksi dan memiliki hierarki semesta? Apakah ini sudah dipelajari? Apakah ada teori domain bagus yang berlaku untuknya? Lebih jauh bagaimana dengan tipe dependen? Dapatkah teori domain entah bagaimana dicampur dengan yang lemah$\omega$-groupoids untuk mencapai sesuatu?

Ada banyak cara untuk memodelkan polimorfisme melalui teori domain, izinkan saya menjelaskan satu yang mudah dipahami, sehingga Anda dapat memikirkannya sendiri. Ini adalah "model PER".

Ambil model apa pun yang belum diketik $\lambda$-calculus, misalnya domain $D$ seperti yang $D \to D$ adalah penarikan $D$ (misalnya, ambil $D$ seperti yang $D \cong \mathbb{N}_\bot \times (D \to D))$. Membiarkan$\Lambda : D \to (D \to D)$ dan $\Gamma : (D \to D) \to D$ menjadi pencabutan dan bagian, masing-masing.

Kami akan menafsirkan jenis sebagai hubungan ekivalensi parsial (PER) pada $D$. Ingatlah bahwa PER adalah hubungan yang simetris dan transitif, tetapi tidak harus refleksif. Untuk setiap jenis$\tau$ jadi kami menetapkan PER $\sim_\tau$. Pikirkan$x \sim_\tau x$ sebagai "$x$ adalah elemen dari $\tau$"dan $x \sim_\tau y$ sebagai "$x$ dan $y$ sama sejauh $\tau$ prihatin ".

Kita dapat memiliki beberapa tipe dasar (tetapi tidak perlu), misalnya jika kita memastikan itu $\mathbb{N}_\bot$ adalah subdomain dari $D$ melalui penyematan $\iota : \mathbb{N} \to D$ maka kita dapat mendefinisikan $\sim_\mathtt{nat}$ oleh

$$x \sim_\mathtt{nat} y \iff \exists n \in \mathbb{N} . x = \iota(n) = y.$$

PER yang diberikan $\sim_\tau$ dan $\sim_\sigma$, tentukan ruang fungsi PER $\sim_{\tau \to \sigma}$ oleh

$$x \sim_{\tau \to \sigma} y \iff \forall z, w \in D . z \sim_\tau w \Rightarrow \Lambda(x)(z) \sim_\sigma \Lambda(y)(w)$$

Istilah-istilah tersebut ditafsirkan sebagai tidak diketik $\lambda$Istilah -kalkulus sebagai orang biasanya menafsirkannya $D$.

Inilah lucunya. Anda dapat menafsirkan polimorfisme sebagai persimpangan PER, yaitu:

$$x \sim_{\forall X. \tau(X)} y \iff \text{for all PERs $\approx$, $x \sim_{\tau(\approx)} y$}.$$ Kami dapat menghitung PER sesuai dengan $\forall X. X$: ini adalah persimpangan dari semua PER, tetapi itu akan menjadi PER kosong. Menghitung$\forall X . X \to X$adalah latihan yang menarik. Menghitung$\forall X . X \to X \to X$ adalah latihan yang sulit (yang membuat saya sibuk selama seminggu ketika saya masih mahasiswa teori domain).

Jika kita ingin rekursi dalam bahasa kita maka kita perlu memperhitungkan poin tetap. Satu kemungkinan adalah untuk membatasi PER untuk yang mengandung$\bot_D$dan ditutup di bawah suprema rantai yang meningkat. Lebih tepatnya, ambil PERs saja$\approx$ untuk itu

• $\bot_D \approx \bot_D$, dan
• jika $x_0 \leq x_1 \leq x_2 \leq \cdots$ dan $y_0 \leq y_1 \leq y_2 \leq \cdots$ meningkatkan rantai $D$ seperti yang $x_i \approx y_i$ untuk semua $i$, kemudian $\sup_i x_i \approx \sup_i y_i$.

Kita sekarang bisa menafsirkan $\mathtt{fix}_{\tau} : (\tau \to \tau) \to \tau$dengan menerapkan teorema Kanster-Tarski tentang keberadaan titik tetap, seperti yang kita lakukan dalam teori domain biasa. Kali ini,$\forall X . X$ tidak kosong, karena mengandung justru $\bot_D$.

Roy Crole memberikan penjelasan yang bagus tentang bagaimana menggunakan teori domain untuk memodelkan tipe polimorfisme dalam bukunya Kategori untuk Jenis , khususnya di bagian 5.6.