Begriff
Idris
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Agda und Coq sind akademisch. Idris will Dependent Types für die Praxis. Edwin Brady (der Erfinder) sagt: "Pac-Man ist vollständig, wenn es alle Level hat." Idris soll echte Software schreiben (Webserver, Spiele, Protokolle), aber mit der Sicherheit von Dependent Types. Es kompiliert zu C (via Chez Scheme) und ist schnell. Es hat Features wie "Linear Types" (für Ressourcen-Management, ähnlich wie Rust Ownership).
Merksatz: Eine general-purpose funktionale Programmiersprache mit abhängigen Typen, die darauf ausgelegt ist, Typ-getriebene Entwicklung (Type-Driven Development) in die Praxisnahe Softwareentwicklung zu bringen.
Das Buch "Type-Driven Development with Idris" ist legendär.
Du definierst erst den Typ.
StringOrInt : Bool -> Type.
StringOrInt True = Int.
StringOrInt False = String.
Eine Funktion, deren Rückgabetyp vom Input abhängt!
getStringOrInt : (x : Bool) -> StringOrInt x.
1. Quantity Interfance (Multilicity)
In Idris 2 haben Variablen eine "Menge" (0, 1, Many).
0: Wird nur zur Compile-Zeit gebraucht (Erasure). Kostenlos zur Laufzeit.1: Muss genau einmal benutzt werden (Linear Type). Damit kann man State-Machines sicher machen: "Der Socket muss genau einmal geschlossen werden."
2. Elaboration
Wie Agda nutzt Idris "Holes". Du schreibst den Typ, drückst einen Knopf, und Idris schreibt den Code. Da der Typ so präzise ist, gibt es oft nur eine mögliche Implementierung. Der Computer programmiert sich selbst.
1. Elaborator Reflection
In Idris kannst du zur Compile-Zeit auf den Elaborator (den Teil des Compilers, der Löcher füllt) zugreifen.
Mit %runElab kannst du Skripte schreiben, die deinen eigenen Code analysieren und vervollständigen.
Beispiel: "Generiere mir automatisch eine JSON-Serialisierung für diesen Datentyp, aber stelle sicher, dass sie dem Schema X entspricht."
Das ist Metaprogrammierung auf einem Level, das weit über C++ Templates oder Java Annotations hinausgeht, da das Skript vollen Zugriff auf die logischen Beweise des Typsystems hat.
2. Totality Checking & Productivity
Ein Feature, das Idris von Haskell unterscheidet: Der Totality Checker. Idris versucht zu beweisen, dass eine Funktion für alle möglichen Inputs ein Ergebnis liefert und niemals in eine Endlosschleife gerät. Für unendliche Datenströme (wie einen Webserver) nutzt Idris Productivity: Eine Funktion muss zwar nicht anhalten, aber sie muss garantieren, dass sie "nach endlicher Zeit das nächste Stück Daten liefert". Wenn der Checker "Total" sagt, ist die Software mathematisch beweisbar frei von Abstürzen durch unendliche Rekursion – ein riesiger Vorteil für Hochverfügbarkeitssysteme.
3. Quantitative Type Theory (QTT)
In Idris 2 ist jede Variable mit einer "Usage" markiert.
Dies basiert auf der Quantitative Type Theory von Conor McBride.
Interessant für die Produktion: Variablen mit Usage 0 existieren zur Laufzeit schlichtweg nicht. Sie werden vom Compiler gelöscht (Erasure).
Das erlaubt es, extrem komplexe logische Beweise und Metadaten in den Code zu schreiben, um die Sicherheit zu garantieren, ohne dass das fertige Programm auch nur ein Byte größer oder eine Nanosekunde langsamer wird. Sicherheit ohne Performance-Verlust ist das Kernversprechen von Idris.
Quick-Check
Besser als Rust?
Mächtigeres Typ-System. Aber Rust hat das bessere Ökosystem und Tooling. Idris ist noch Nische.Pac-Man?
Edwin Brady nutzt Pac-Man immer als Beispiel, um zu zeigen, dass man auch Spiele verifizieren kann ("Geister können nicht durch Wände gehen").Ernsthafte Nutzung?
Wird langsam mehr. Vor allem in sicherheitskritischen Bereichen, wo C zu gefährlich und Java zu langsam/unsicher ist.