Domänentheorie und Polymorphismus

Die Domänentheorie liefert eine erstaunliche Theorie der Berechenbarkeit bei Vorhandensein einfacher Typen. Aber wenn parametrischer Polymorphismus hinzugefügt wird, scheint es keine schöne Theorie zu geben, die erklärt, was ganz so gut vor sich geht, wie die Domänentheorie die Berechnung über einfache Typen erklärt. Sicher würde ich nicht erwarten, dass so etwas für System-F existiert, da es keine satztheoretischen Modelle von System-F gibt. Was ist mit einer Einschränkung von System-F, die prädiktiv ist und eine Universushierarchie hat? Wurde dies untersucht? Gibt es eine nette Domänentheorie, die darauf zutrifft? Was ist mit abhängigen Typen? Kann die Domänentheorie irgendwie mit schwachen Gruppoiden gemischt werden , um etwas zu erreichen?$\omega$

Es gibt viele Möglichkeiten, Polymorphismus über die Domänentheorie zu modellieren. Lassen Sie mich nur eine beschreiben, die leicht zu verstehen ist, damit Sie selbst darüber nachdenken können. Es ist ein "PER-Modell".

Nehmen Sie ein beliebiges Modell des untypisierten Kalküls, zum Beispiel eine Domäne so dass ein Rückzug von (nehmen Sie zum Beispiel so, dass . Sei und der Rückzug bzw. der Abschnitt.D D → D D D D ≅ N ⊥ × ( D → D ) ) Λ : D → ( D → D ) Γ : ( D → D ) → $\lambda$$D$$D \to D$$D$$D$$D \cong \mathbb{N}_\bot \times (D \to D))$$\Lambda : D \to (D \to D)$$\Gamma : (D \to D) \to D$

Wir werden die Typen als partielle Äquivalenzrelationen (PER) auf interpretieren . Denken Sie daran, dass ein PER eine Beziehung ist, die symmetrisch und transitiv ist, aber nicht reflexiv sein muss. Jedem Typ weisen wir daher ein PER . Betrachten als " ein Element ist " und als " und gleich sind , so weit wie betroffen ist ".τ ~ τ x ~ τ x x τ x ~ τ y x y $D$$\tau$$\sim_\tau$$x \sim_\tau x$$x$$\tau$$x \sim_\tau y$$x$$y$$\tau$

Wir können einige Grundtypen haben (müssen es aber nicht), zum Beispiel wenn wir sicherstellen, dass eine Subdomäne von ist , indem wir einbetten, können wir definieren von $\mathbb{N}_\bot$$D$$\iota : \mathbb{N} \to D$$\sim_\mathtt{nat}$

Definieren Sie unter PERs und den Funktionsraum PER durch $\sim_\tau$$\sim_\sigma$ $\sim_{\tau \to \sigma}$

Die Begriffe werden als untypisierte Kalkül-Begriffe interpretiert, wie man sie normalerweise in interpretieren würde .$\lambda$$D$

Hier ist die Pointe. Sie können Polymorphismus als Schnittpunkt von PERs interpretieren, dh: Wir können das PER berechnen, das : Es ist der Schnittpunkt aller PERs, aber das wird das leere PER sein. berechnen ist eine interessante Übung. berechnen ist eine schwierige Übung (die mich eine Woche lang beschäftigt hat, als ich Student der Domänentheorie war).∀ X . X ∀ X . X → X ∀ X . X → X →

Wenn wir eine Rekursion in unserer Sprache wünschen, müssen wir Fixpunkte berücksichtigen. Eine Möglichkeit besteht darin, PERs auf diejenigen zu beschränken, die enthalten und unter dem zunehmender Ketten geschlossen sind. Genauer gesagt, nehmen Sie nur die PERs für die$\bot_D$$\approx$

• $\bot_D \approx \bot_D$ und
• Wenn und die Ketten in so erhöhen, dass für alle , dann .$x_0 \leq x_1 \leq x_2 \leq \cdots$$y_0 \leq y_1 \leq y_2 \leq \cdots$$D$$x_i \approx y_i$$i$$\sup_i x_i \approx \sup_i y_i$

Wir können nun interpretieren, indem wir den Kanster-Tarski-Satz über die Existenz von Fixpunkten anwenden, genau wie wir es in der gewöhnlichen Domänentheorie tun. Diesmal ist nicht leer, da es genau enthält .$\mathtt{fix}_{\tau} : (\tau \to \tau) \to \tau$$\forall X . X$$\bot_D$

Roy Crole gibt in seinem Buch Categories for Types , insbesondere in Abschnitt 5.6, eine schöne Erklärung zur Verwendung der Domänentheorie zur Modellierung des Typpolymorphismus .