Warum ich keine abhängigen Typen verwende

• Abhängige Typen (type theory) enthalten zwar Beweisobjekte, doch der Autor bewertet sie als unnötige und ineffiziente Struktur
• Der Autor hat frühere auf abhängigen Typen basierende Systeme wie AUTOMATH und Martin-Löf Type Theory direkt untersucht, Isabelle entwickelte sich jedoch zu einem allgemeinen (generic) logischen Framework
• Isabelle/HOL auf Basis der einfachen Typentheorie (higher-order logic) zeigt Stärken bei Automatisierung, großen Bibliotheken und Lesbarkeit
• Das ALEXANDRIA-Projekt zeigte, dass selbst mit höherer Logik allein die Formalisierung fortgeschrittener mathematischer Sätze möglich ist
• Trotz der Reife abhängiger Typsysteme wie Lean bevorzugt der Autor wegen Performance-Problemen und Komplexität weiterhin die praktische Nutzbarkeit des Ansatzes mit höherer Logik

---

Abhängige Typen und Beweisobjekte

• In der Theorie abhängiger Typen sind Beweisobjekte (proof objects) unverzichtbar, doch der Autor betrachtet sie als Platzverschwendung
  • In der LCF-Architektur können gültige Beweisschritte auch allein über Typprüfung auf Ebene der Implementierungssprache statt innerhalb der Logik ausgeführt werden
  • Durch Robin Milners Einsicht wurde das Konzept des proof kernel eingeführt, das zur Grundlage von Isabelle wurde
• Auf die Frage, warum er „keine abhängigen Typen verwendet“ antwortet der Autor: „Ich habe sie lange verwendet“

Erfahrungen mit AUTOMATH

• 1977 hörte der Autor am Caltech Vorlesungen von N. G. de Bruijn über AUTOMATH, konnte das System selbst jedoch nicht direkt benutzen
  • Der Grund war, dass das System der Universität Eindhoven nicht an das ARPAnet angeschlossen war und ein ALGOL-60-basierter Computer benötigt wurde
• AUTOMATH ist zwar ein System mit abhängigen Typen, implementiert aber nicht die Curry–Howard-Korrespondenz
  • Nutzer mussten Symbole und Schlussregeln der gewünschten Logik selbst als Axiome hinzufügen
  • de Bruijn verglich das mit einem „großen Restaurant, das jedes Gericht anbietet“
• Isabelle übernahm diese Idee und verfolgte die Allgemeinheit als logisches Framework
  • de Bruijn jedoch verabscheute Mengenlehre und sah Mathematik im Kern als typbasiert an
• Der Autor fragte nach der Korrektheitsprüfung von AUTOMATH, worauf de Bruijn ihm ein 300-seitiges Buch zur Sprachtheorie schickte, das ihn jedoch nicht zufriedenstellte

Martin-Löf-Typentheorie

• An der Chalmers University in Göteborg untersuchte der Autor die Martin-Löf-Typentheorie und war von der Möglichkeit der Programmsynthese fasziniert
  • Er bewertete sie als klar „richtig“, weil sie die Prinzipien der intuitionistischen Logik von Heyting direkt umsetzte
• Über mehrere Jahre setzte er frühe Versionen von Isabelle in Martin-Löf-Theorie um
  • Das ist bis heute als Isabelle/CTT Teil der Distribution
• Doch eine dogmatische Atmosphäre rund um Per Martin-Löf und der erzwungene Wechsel zu intensional equality ließen diese Forschung scheitern
• Auch später entstandene Systeme wie Calculus of Constructions (CoC), Rocq und Lean ließen dieselben Fragen offen
  • CoC hat über Jahrzehnte hinweg zahlreiche Varianten und optionale Axiome hervorgebracht

Forschungsentscheidungen und die Ausrichtung von Isabelle

• Forschende müssen wählen zwischen der Entwicklung neuer formaler Systeme und der erweiterten Nutzung bestehender Systeme
  • Isabelle wurde als verallgemeinertes Framework entworfen und kann verschiedene Logiken aufnehmen
• 1985 führte Mike Gordon mit Churchs einfacher Typentheorie Hardware-Verifikation durch
  • Später entwickelte John Harrison ein Encoding für Vektordimensionen
• Isabelle/HOL ergänzte Churchs Theorie um axiomatische Type Classes und das Locale-Modulsystem
• Die Lean-Community erreichte auf Basis von CoC mit mathlib eine gewaltige mathematische Formalisierung

Das ALEXANDRIA-Projekt und der Grenztest höherer Logik

• Das ERC-geförderte ALEXANDRIA-Projekt betonte Isabelles Stärken bei Automatisierung, Bibliotheken und Lesbarkeit
• Anfangs wurde erwartet, dass höhere Logik hier an Grenzen stoßen würde, tatsächlich konnten jedoch sogar fortgeschrittene mathematische Themen wie Grothendieck-Schemata erfolgreich formalisiert werden
  • Paulo Emílio de Vilhena und Martin Baillon bewiesen, dass jeder Körper eine algebraisch abgeschlossene Erweiterung besitzt
• Das Projekt wurde auf anspruchsvolle Resultate wie den Satz von Balog–Szemerédi–Gowers ausgeweitet
  • Von der Behauptung „Ohne abhängige Typen ist mathematische Formalisierung unmöglich“ blieb am Ende nur noch die Aussage übrig, „mit abhängigen Typen sei es eleganter“

Lean und die heutige Sicht auf abhängige Typen

• Die Größe der Lean-Community und das Blueprint-Tool sind beneidenswert, doch Performance-Probleme und Komplexität bleiben bestehen
  • Konflikte mit intensional equality und die schwierige Entscheidung, wann abhängige Typen eingesetzt werden sollten, werden immer wieder berichtet
• Der Autor vergleicht abhängige Typen mit Teslas Full Self-Driving und weist auf die überzogenen Erwartungen und den tatsächlichen Mehraufwand hin

Anhang: Theoretische Grenzen höherer Logik

• Manche behaupten, höhere Logik sei beweistheoretisch schwach, doch das bedeutet lediglich, dass sie im Vergleich zur ZF-Mengenlehre schwächer ist
• Laut den ALEXANDRIA-Ergebnissen kann höhere Logik dennoch komplexe mathematische Strukturen wie Grothendieck-Schemata behandeln
  • Nur zwei Beweise benötigten die Hinzunahme von ZF-Axiomen, und dabei handelte es sich um Sätze, die ZF-Objekte direkt erwähnen

Fußnote

• Intuitionismus ist eine philosophische Sichtweise, die Sprache als bloßes Mittel der Aufzeichnung betrachtet, und unterscheidet sich von der heutigen constructive mathematics

[GN⁺]

Hacker-News-Diskussion

• Abhängige Typen (dependent types) sind in bestimmten Situationen sehr nützlich.
  Zum Beispiel fände ich es gut, wenn Python einen „10×5-Float32-Matrix“-Typ ausdrücken und typprüfen könnte.
  Aber Konzepte wie die Curry–Howard-Korrespondenz, die Beweise und Typen gleichsetzt, sind aus menschlicher Sicht verwirrend.
  Ein Typfehler fühlt sich einfach wie ein behebbarer Irrtum an, während ein Beweisfehler ein viel komplexeres Problem ist, das mehr Nachdenken erfordert.
  Deshalb sehe ich die eigentliche Stärke von Lean nicht im Typsystem, sondern in der Community und der Open-Source-Struktur von mathlib.
  Während Isabelles AFP eher wie eine Fachzeitschrift organisiert ist, gibt es bei Lean lebhafte Zusammenarbeit auf Pull-Request-Basis.
  Derzeit entwickle ich den neuen Theorembeweiser Acorn(acornprover.org) und versuche, die Vorzüge von Lean und Isabelle zu verbinden.
  Die einfache Ausdrucksstärke von abhängigen Typen in Lean gefällt mir, aber wenn man sie zu tiefgehend nutzt, wird das Debugging schwierig.

  • Auch in C++ oder Rust ist eine solche Typdarstellung für Arrays mit konstanter Größe möglich.
    Den Bereich von Indizes, die erst zur Laufzeit bekannt sind, kann man damit allerdings nicht zur Compile-Zeit garantieren.
    Eine echte Sprache mit abhängigen Typen kann Laufzeitfehler auf Typebene verhindern.
  • Mit Rusts const generics oder C++-non-type-template-Parametern ist das ebenfalls gut möglich.
    Tatsächlich werden abhängige Typen auch in Sprachen mit echten dependent types nur selten zur Vermeidung von Laufzeitfehlern eingesetzt,
    sondern vor allem für Invarianten von Datenstrukturen oder zur Verifikation nach der Definition eines Programms.
    Dazu: division-by-zero in type theory FAQ, Vortragsfolien von Xavier Leroy
  • Auch in TypeScript kann man abhängige Typen ein Stück weit nachahmen.
    Zum Beispiel kann man wie in diesem Code in Zeile 38 die Matrixgröße im Typ ausdrücken.
    Ich habe auch einen Vektortyp sowie den Ergebnistyp der Matrixmultiplikation implementiert.
    Das ist allerdings eher ein Experiment auf dem Niveau eines privaten Projekts und möglicherweise nicht für große Datenprojekte geeignet.
  • Die Aussage „Ein Beweis ist dasselbe wie ein Typ“ ist interessant.
    Das hängt mit dem Konzept Propositions as Types zusammen.
    Ich frage mich, wie abhängige Typen zur Laufzeit funktionieren und ob man sowohl Compile-Time- als auch Runtime-Typprüfung braucht.
    Bei der Implementierung scheint die Frage naheliegend, ob dadurch nicht zusätzliche Komplexität durch viele indirekte Referenzen entsteht.
  • Wenn man sagt, man wolle in Python einen 10×5-Matrixtyp ausdrücken, heißt das am Ende nicht einfach, dass man dafür selbst eine Klasse definieren sollte?

• Dr. Paulsons Argument ist nicht, dass abhängige Typen schlecht sind, sondern dass sie nicht zwingend erforderlich sind.
  Ich hätte mir mehr Diskussion über die Performance-Probleme von Lean und über intensionale Gleichheit (intensional equality) gewünscht.
  Fälle wie HEq in Isabelle(Link), also wenn keine definitorische Gleichheit vorliegt, verursachen Probleme.
  Deshalb denke ich, dass man abhängige Typen möglichst sparsam einsetzen sollte.
  Auch in Systemen ohne statische Typen wie ACL2 ist Verifikation gut möglich.
  Letztlich geht es um das Gleichgewicht zwischen Praktikabilität und Verifizierbarkeit.

  • Aus Sicht der Softwareverifikation ist Isabelle (ohne abhängige Typen) bereits sehr leistungsfähig.
    Lean oder Agda werden für Verifikation im industriellen Maßstab noch weniger eingesetzt.
    Ein Vergleich zwischen Concrete Semantics(Link) und Logical Verification 2025(Link) ist durchaus interessant.
    In der Praxis könnten Refinement Types nützlicher sein.
    Beispiele: Rust Creusot, Dafny, das leftpad-Beweisbeispiel für LiquidHaskell.
  • In der Mathematik funktionieren abhängige Typen gut, weil man Beweise dort nicht als Programme verwendet.
    Bei der Programmverifikation braucht man jedoch komplexe Hilfslemmata, etwa um zu zeigen, dass zwei Beweise gleich sind, und das ist oft gar nicht beweisbar.
  • Mich würde interessieren, warum man abhängige Typen „so wenig wie möglich“ verwenden sollte.
  • Die Aussage „nicht notwendig“ wirkt wie ein Ausweichen.
    Die entscheidende Frage ist, wie nützlich eine Funktion ist, nicht ob ihre Existenz notwendig ist.
    Am Ende ist die Werkzeugwahl eine Frage von Vorlieben und Effizienz der Entwickler.

• Interessant ist, dass ein großer Teil der modernen Debatten in der Logik letztlich auf ästhetische Vorlieben hinausläuft.
  Wären die praktischen Vorteile überwältigend, gäbe es diese Debatten wohl nicht.
  Lesenswert ist in diesem Zusammenhang Paulsons und Lamports Aufsatz von 1999 „Typing in Specification Languages“.
  Danach entwickelten sich auch Formen von informellem Formalismus wie Lamports TLA+.

  • Ich sehe darin weniger eine rein ästhetische Frage als vielmehr eine Frage von Trade-offs.
    Man gewinnt Garantien zur Compile-Zeit, bezahlt dafür aber mit mehr Komplexität und längeren Build-Zeiten.
    Entscheidend ist letztlich, ob sich dieser Tausch lohnt.

• Das Problem von HOL (simple type theory) ist nicht die Abhängigkeit, sondern zu geringe logische Stärke.
  Es ist äquivalent zu einer eingeschränkten Version der Zermelo-Mengenlehre und zu schwach, um die moderne Mathematik vollständig zu formalisieren.
  Insbesondere ist es schwer, Größenprobleme in Bereichen wie der Kategorientheorie (category theory) zu behandeln.

  • Es gibt ein Beispiel für die Formalisierung von Grothendieck-Schemata mit der Locales-Funktion von Isabelle.
    Ich frage mich, wie stark sich das vom Stil tatsächlicher Mathematiker unterscheidet.
  • Um die logische Stärke zu erhöhen, kann man auch Axiome hinzufügen.
    Fügt man zum Beispiel eine inaccessible cardinal hinzu, ähnelt das dem Universe-Konzept der Typentheorie.

• Ich habe Formal Methods studiert und fand abhängige Typen faszinierend, aber ihr praktischer Einsatz war immer ein harter Kampf.
  Als ich F# verwendet habe, wollte ich F* einführen, aber meinen Kollegen war die mathematische Lernkurve zu abschreckend.
  Am Ende bin ich zu dem zynischen Schluss gekommen, dass Ingenieure Werkzeuge mit viel Mathematik darin nicht gut annehmen.

  • F* ist weniger mathematikzentriert als Lean und stärker auf Softwareverifikation ausgerichtet.
    Es nutzt SMT-basierte Constraint-Solver und ermöglicht dadurch einen leichteren Einsatz abhängiger Typen.
    Auf die philosophische Frage „Ist das wirklich richtig?“ gibt es aber keine Antwort.
    Die Welt mathematischer Beweise und die Welt der Softwareverifikation unterscheiden sich ziemlich stark.
  • Es ist nicht so, dass Menschen nichts Neues lernen wollen, sondern eher, dass sie den Nutzen im Verhältnis zum Aufwand als zu gering einschätzen.
    Zeit ist am Ende begrenzt.

• In unserem Unternehmen Phosphor experimentieren wir damit, abhängige Typen mit Datenbank-/Graph-Abfragen zu kombinieren.
  So konnten wir die Grenzen von RDF ausgleichen und ein logikbasiertes Query-System bauen.
  In der Praxis verwenden wir TypeDB(typedb.com); es ist schneller als MongoDB und nützlich für komplexe Datenmodellierung.
  Das ähnelt auch dem Ontology-Konzept von Palantir.

  • Könntest du die Formulierung „einen nicht verwässernden Wachstumsmechanismus aufbauen“ etwas konkreter erklären?
  • Mich würde interessieren, warum ihr euch für TypeDB entschieden habt und welche konkreten Leistungswerte ihr in der Praxis seht.

• Das Geheimnis abhängiger Typen scheint letztlich darin zu liegen, zu wissen, wann man sie nicht verwenden sollte.
  Statt Lean oder Rocq zu kritisieren, könnte man je nach Situation vielleicht auch im Stil von Isabelle vorgehen.

• Das Formalisierungsprojekt Alexandria(Link) von Paulsons Forschungsgruppe ist beeindruckend.
  Besonders spannend finde ich die Formalisierungsforschung zu Quantencomputing-Algorithmen(Paper-Link).

• Früher dachte ich, abhängige Typen seien die Zukunft, aber in realen Projekten war der Produktivitätsverlust groß.
  Heute bevorzuge ich klarere und leichter wartbare Lösungen.
  Wenn ein Team ein Tool versteht und erweitern kann, dann ist es ein gutes Tool.

• Ich mag eher Typsysteme an der Grenze zu abhängigen Typen als vollständig abhängige Typen.
  Purescript bietet zum Beispiel stärkere Row-Types als Haskell standardmäßig an
  und unterstützt Listen, Strings und reguläre Ausdrücke auf Typebene.
  Das lässt sich als typeclass-basierte Form logischer Programmierung nutzen.