Lambda-Kalkül durch JavaScript, Teil 4

Dieser Artikel wurde ursprünglich auf 47deg.com am 28. Januar 2021 veröffentlicht.

Dies ist der vierte Beitrag in der Serie Lambda Calculus Through JavaScript. Wenn Sie gerade erst einsteigen, sollten Sie noch einmal zurückgehen und mit Lambda Calculus durch JavaScript, Teil 1, beginnen.

Wir haben die Lehrlingsphase des Lambda-Kalküls definitiv hinter uns gelassen: Wir kennen die Regeln der Sprache, wissen, wie man Boolesche Operatoren und Zahlen kodiert, und haben ein Gefühl dafür, wie wir mit Fixpunkten Rekursionen kodieren können. Aber niemand schreibt ein Programm nur mit Booleschen Werten und Zahlen (es sei denn, Sie sind eine Turing-Maschine oder ein Low-Level-C-Programmierer); neue Datentypen zu definieren ist ein Muss. Wie üblich werden wir feststellen, dass das Lambda-Kalkül uns die Zutaten liefert, um dieses Konzept einzuführen, ohne die Sprache zu erweitern, einfach durch Übersetzung.

Umklappen von Listen und Bäumen

Keine Einführung in die funktionale Programmierung ist vollständig ohne eine Diskussion über das Reduzieren oder Falten über Listen oder Arrays. In JavaScript nimmt diese Operation die folgende Form an: Sie geben ihr eine Möglichkeit, den Akkumulator mit dem aktuellen Wert zu kombinieren, der gerade verarbeitet wird, und (optional) einen Wert, um die Operation zu starten.

arr.reduce((acc, current) => do something, initialValue)

Diese Operation ist ein Baustein für den Rest der Funktionalität in diesem Stil. Mit reduce können Sie map, filter, concat, ... im Allgemeinen jede beliebige Funktion über Arrays definieren.

Es besteht eine enge Verbindung zwischen der Funktion reduce und der üblichen Definition von Listen in den meisten funktionalen Programmiersprachen. In der ReScript-Syntax werden Listen so definiert, dass Sie bei jedem Schritt die Wahl haben zwischen dem Beenden der Liste (mit ) oder dem Hinzufügen eines neuen Elements am Kopf einer anderen Liste (mit ). Die 'a ist die Syntax von ReScript (und OCaml) für ein generisches Argument.

type rec list<'a> =
  | Cons({ hd: a, tl: list<'a> })
  | Nil

Hier ist der Typ der entsprechenden reduce Funktion - nun, ich habe die Reihenfolge einiger Argumente geändert, um der JavaScript-Version zu entsprechen:

let reduce: (list<'a>, ('b, 'a) => 'b, 'b) => 'b

Der Link funktioniert folgendermaßen: Um die reduce Funktion haben wir die Typen der Argumente für jeden Konstruktor genommen - a und list<'a> im ersten Fall, keine im zweiten -; ersetzt alle rekursiven Komponenten durch 'b - nur im Cons Fall in diesem Fall -; und fragen Sie schließlich nach einer Funktion über jedes Argument, die 'b - im Falle von Nilbedeutet das Fehlen von Argumenten, dass diese Funktion einfach ein Wert ist.

Sie können dieses Spiel mit jedem Datentyp spielen, den Sie in dieser Form definieren (normalerweise algebraische Datentypen genannt). Hier ist zum Beispiel ein Typ für binäre Bäume:

type rec tree<'a> =
  | Node({ value: a, left: tree<'a>, right: tree<'a> })
  | Lead({ value: a })

Wenn Sie denselben Algorithmus ausführen, erhalten Sie den folgenden Typ für eine Faltung über Bäume. Wenn Sie sich mutig fühlen, versuchen Sie, die Funktion selbst zu definieren ;)

let reduceTree(tree<'a>, ('a, 'b, 'b) => 'b, ('a) => 'b) => 'b

Faltung über Boolesche Werte

Was wäre, wenn wir dieses Verfahren auf Typen anwenden würden, die wir bereits besprochen haben, wie z.B. Booleans? Zunächst einmal benötigen wir die Definition des Typs als algebraischen Datentyp. Glücklicherweise machen die meisten funktionalen Sprachen dies auf ähnliche Weise:

type boolean =
  | True
  | False

Da keiner der Konstruktoren Argumente hat, ist der entsprechende Typ der Falte wie folgt.

let reduceBoolean(boolean, 'b, 'b) => 'b

Wenn Ihnen der Typ allein nichts sagt, möchte ich Ihnen ein Beispiel dafür geben, wie Sie diese Funktion verwenden, um die Negation eines booleschen Wertes zu definieren.

let not = (b) => reduceBoolean(b, False, True)

Dies ist genau die gleiche Art und Weise, wie wir if_ in Teil 2 verwendet haben!

Daten und Falten austauschen

Zeit für den Zaubertrick Es stellt sich heraus, dass wir auf die gleiche Weise, wie wir boolesche Werte durch Funktionen ersetzt haben, dasselbe mit jedem Datentyp tun können. Der Kerngedanke ist, dass wir die Daten durch ihre Faltung darstellen. Das oben beschriebene Verfahren zur Ermittlung des Typs der Falte ist hier immer noch relevant, um uns die Form der Funktion mitzuteilen.

Konkreter: Lassen Sie uns herausfinden, wie wir Listen auf diese Weise darstellen. Sie erinnern sich, dass wir gesagt haben, dass Listen durch Funktionen mit dem Typ dargestellt werden. Da ich mich nicht auf eine Diskussion darüber einlassen möchte, wie man diese Funktion tatsächlich tippen kann - denn wir brauchen etwas, das man höherrangige Typen nennt, weil 'b auf der rechten Seite erscheint, aber nicht auf der linken -, werde ich das Gleichheitszeichen einfach auf einer intuitiven Ebene belassen.

type list<'a> "=" (('b, 'a) => 'b, 'b) => 'b

Wie oben beschrieben, wird jede Liste aus Nil und Cons konstruiert. Mit anderen Worten: Wenn wir beschreiben, wie wir diese beiden Konstruktoren als Fold kodieren, können wir jede beliebige Liste darstellen. Wenn wir auf anwenden, ist das Ergebnis das zweite Argument, das ihm gegeben wird, nämlich . Das sollte dann das Verhalten von Nil sein, das als Fold dargestellt wird:

const nil_ = (callback) => (initialValue) => initialValue

Noch einmal: Dies ist unsere Definition von leeren Listen im Lambda-Kalkül.

Der Cons Konstruktor nimmt zwei Argumente entgegen und gibt dann eine Liste/Falte zurück. Das bedeutet, dass das Skelett der Funktion sein sollte:

const cons_ = hd => tl =>
                callback => initialValue => ???

Das Ergebnis der Reduzierung einer Liste mit mehr als einem Element ist dasselbe wie die Anwendung von callback auf den aktuellen Wert - also einfach hd - und die rekursive Anwendung von reduce auf den Rest. Wenn wir unseren "eine Liste ist eine Falte"-Hut aufsetzen, ist dieser letzte Teil einfach die Anwendung von tl auf die Argumente.

const cons_ = hd => tl =>
                callback => initialValue =>
                  callback(hd, tl(callback, initialValue))

Der letzte Teil des Tricks besteht darin, dass jetzt keine Notwendigkeit besteht, reduce zu definieren, da die Listen selbst die Falte sind. Wenn wir reduce schreiben würden, kämen wir in eine sehr ähnliche Situation wie bei der Definition von if_: Es ist einfach die Anwendung des ersten Arguments auf den Rest!

const reduce = list => callback => initialValue => list(callback, initialValue)

Dies ist ein alter Trick

Diese Darstellung ist als Church-Kodierung bekannt, da sie als Verallgemeinerung der Art und Weise entstanden ist, wie Alonzo Church in seiner Arbeit Booleans dargestellt hat. Dies ist jedoch nicht die einzige Möglichkeit, Datentypen darzustellen, es gibt auch andere Möglichkeiten:

• Die Scott-Kodierung ersetzt Datentypen nicht durch ihre Faltungsfunktionen, sondern durch ihre Mustervergleichsfunktion. Im Fall von list bedeutet das, dass die rekursive Anwendung des Rückrufs nicht dargestellt wird; Sie erhalten einfach Werte zurück, die den Kopf und das Ende darstellen.
• Mit der Boehm-Berarducci-Codierung wurde die Church-Codierung in den typisierten Lambda-Kalkül eingeführt. Wie oben beschrieben, erfordert die Typisierung von Church-Kodierungen einige fortgeschrittene Techniken, die wir jedoch umgehen können, da wir in einer nicht typisierten Umgebung arbeiten.

Beachten Sie, dass die drei Techniken in der Regel einfach als Church-Kodierungen bezeichnet werden.

Darstellung von Paaren

Als letzte Übung für den Leser: Was ist die Church-Kodierung eines Paares? Zur Erinnerung: Wir können die Typen von Paaren wie folgt definieren. Beachten Sie, dass dies nicht ganz idiomatisch ist (warum sollten Sie einen Konstruktor für nur eine Auswahl einführen?), aber die ganze Idee zusammenhält.

type pair<'x, 'y> =
  | Pair({ left: 'x, right: 'y })

Lösung: Wir haben einen Konstruktor, so dass die Form der entsprechenden Reduktionsfunktion nur ein funktionales Argument benötigt. Es gibt kein rekursives Auftreten von tuple, so dass wir keine Substitution vornehmen müssen. Das Ergebnis ist der folgende Typ:

let reducePair(tuple<'x, 'y>, ('x, 'y) => 'b) => 'b

Schließlich stellen wir den Konstruktor dar. Dieser hat zwei Argumente, die beiden Komponenten des Paares. Und es gibt nur eine Sache, die wir tun können: die entsprechende Callback-Funktion anwenden.

const pair_ = l => r => callback => callback(l, r)

Wenn Sie glauben, dass Sie keine Paare haben, aber Funktionen höherer Ordnung haben, dann haben Sie tatsächlich Paare!

Genug für heute

Endlich haben wir eine Sprache, die wir eine richtige Programmiersprache nennen können. Bedingungen, Rekursion und Datentypen sind in Kombination mit den primitiven Funktionen die grundlegenden Werkzeuge der funktionalen Programmierung.