Definieren Sie eine Liste nur mit dem Hindley-Milner-System

Ich arbeite an einem kleinen Lambda-Kalkül-Compiler, der über ein funktionierendes Inferenzsystem vom Typ Hindley-Milner verfügt und jetzt auch rekursive Let's (nicht im verknüpften Code) unterstützt. Ich verstehe, dass dies ausreichen sollte, um Turing vollständig zu machen .

Das Problem ist jetzt, dass ich keine Ahnung habe, wie ich es zu Unterstützungslisten machen soll oder ob es sie bereits unterstützt, und ich muss nur einen Weg finden, sie zu codieren. Ich möchte sie definieren können, ohne dem Typsystem neue Regeln hinzufügen zu müssen.

Der einfachste Weg, wie ich mir eine Liste vorstellen kann, xist etwas, das entweder null(oder die leere Liste) ist, oder ein Paar, das sowohl eine xals auch eine Liste von enthält x. Aber um dies zu tun, muss ich in der Lage sein, Paare und / oder zu definieren, von denen ich glaube, dass sie das Produkt und die Summentypen sind.

Scheint, dass ich Paare folgendermaßen definieren kann:

pair = λabf.fab
first = λp.p(λab.a)
second = λp.p(λab.b)

Da pairder Typ a -> (b -> ((a -> (b -> x)) -> x))nach dem Übergeben von beispielsweise a intund a stringetwas mit Typ ergeben würde (int -> (string -> x)) -> x, wäre dies die Darstellung eines Paares von intund string. Was mich hier stört, ist, dass wenn das ein Paar darstellt, warum das nicht logisch äquivalent ist oder den Satz impliziert int and string? Dies entspricht jedoch (((int and string) -> x) -> x), als ob ich nur Produkttypen als Parameter für Funktionen haben könnte. Diese Antwortscheinen dieses Problem anzusprechen, aber ich habe keine Ahnung, was die von ihm verwendeten Symbole bedeuten. Wenn dies einen Produkttyp nicht wirklich codiert, kann ich dann etwas mit Produkttypen tun, die ich mit meiner obigen Definition von Paaren nicht tun konnte (wenn ich bedenke, dass ich auf die gleiche Weise auch n-Tupel definieren kann)? Wenn nicht, würde dies nicht der Tatsache widersprechen, dass Sie die AFAIK-Konjunktion nicht nur implizit ausdrücken können?

Wie wäre es auch mit dem Summentyp? Kann ich es irgendwie nur mit dem Funktionstyp codieren? Wenn ja, würde dies ausreichen, um Listen zu definieren? Oder gibt es eine andere Möglichkeit, Listen zu definieren, ohne mein Typensystem erweitern zu müssen? Und wenn nicht, welche Änderungen müsste ich vornehmen, um es so einfach wie möglich zu halten?

Bitte denken Sie daran, dass ich ein Computerprogrammierer bin, aber kein Informatiker oder Mathematiker und ziemlich schlecht darin, Mathematiknotation zu lesen.

Bearbeiten: Ich bin nicht sicher, wie der technische Name meiner bisherigen Implementierung lautet, aber alles, was ich habe, ist im Grunde der Code, den ich oben verlinkt habe. Hierbei handelt es sich um einen Algorithmus zur Generierung von Einschränkungen, der die Regeln für Anwendungen, Abstraktionen und Variablen verwendet vom Hinley-Milner-Algorithmus und dann einem Vereinigungsalgorithmus, der den Haupttyp erhält. Beispielsweise gibt der Ausdruck \a.aden Typ aus a -> a, und der Ausdruck \a.(a a)löst einen aufgetretenen Überprüfungsfehler aus. Darüber hinaus gibt es nicht genau eine letRegel, sondern eine Funktion, die den gleichen Effekt zu haben scheint, mit der Sie rekursive globale Funktionen wie diesen Pseudocode definieren können:

GetTypeOfGlobalFunction(term, globalScope, nameOfFunction)
{
    // Here 'globalScope' contains a list of name-value pair where every value is of class 'ClosedType', 
    // meaning their type will be cloned before unified in the unification algorithm so that they can be used polymorphically 
    tempType = new TypeVariable() // Assign a dummy type to `tempType`, say, type 'x'.
    // The next line creates an scope with everything in 'globalScope' plus the 'nameOfFunction = tempType' name-value pair
    tempScope = new Scope(globalScope, nameOfFunction, tempType) 
    type = TypeOfTerm(term, tempScope) // Calculate the type of the term 
    Unify(tempType, type)
    return type
    // After returning, the code outside will create a 'ClosedType' using the returned type and add it to the global scope.
}

Der Code erhält grundsätzlich den Typ des Begriffs wie gewohnt, fügt jedoch vor dem Vereinheitlichen den Namen der Funktion, die mit einem Dummy-Typ definiert wird, in den Typbereich ein, damit er rekursiv aus sich heraus verwendet werden kann.

Bearbeiten 2: Ich habe gerade festgestellt, dass ich auch rekursive Typen benötigen würde, die ich nicht habe, um eine Liste wie gewünscht zu definieren.

Paare

Diese Kodierung ist die kirchliche Kodierung von Paaren. Ähnliche Techniken können Boolesche Werte, Ganzzahlen, Listen und andere Datenstrukturen codieren.

Im Kontext x:a; y:bhat der Begriff pair x yden Typ (a -> b -> t) -> t. Die logische Interpretation dieses Typs ist die folgende Formel (ich verwende mathematische Standardnotationen: ist Implikation, ist oder, ist und, ist Negation; ist Äquivalenz von Formeln): Warum " und oder "? Intuitiv, weil$\to$$\vee$$\wedge$$\neg$$\iff$

pairist ein Konstruktor für den Paartyp und firstund secondsind Destruktoren. (Dies sind die gleichen Wörter, die in der objektorientierten Programmierung verwendet werden. Hier haben die Wörter eine Bedeutung, die mit der logischen Interpretation der Typen und Begriffe zusammenhängt, auf die ich hier nicht eingehen werde.) Intuitiv können Sie mit den Destruktoren auf das zugreifen, was ist im Objekt und die Konstruktoren ebnen dem Destruktor den Weg, indem sie eine Funktion als Argument nehmen, die sie auf die Teile des Objekts anwenden. Dieses Prinzip kann auf andere Typen angewendet werden.

Summen

Die kirchliche Kodierung einer diskriminierten Vereinigung ist im Wesentlichen doppelt so groß wie die kirchliche Kodierung eines Paares. Wenn ein Paar zwei Teile hat, die zusammengefügt werden müssen, und Sie das eine oder das andere extrahieren können, können Sie die Vereinigung auf zwei Arten erstellen. Wenn Sie sie verwenden, müssen Sie beide Möglichkeiten zulassen. Es gibt also zwei Konstruktoren und einen einzigen Destruktor, der zwei Argumente akzeptiert.

let case w = λf. λg. w f g           case : ((a->t) -> (b->t) -> t) -> (a->t) -> (b->t) -> t
  (* or simply let case w = w *)
let left x = λf. λg. f x             left : a -> ((a->t) -> (b->t) -> t)
let right y = λf. λg. g x            right : b -> ((a->t) -> (b->t) -> t)

Lassen Sie mich den Typ (a->t) -> (b->t) -> tals abkürzen SUM(a,b)(t). Dann sind die Typen der Destruktoren und Konstruktoren:

case : SUM(a,b)(t) -> (a->t) -> (b->t) -> t
left : a -> SUM(a,b)(t)
right : b -> SUM(a,b)(t)

Somit

case (left x) f g → f x
case (rightt y) f g → g y

Listen

Wenden Sie für eine Liste erneut dasselbe Prinzip an. Eine Liste, deren Elemente den Typ haben, akann auf zwei Arten erstellt werden: Es kann sich um eine leere Liste oder um ein Element (den Kopf) und eine Liste (den Schwanz) handeln. Im Vergleich zu Paaren gibt es eine kleine Wendung bei den Destruktoren: Sie können nicht zwei separate Destruktoren haben headund tailweil sie nur für nicht leere Listen funktionieren würden. Sie benötigen einen einzelnen Destruktor mit zwei Argumenten, von denen eines eine 0-Argument-Funktion (dh ein Wert) für den Null-Fall und das andere eine 2-Argument-Funktion für den Cons-Fall ist. Funktionen , wie is_empty, headund tailkann sich von dem ableiten. Wie bei Summen ist die Liste direkt eine eigene Destruktorfunktion.

let nil = λn. λc. n
let cons h t = λn. λc. c h t
let is_empty l = l true (λh. λt. false) 
let head l default = l default (λh. λt. h)
let tail l default = l default (λh. λt. t)

Jede dieser Funktionen ist polymorph. Wenn Sie die Typen dieser Funktionen verwenden, werden Sie feststellen, dass dies consnicht einheitlich ist: Der Typ des Ergebnisses stimmt nicht mit dem Typ des Arguments überein. Der Typ des Ergebnisses ist eine Variable - es ist allgemeiner als das Argument. Wenn Sie consAnrufe verketten, werden die aufeinanderfolgenden Aufrufe zum Erstellen einer Liste consbei verschiedenen Typen instanziiert . Dies ist wichtig, damit Listen ohne rekursive Typen funktionieren. Auf diese Weise können Sie heterogene Listen erstellen. Tatsächlich sind die Typen, die Sie ausdrücken können, nicht "Liste von ", sondern "Liste, deren erste Elemente vom Typ ".$T$$T_1,\ldots,T_n$

Wie Sie vermuten, benötigen Sie rekursive Typen, wenn Sie einen Typ definieren möchten, der nur homogene Listen enthält. Warum? Schauen wir uns den Typ einer Liste an. Eine Liste wird als eine Funktion codiert, die zwei Argumente akzeptiert: den Wert, der in leeren Listen zurückgegeben werden soll, und die Funktion, um den Wert zu berechnen, der in einer Cons-Zelle zurückgegeben werden soll. Sei ader Elementtyp, bder Typ der Liste und cder vom Destruktor zurückgegebene Typ. Der Typ einer Liste ist

a -> (a -> b -> c) -> c

Um die Liste homogen zu machen, muss der Schwanz den gleichen Typ wie das Ganze haben, dh es wird die Einschränkung hinzugefügt, wenn es sich um eine Cons-Zelle handelt

a -> (a -> b -> c) -> c = b

Das Hindley-Milner-Typsystem kann mit solchen rekursiven Typen erweitert werden, und tatsächlich tun dies praktische Programmiersprachen. Praktische Programmiersprachen neigen dazu, solche „nackten“ Gleichungen nicht zuzulassen und erfordern einen Datenkonstruktor, aber dies ist keine wesentliche Anforderung der zugrunde liegenden Theorie. Das Erfordernis eines Datenkonstruktors vereinfacht die Typinferenz und vermeidet in der Praxis das Akzeptieren von Funktionen, die tatsächlich fehlerhaft sind, aber zufällig mit einer unbeabsichtigten Einschränkung typisierbar sind, die bei Verwendung der Funktion einen schwer verständlichen Typfehler verursacht. Aus diesem Grund akzeptiert OCaml beispielsweise unbewachte rekursive Typen nur mit der nicht standardmäßigen -rectypesCompileroption. Hier sind die obigen Definitionen in der OCaml-Syntax zusammen mit einer Typdefinition für homogene Listen unter Verwendung der Notation fürrekursive Alias-Typen : Bedeutettype_expression as 'a , dass der Typ type_expressionmit der Variablen vereinheitlicht wird 'a.

# let nil = fun n c -> n;;
val nil : 'a -> 'b -> 'a = <fun>
# let cons h t = fun n c -> c h t;;
val cons : 'a -> 'b -> 'c -> ('a -> 'b -> 'd) -> 'd = <fun>
# let is_empty l = l true (fun h t -> false);;
val is_empty : (bool -> ('a -> 'b -> bool) -> 'c) -> 'c = <fun>
# let head l default = l default (fun h t -> h);;
val head : ('a -> ('b -> 'c -> 'b) -> 'd) -> 'a -> 'd = <fun>
# let tail l default = l default (fun h t -> t);;
val tail : ('a -> ('b -> 'c -> 'c) -> 'd) -> 'a -> 'd = <fun>
# type ('a, 'b, 'c) ulist = 'c -> ('a -> 'b -> 'c) -> 'c;;
type ('a, 'b, 'c) ulist = 'c -> ('a -> 'b -> 'c) -> 'c
# is_empty (cons 1 nil);;
- : bool = false
# head (cons 1 nil) 0;;
- : int = 1
# head (tail (cons 1 (cons 2.0 nil)) nil) 0.;;
- : float = 2.

(* -rectypes is required for what follows *)
# type ('a, 'b, 'c) rlist = 'c -> ('a -> 'b -> 'c) -> 'c as 'b;;
type ('a, 'b, 'c) rlist = 'b constraint 'b = 'c -> ('a -> 'b -> 'c) -> 'c
# let rcons = (cons : 'a -> ('a, 'b, 'c) rlist -> ('a, 'b, 'c) rlist);;
val rcons :
  'a ->
  ('a, 'c -> ('a -> 'b -> 'c) -> 'c as 'b, 'c) rlist -> ('a, 'b, 'c) rlist =
  <fun>
# head (rcons 1 (rcons 2 nil)) 0;;
- : int = 1
# tail (rcons 1 (rcons 2 nil)) nil;;
- : 'a -> (int -> 'a -> 'a) -> 'a as 'a = <fun>
# rcons 1 (rcons 2.0 nil);;
Error: This expression has type
         (float, 'b -> (float -> 'a -> 'b) -> 'b as 'a, 'b) rlist = 'a
       but an expression was expected of type
         (int, 'b -> (int -> 'c -> 'b) -> 'b as 'c, 'b) rlist = 'c

Falten

Wenn man dies etwas allgemeiner betrachtet, welche Funktion repräsentiert die Datenstruktur?

• Für eine natürliche Zahl: wird als die Funktion dargestellt, die ihr Argument mal wiederholt .$n$$n$
• Für ein Paar gilt: als eine Funktion, die ihr Argument auf und anwendet .$(x,y)$$x$$y$
• Für eine Summe: wird als eine Funktion dargestellt, die ihr tes Argument auf anwendet .$\mathrm{in}_i(x)$$i$$x$
• Für eine Liste: wird als eine Funktion dargestellt, die zwei Argumente akzeptiert, den Wert, der für die leere Liste zurückgegeben werden soll, und die Funktion, die auf Nachteile-Zellen angewendet werden soll.$[x_1,\ldots,x_n]$

Im Allgemeinen wird die Datenstruktur als ihre Faltfunktion dargestellt . Dies ist ein allgemeines Konzept für Datenstrukturen: Eine Faltfunktion ist eine Funktion höherer Ordnung, die die Datenstruktur durchläuft. Es gibt einen technischen Sinn, in dem Fold universell ist : Alle „generischen“ Datenstrukturdurchläufe können als Fold ausgedrückt werden. Dass die Datenstruktur als ihre Faltfunktion dargestellt werden kann, zeigt dies: Alles, was Sie über eine Datenstruktur wissen müssen, ist, wie sie durchlaufen wird, der Rest ist ein Implementierungsdetail.

Sie können Summentypen als Produkttypen mit Tags und Werten darstellen. In diesem Fall können wir ein bisschen schummeln und ein Tag verwenden, um Null darzustellen oder nicht, wobei das zweite Tag das Kopf / Schwanz-Paar darstellt.

Wir definieren Boolesche Werte auf die übliche Weise:

true = λi.λe.i
false = λi.λe.e
if = λcond.λthen.λelse.(cond then else)

Eine Liste ist dann ein Paar mit dem ersten Element als Boolescher Wert und dem zweiten Element als Kopf / Schwanz-Paar. Einige grundlegende Listenfunktionen:

isNull = λl.(first l)
null = pair false false     --The second element doesn't matter in this case
cons = λh.λt.(pair true (pair h t ))
head = λl.(fst (snd l))   --This is a partial function
tail = λl.(snd (snd l))   --This is a partial function  

map = λf.λl.(if (isNull l)
                 null 
                 (cons (f (head l)) (map f (tail l) ) )