Lambda-Kalkül durch JavaScript, Teil 1

Dieser Artikel wurde ursprünglich auf 47deg.com am 22. Dezember 2020 veröffentlicht.

Das Lambda-Kalkül ist einer der Höhepunkte der Informatik und liegt an der Schnittstelle zwischen Logik, Programmierung und den Grundlagen der Mathematik. In unserem Fall werden wir sie als minimale (funktionale) Programmiersprache betrachten und sehen, wie wir den Rest einer "richtigen" Sprache darauf aufbauen können.

In den meisten Beschreibungen der Lambda-Berechnung wird diese als losgelöst von jeder "echten" Programmiererfahrung dargestellt, mit einem Formalitätsgrad, der der mathematischen Praxis nahe kommt. Glücklicherweise ist das alles andere als wahr! Sie haben wahrscheinlich einen Interpreter der Lambda-Berechnung auf Ihrem Computer: einen beliebigen Interpreter von JavaScript. Sie können entweder die Developer Tools in Ihrem Lieblingsbrowser öffnen oder die Node.js REPL mit node in einem Terminal starten.

> const id = a => a
undefined
> id
[Function: id]
> id(3)
3

Hier sind die Regeln, die Sie und ich befolgen werden, um JavaScript so zu verwenden, wie es das Lambda-Kalkül vorschreibt:

1. Unsere Definitionen dürfen nur anonyme Funktionen, Funktionsaufrufe und Verweise auf Funktionsargumente verwenden;
2. Jede Funktion muss jeweils ein einziges Argument annehmen, variable => body;
3. Funktionen können aus einem einzigen Ausdruck bestehen. In der Praxis können wir keine Anweisungsblöcke mit geschweiften Klammern verwenden, sondern nur ausdrucksähnliche Körper.

Wir können diese harten Anforderungen zu Beginn sogar lockern. Bis wir zum Beispiel Ziffern einführen - die Art und Weise, wie wir Zahlen im Lambda-Kalkül kodieren - verwenden wir die eingebauten Zahlen in Codeblöcken, wie wir es oben getan haben.

Die zweite Bedingung mag einschränkend erscheinen, ist es aber in Wirklichkeit nicht. Angenommen, wir möchten eine Funktion definieren, die zwei Zahlen addiert. Unser erster Impuls könnte sein, sie wie folgt zu definieren:

const add = (x, y) => x + y

Dies widerspricht der oben erwähnten Regel. Der Trick, der als Currying bekannt ist, besteht darin, eine Folge von verschachtelten Funktionen zu erstellen, die jeweils nur ein einziges Argument annehmen:

const add = x => y => x + y

Dies ist nur der erste von vielen Tricks - im guten Sinne des Wortes -, die wir anwenden werden, um unser Ziel zu erreichen, jedes einzelne Stück Programmierung aus diesem sehr kleinen und strengen Satz von Elementen aufzubauen.

Die vielen Formen des Lambda-Kalküls

Die Lambda-Berechnung ist wie Eiscreme: Es gibt sie in verschiedenen Geschmacksrichtungen (die beste ist natürlich Turrón). In diesem Fall bezieht sich jede Geschmacksrichtung auf ein anderes Typsystem, das den Funktionen selbst überlagert ist. In diesem Beitrag sprechen wir über das untypisierte Lambda-Kalkül, also das, bei dem es keine Einschränkung gibt! JavaScript ist dynamisch typisiert, daher ist diese Wahl naheliegend. Der untypisierte Lambda-Kalkül wurde als erstes von seinem Schöpfer Alonzo Church untersucht, weil er sich auf die grundlegenden Aspekte der Berechnung konzentriert: die Definition und den Aufruf von Funktionen.

Die einfachste Art, dem untypisierten Lambda-Kalkül Typen hinzuzufügen, wird als einfach typisierter Lambda-Kalkül (oder STLC) bezeichnet. Jedem Element in der Sprache ist ein einziger Typ zugeordnet.

const add = (x : number) => (y : number) => x + y

STLC greift zu kurz, weil Sie nicht von polymorphen Funktionen sprechen können - mit anderen Worten, Sie müssten für jeden Typ unterschiedliche id Funktionen definieren. Wenn Sie Generics in Java, Kotlin, TypeScript usw. verwendet haben, wissen Sie sicher, wie man das ein für alle Mal macht:

const id: <U>(x: U) => U = x => x

In akademischen Kreisen ist die Erweiterung des Lambda-Kalküls um polymorphe Typen bekannt als System F . Es ist jedoch nicht die einfache Version, die wir hier sehen. Im tatsächlichen System F müssen Sie explizit Typen einführen oder bereitstellen, wie Sie es für andere Parameter tun:

// fake syntax for introducing types
const id = (type U) => (x: U) => x
// fake syntax for applying types
const isStillTrue = id(type bool)(true)

Mehrere Sprachen, von denen Haskell die beliebteste ist, verwenden System F als logischen Kern. GHC - der wichtigste Haskell-Compiler - übersetzt den gesamten vom Programmierer geschriebenen Code in diese sehr explizite Syntax als einen der Schritte in der Kompilierungspipeline.

Angesichts der Tatsache, dass System F zu viele Anmerkungen erfordert, erfanden Hindley, Damas und Milner ein eingeschränkteres, aber praktisches System. Dies war bis vor einigen Jahrzehnten die Grundlage für die Oberflächensprache von Haskell und ML (die Programmiersprache, nicht das Maschinelle Lernen oder das Auto). In HM (wie es gewöhnlich abgekürzt wird) kann jeder Typ abgeleitet werden und erhält den bestmöglichen Typ.

Heutzutage befasst man sich mit abhängigen Typen, die Typen erlauben, die Werte enthalten. In Sprachen mit abhängigen Typen sind Typen in dem Sinne erstklassig, dass sie Argumente sein können und von Funktionen zurückgegeben werden können. Es gibt noch mehr Feinheiten und Unterscheidungen: Die meisten davon sind im sogenannten Lambda-Würfel zusammengefasst.

Bindung mit Konstanten

Nach diesem kurzen Exkurs lassen Sie uns nun wieder mit dem Lambda-Kalkül spielen. Nun, "spielen" ist vielleicht nicht das richtige Wort, wenn man die lästigen Beschränkungen bedenkt, die wir haben. Könnten wir daraus nicht eine richtige Programmiersprache machen? Zum Beispiel eine mit Variablen (natürlich unveränderlich), Konditionalen und Schleifen?

Natürlich können wir das! Wie schon bei den Funktionen mit mehreren Argumenten besteht der Trick darin, das Gewünschte in Form von Lambda-Kalkülen zu kodieren. Wann immer wir etwas in der Form ausdrücken wollen:

const x = something
rest

übersetzen wir ihn wie folgt:

(x => rest) something

Wir erstellen eine Funktion, die ein Argument mit dem richtigen Namen liefert, so dass die Verwendung in rest in Ordnung ist. Die Berechnung für something wird dann ausgeführt und als Wert dieser x übergeben.

Schauen wir uns ein Beispiel an, um die Dinge zu verdeutlichen. Die folgende Funktion berechnet die Norm (oder quadrierte Länge) eines Vektors . Wir haben die Berechnung der einzelnen Quadrate in eine eigene Variable aufgeteilt:

const norm = x => y => {
  const sqX = x * x
  const sqY = y * y
  return sqX + sqY
}

Der "Trick" übersetzt dann einen solchen Code in einen Code, der alle Beschränkungen der Lambda-Kalkulation erfüllt.

const norm = x => y => ( sqX => ( sqY => sqX + sqY ) (y * y) ) (x * x)

Wenn Sie die Node.js REPL öffnen und diese Funktion eingeben, funktioniert alles wie erwartet:

> norm(3)(2)
13
> norm(0)(0)
0

Genug für heute

Wir haben viel gearbeitet, aber leider sind wir noch weit von einer "richtigen" Sprache entfernt: Uns fehlt noch eine Möglichkeit, verschiedene Verzweigungen (Konditionale) zu nehmen und Berechnungen zu wiederholen (mit Schleifen oder Rekursion). Bleiben Sie dran für die nächsten Beiträge!