Idris ist eine rein funktionale Programmiersprache mit abhängigen Typen, entwickelt von Edwin Brady (University of St Andrews). Sie entstand ab etwa 2007 als Fortführung der Ideen von Epigram und Dependent Haskell; die aktuelle Version Idris 2 (seit 2020/2021) basiert auf der Quantitativen Typentheorie (QTT) und ist in sich selbst implementiert. Idris wird genutzt, um Typsicherheit bis in die Semantik von Programmen zu treiben und um Programme formal zu verifizieren.
Erste Schritte
idris2 hello.idr # Datei ausführen (JIT)
idris2 --build hello.ipkg # Projekt bauen (IPKG-Manifest)
idris2 --check hello.idr # Nur Typcheck, keine Ausführung
idris2 --repl # REPL starten
idris2 --package contrib # Zusatzpaket einbinden
idris2 --version # Version anzeigenKernkonzepte
- Abhängige Typen: Typen können von Werten abhängen, z.B. ein Listen-Typ
Vect n a, dessen Länge im Typ steht. Damit lässt sich ausdrücken, dass Funktionen nie auf leere Listen zugreifen. - Quantitative Typentheorie: Jede Variable hat eine Multiplizität (0, 1, unbegrenzt). Multiplizität 0 bedeutet: Der Wert existiert nur zur Compile-Zeit (erased), Multiplizität 1 erlaubt lineare Nutzung für Ressourcen wie Datei-Handles.
- Totality Checking: Der Compiler prüft, ob Funktionen total sind (terminieren und alle Eingaben abdecken) — die Grundlage für verlässliche Beweise.
- Type-Driven Development: Man schreibt zuerst den Typ, entwickelt dann die Implementierung mit
Holesund nutzt die REPL-Interaktion (C-c C-t zum Typ-anzeigen, C-c C-s zum Suchen).
Praxis-Tipps
data Vect : Nat -> Type -> Typedeklariert den abhängigen Vektor-Typ.:tund:docin der REPL zeigen Typen und Dokumentation.- Die Paketverwaltung läuft über
ipkg-Dateien; Bibliotheken wiecontribundnetworkerweitern den Kern. - Für Nebenläufigkeit bringt Idris typsichere Session-Typen mit, die Protokolle wie „erst senden, dann empfangen“ bereits im Typ erzwingen.
Verwandte Grundlagen: Agda-Befehle, Coq-Befehle, Haskell-Befehle (Haskell diente Idris als Vorbild).