Q ist eine array-orientierte Programmiersprache von Arthur Whitney, die 2003 von KX Systems als Abfrage- und Skriptsprache der Datenbank kdb+ veröffentlicht wurde. Sie ist extrem kompakt, arbeitet auf ganzen Vektoren statt Schleifen und wird vor allem in der Finanzbranche für die Analyse großer Zeitreihen (Tick-Daten) eingesetzt.

Erste Schritte

Q startet man über die kdb+-Konsole q. Ein einfacher Ausdruck wertet sofort aus:

q)sum til 5
10
q)2 * 1 2 3
2 4 6

til n erzeugt die Zahlen 0 bis n-1, sum addiert den ganzen Vektor auf.

Wichtige Befehle und Operatoren

• til n — Liste 0 1 ... n-1 erzeugen
• count x — Länge eines Vektors
• flip t — Tabelle/Matrix transponieren
• group x — Werte nach Schlüssel gruppieren
• distinct x — doppelte Elemente entfernen
• asc/desc — auf-/absteigend sortieren
• first/last — erstes/letztes Element
• sum, avg, max, min — Vektoraggregate

Tabellen und q-SQL

kdb+-Tabellen werden mit einer Liste angelegt, Spalten entstehen durch Zuordnung:

t:([] sym:`IBM`AAPL; price:100 150)
select avg price by sym from t
update price:price * 1.1 from t where sym=`IBM

select, update und delete ähneln SQL, arbeiten aber direkt auf Spaltenvektoren.

Adverbien

Adverbien modifizieren Funktionen: each (') wendet auf jedes Element an, over (/) faltet, scan () liefert alle Zwischenergebnisse.

Q ist ein lesbarer Wrapper um die noch knappere Sprache K und gehört zur APL-Familie — verwandte Einträge: K-Befehle und J-Befehle.

J ist eine array-orientierte Programmiersprache, die Kenneth E. Iverson und Roger Hui Anfang der 1990er-Jahre entwickelten. Sie überträgt die Ideen von APL auf den normalen ASCII-Zeichensatz, ist frei verfügbar (GPL) und gilt als die wichtigste Weiterentwicklung der Iverson-Linie.

Erste Schritte

Die interaktive Konsole heißt jconsole. Funktionen heißen Verben, Modifikatoren Adverbien:

   +/ i.5
10
   2 * 1 2 3
2 4 6

i.5 erzeugt 0 1 2 3 4, +/ ist die Insertion der Addition über den ganzen Vektor.

Wichtige Verben

• i. n — Vektor 0 1 ... n-1
• # y — Anzahl der Elemente
• +/ y — Summe (Insertion)
• % — Division, *: — Quadrat
• >./<. — Maximum/Minimum
• |. y — umkehren (Reverse)
• /:/: — auf-/absteigend sortieren

Tacit Programming

Charakteristisch für J ist die tacite (punktfreie) Notation: Fork (f g h) y bedeutet (f y) g (h y), ein Hook (f g) y bedeutet y f (g y). So entstehen komplexe Funktionen ohne benannte Zwischenwerte:

   mean =: +/ % #
   mean 2 4 6
4

Die kurze Notation stammt aus APL; verwandte Sprachen derselben Familie sind Q und K.

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 anzeigen

Kernkonzepte

• 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 Holes und nutzt die REPL-Interaktion (C-c C-t zum Typ-anzeigen, C-c C-s zum Suchen).

Praxis-Tipps

• data Vect : Nat -> Type -> Type deklariert den abhängigen Vektor-Typ.
• :t und :doc in der REPL zeigen Typen und Dokumentation.
• Die Paketverwaltung läuft über ipkg-Dateien; Bibliotheken wie contrib und network erweitern 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).

Agda ist eine abhängig typisierte, rein funktionale Programmiersprache und zugleich ein Proof Assistant (Beweisassistent). Sie basiert auf der intuitionistischen Typentheorie von Per Martin-Löf. Der Ursprung liegt an der Chalmers University of Technology (Göteborg): Das ursprüngliche System entwickelte Catarina Coquand ab 1999, die heutige Version Agda 2 stammt aus der Dissertation von Ulf Norell (2007). Agda wird in der konstruktiven Mathematik und bei der formalen Verifikation eingesetzt.

Erste Schritte

agda Datei.agda           # Typcheck einer Datei
agda --interactive Datei.agda  # Interaktiver Modus (Emacs)
agda-mode                  # Emacs-Modus starten
c-c c-l                    # Load: Datei laden und prüfen
c-c c-t                    # Goal/Typ anzeigen
c-c c-c                   # Case split: Fallunterscheidung erzeugen
c-c c-a                    # Auto: Beweisversuch suchen (Auto-Suche)
agda --version             # Version anzeigen

Kernkonzepte

• Dependent Types: Typen können von Werten abhängen; man schreibt Programme und Beweise in derselben Sprache (Curry-Howard-Korrespondenz).
• Interaktive Entwicklung: In Emacs entwickelt man Beweise schrittweise mit Goal-Anzeige, Case Splits und Lücken (?).
• Termination Checking: Agda akzeptiert nur terminierende Funktionen und vollständige Pattern-Matches — so bleiben Typen konsistent.
• Universe: Typen leben in Hierarchien (Set, Set₁, Set₂, …), um Paradoxien zu vermeiden.

Praxis-Tipps

• Mit cubical (Cubical Agda) lassen sich höhere induktive Typen und Homotopietypentheorie direkt ausdrücken.
• Bibliotheken wie agda-stdlib liefern fertige Beweise zu Zahlen, Listen und Relationen.
• Beispiel: data Nat : Set where zero : Nat; suc : Nat -> Nat definiert die natürlichen Zahlen induktiv.
• Beweise werden wie Funktionen geschrieben: Der Typ 1 + 1 ≡ 2 ist ein Datentyp, dessen Konstruktor (der Beweis) gesucht wird.

Verwandte Grundlagen: Idris-Befehle, Coq-Befehle, Haskell-Befehle (Agda teilt mit Haskell die syntaktische Tradition).