Agda

Agda
Basisdaten
Paradigmen:	funktional
Erscheinungsjahr:	2007
Designer:	Catarina Coquand und Makoto Takeyama (Agda 1), Ulf Norell (Agda 2)
Entwickler:	Andreas Abel, Guillaume Allais, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Nils Anders Danielsson, Amélia Liao, Ulf Norell
Aktuelle Version:	2.8.0  (2025-07-05)
Aktuelle Vorabversion:	2.9.0  ()
Typisierung:	statisch, stark, Typinferenz, term-abhängig (engl. dependent)
Beeinflusst von:	Haskell
Betriebssystem:	plattformübergreifend
Lizenz:	Agda Lizenz
https://wiki.portal.chalmers.se/agda/Main/HomePage

Agda ist eine funktionale Programmiersprache, die sich durch ihr Typsystem auch als Beweisassistent eignet. Das Wort „funktional“ bezieht sich hier auf die Verwendung von Funktionen als Objekte, die nicht nur definiert und aufgerufen werden, sondern auch als Variablen übergeben und als Wert zurückgegeben werden können. Es ist eine sog. totale Sprache, in der alle Funktionen terminieren und einen Wert des Ergebnistyps zurückgeben. Diese Eigenschaft ist notwendig, damit die Beweise, die man in Agda formuliert, stichhaltig sind. Das Typsystem basiert auf Arbeiten von Per Martin-Löf und kann über die Curry-Howard-Korrespondenz zur Formulierung logischer Aussagen genutzt werden. Dazu ist es notwendig, dass die Typen in Agda auch von Werten abhängen können (engl. dependently typed).

In Agda kann man einerseits klassische Programme schreiben, die zuerst in Haskell und über den Glasgow-Haskell-Compiler in eine ausführbare Datei übersetzt werden. Andererseits – und das ist eher die Regel – kann man auch Programme schreiben, bei denen der Typprüfer sämtliche zur Übersetzungszeit vorliegenden Informationen nutzt, um bestimmte Berechnungen durchzuführen. Das Programm braucht nicht in eine ausführbare Datei übersetzt zu werden und benötigt dementsprechend keinen Einsprungpunkt (main-Funktion).

Weiterhin kann man in Agda mit einem leeren Quelltext beginnen und von Grund auf eigene Typen und Funktionen definieren, ohne dass man eine Standardbibliothek für Basisfunktionen nutzen muss. Es sind dann auch keine impliziten Typ- oder Funktionsdefinitionen vorhanden (außer der Set-Hierarchie). Es gibt jedoch eine Standardbibliothek, die derzeit (Stand 2025) aktiv weiterentwickelt wird.

Der Quelltext in Agda kann an bestimmten Stellen Lücken (eingegeben durch ein ?) enthalten. Diese verhindern zwar die Erstellung eines ausführbaren Programms, gelten aber nicht als Fehler während der Kompilierung. Vielmehr meldet der Compiler, welchen Typ er an der entsprechenden Stelle erwartet. Dies wird üblicherweise als Ziel (engl. Goal) bezeichnet. Ist der Typ so weit eingeschränkt, dass der Compiler bestimmen kann, welcher Wert eingesetzt werden muss, kann dieser den fehlenden Wert automatisch einsetzen.

Agda wird normalerweise über Plug-ins in Emacs, Vim oder Visual Studio Code bedient. Hier werden bestimmte Tastenkombinationen genutzt, um den Quelltext auf Typ-Korrektheit zu prüfen, die Typziele der Lücken abzufragen, automatische Einsetzungen vorzunehmen, Typen abzufragen oder auch den vom Compiler berechneten Wert einer Variable zu ermitteln. Ist der Quelltext typkorrekt, dann wird er auch entsprechend der Syntax eingefärbt. Dies ist eine andere Reihenfolge als bei Programmiersprachen, bei denen die integrierte Entwicklungsumgebung den Quelltext zuerst einfärbt (und eventuelle Syntaxfehler aufzeigt) und später bei der Kompilierung nachträglich noch Typfehler aufdeckt.

Die Syntax von Agda basiert auf der Verwendung von Leerzeichen zur Trennung von Syntaxelementen oder zur Einrückung. Bezeichner können (fast) beliebige Unicode-Zeichen enthalten. Zum Beispiel ist 1≤2 (ohne Leerzeichen) ein gültiger Bezeichner, während 1 ≤ 2 (mit Leerzeichen) einen Ausdruck darstellt. Funktionen werden mit Hilfe von Pattern Matching definiert.

Es ist möglich und vorgesehen, dass man Agda-Quelltexte auch direkt in Dokumenten und Artikeln (engl. literate programming) verwendet. Die Quelltexte haben dann nicht mehr die Endung .agda, sondern z. B. .lagda.md für Markdown-Text oder .lagda.tex für LaTeX-Dokumente. Der Quelltext wird in entsprechende Blöcke im Dokument eingefasst.

Agda ist auf verschiedenen Plattformen verfügbar und kann mittels des Cabal-Paketsystems von Haskell installiert werden. Für die Benutzung ohne Installation steht das Onlinetool Agdapad zur Verfügung.

Compilerdialog und Programme ohne Einsprungpunkt

Ein sehr einfaches Agda-Programm, das einen Daten-Typ Bool definiert und das logische UND implementiert, könnte wie folgt aussehen:

module wiki-simple where -- jede Quelldatei ist ein Modul

data Bool : Set where -- Bool ist ein:
  true  : Bool        -- entweder "true"
  false : Bool        -- oder "false"

_∧_ : Bool → Bool → Bool  -- logisch-UND ist eine Funktion, die zwei Bool-Argumente benötigt und einen Bool zurückgibt
true  ∧ b = b             -- 1. Fall: 1. Argument = true, 2. Argument beliebig: Rückgabe = 2. Argument.
false ∧ b = false         -- 2. Fall: 1. Argument = false, 2. Argument beliebig: Rückgabe = false

x : Bool  -- x ist vom Typ Bool
x = true  -- x ist "true"

y : Bool  -- y ist vom Typ Bool
y = false -- y ist "false"

z : Bool  -- z ist vom Typ Bool
z = x ∧ y -- z ist x UND y; C-n z (normalisieren von z) ergibt false

Hierzu einige Bemerkungen:

• data ist notwendig, damit man mit einem leeren Quelltext starten kann. Es ist die Basis dafür, dass man „alles“ selbst implementieren kann.
• In Agda wird durch den Doppelpunkt : ein Typurteil gekennzeichnet. Man sieht, dass Bool den Typ Set hat. Das bedeutet so viel wie, dass Bool ein „kleiner“ Typ ist. Set (ist implizit Set 0) selbst hat den Typ Set 1. Somit wird eine unendliche Hierarchie an Typen aufgebaut. Dies vermeidet z. B. die Russellsche Antinomie.
• true und false nennt man (Daten)konstruktoren.
• Das logische UND wird durch _∧_ repräsentiert. Die zwei Unterstriche weisen ∧ als Infix-Funktion aus.
• Der Pfeil _→_ repräsentiert einen Funktionstyp. Verkettete Pfeile sind eine andere Schreibweise für Funktionen mit mehreren Eingaben. Der Pfeil ist rechtsassoziativ, d. h., Bool → Bool → Bool bedeutet eigentlich Bool → (Bool → Bool). Wenn man also das linke Argument in _∧_ einsetzt, erhält man eine Funktion, die einen Bool braucht (das rechte Argument) und daraus einen Bool macht. Siehe hierzu Currying oder Schönfinkeln.
• Die Definitionen von _∧_ decken alle Fälle ab, dafür sorgt der Typprüfer. Er prüft auch, ob die Funktion terminiert.
• Die Vorgaben von x und y zur Typprüfungszeit ermöglichen es, z bei der Typprüfung auszurechnen. Daher kann man z nach der Typprüfung abfragen.
• Ein Einsprungpunkt main ist in diesem Beispiel nicht vorhanden.

Definiert man nun eine Funktion für das logische ODER, sieht das so aus:

_∨_ : Bool → Bool → Bool  -- logisch-ODER ist eine Funktion, die zwei Bools als Argumente braucht und einen Bool zurückgibt
a ∨ b = {!!}              -- Definition mit Lücke

Die Lücke wird nach der Typprüfung mit { }0 bezeichnet und im Meldungsfenster wird

?0 : Bool

gezeigt. Das ist ein Hinweis darauf, dass noch Lücken existieren, die geschlossen werden müssen. Man kann die Ziele noch detaillierter anzeigen lassen. Die Ziel-Ansicht der Lücke { }0 zeigt

Goal: Bool
————————————————————————————————————————————————————————————
b : Bool
a : Bool

Dies besagt, dass hier ein Bool erwartet wird und dafür a und b, beide jeweils Bool, im Kontext verfügbar sind. Bool ist an dieser Stelle allerdings so unspezifisch, dass der Typprüfer nicht eindeutig ermitteln kann, was in die Lücke eingesetzt werden muss. Die Semantik muss hier also vom Programmierer festgelegt werden. Das weitere Vorgehen ist es, eine Fallunterscheidung für a nach true oder false vorzunehmen und dann die beiden Zeilen entsprechend auszufüllen:

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

Programme mit Einsprungpunkt

Um ein Programm mit Einsprungpunkt in Agda zu erstellen, empfiehlt es sich, die Standardbibliothek zu nutzen.

{-# OPTIONS --guardedness #-}
module wiki-hello where

open import IO
-- notwendig für "Main", "putStrLn", "getLine", alle Ein-/Ausgabeoperationen
open import Data.String using (_++_)
-- notwendig für Stringoperationen: _++_ = Stringverkettung

main : Main                          -- Einsprungpunkt
main = run do                        -- do-Notation wie in Haskell
  putStrLn "Gib Deinen Namen ein: "  -- putStrLn kann nur innerhalb von "do" verwendet werden
  name ← getLine                     -- "Zuweisung" des Outputs von getLine an "name"
  putStrLn ("Hallo, " ++ name)       -- Verwendung von "name" in putStrLn

Hier muss man auch noch ein paar Bemerkungen machen:

• --guardedness ist notwendig für z. B. unendliche Listen (Streams) oder allgemein coinduktive Daten, wie sie von IO genutzt werden.
• import importiert aus einem Modul alles oder mit using nur die spezifizierten (vollständig qualifizierten) Bezeichner in das aktuelle Modul.
• open entfernt den vorderen Teil des vollständigen Bezeichners (also statt IO.Main nur Main).
• Die Importe sind aus der Standardbibliothek.
• Main ist eine Abkürzung für den Typ IO ⊤, wobei ⊤ für den sog. Einheitstyp steht.
• Die do-Notation funktioniert wie in Haskell. IO ist eine Monade und do ist nur syntaktischer Zucker für eine monadische Verkettung von Operationen wie putStrLn und getLine.

Mit Hilfe der hier genannten Mittel kann man ein ausführbares Programm in Agda erzeugen, welches Terminaleingaben entgegennimmt und -ausgaben erzeugt.

Unendliche, indizierte und parametrisierte Datentypen

Oben wurde der einfache Datentyp Bool eingeführt. Mit endlichen „ist ein“-Datentypen kann man genauso verfahren, also die Konstruktoren einfach aufzählen. Bei „unendlichen“ Datentypen hingegen sind meistens Argumente der Konstruktoren durch den Datentyp selbst gegeben. Daneben unterstützt das data-Schlüsselwort noch Typindizes (rechts vom Doppelpunkt) und Typparameter (links vom Doppelpunkt).

Natürliche Zahlen

Für die natürlichen Zahlen funktioniert die endliche Aufzählung der Konstruktoren nicht mehr. Hier behilft man sich mit den Peano-Axiomen, unter anderem:

• Null ist eine natürliche Zahl und
• jede andere natürliche Zahl ist Nachfolger einer natürlichen Zahl.

Das wird in Agda wie folgt dargestellt:

data ℕ : Set where
  zero : ℕ     -- Null: kann direkt konstruiert werden
  suc  : ℕ → ℕ -- Nachfolger: braucht ein Argument vom Typ ℕ

Hier kommt neu hinzu, dass der Konstruktor suc (für Nachfolger) eine natürliche Zahl als Parameter braucht, um ein gültiges Element des Typs zu erzeugen. Dann ist z. B. eins = suc zero und zwei = suc (suc zero) usw.

Nun kann man noch eine Addition natürlicher Zahlen definieren, die sich die Formulierung in Form von Null und Nachfolger zunutze macht:

_+_ : ℕ → ℕ → ℕ
zero  + m = m           -- 0 + m = m (aber NICHT m + 0 = m!)
suc n + m = suc (n + m) -- suc n + m = suc (n + m)

Hier gibt es eine Fallunterscheidung im ersten Argument. Die Addition wird rekursiv definiert, und zwar so, dass für den Fall „Null“ rechts keine Rekursion mehr steht (Basisfall) und für den Fall „Nachfolger“ rechts „strukturell kleinere“ Argumente für _+_ stehen (insbesondere kein suc mehr).

Typindizes als Relationen

Will man nun natürliche Zahlen mit Hilfe der Kleiner-gleich-Beziehung vergleichen, hat man mehrere Möglichkeiten. Die erste ist, dass man eine Funktion schreibt, die den Typ ℕ → ℕ → Bool hat. Hier verliert man aber sehr viele Informationen sowie die Semantik (engl. Boolean Blindness). Die zweite Möglichkeit ist, dass man einen Typ anlegt, der das leistet. Gemäß der Curry-Howard-Korrespondenz sind Typen auch als Aussagen zu verstehen. Dazu braucht man eine sog. (homogene, zweistellige) Relation. Mathematisch ist das eine Teilmenge des kartesischen Produkts der Ausgangsmenge mit sich selbst, also . In Agda modelliert man das mit sog. indizierten Datentypen (hier mit zwei Indizes):

data _≤_ : ℕ → ℕ → Set where              -- jeder Konstruktor braucht zwei Argumente
  z≤n : {n : ℕ}   →          zero ≤ n     -- z≤n kann direkt generiert werden
  s≤s : {n m : ℕ} → m ≤ n → suc m ≤ suc n -- s≤s braucht als Argument einen Beweis, dass die beiden Vorgänger auch die Relation erfüllen

Am Ende heißt das, dass jeder Konstruktor mit zwei natürlichen Zahlen parametrisiert wird. Im vorliegenden Fall braucht man aber nur zwei Konstruktoren:

• Null ist immer kleiner oder gleich einer beliebigen natürlichen Zahl (z≤n) und
• Falls n ≤ m, dann gilt das auch für ihre Nachfolger (s≤s).
• Die Argumente in geschweiften Klammern sind implizit und werden von Agda ausgefüllt.

Das kann man z. B. zum Beweis nutzen, dass 2 ≤ 4 ist:

2-kleiner-gleich-4 : (suc (suc zero)) ≤ (suc (suc (suc (suc zero))))
2-kleiner-gleich-4 = s≤s (s≤s z≤n)

data definiert einen Typ. Daher ist die Aussage 2 ≤ 4 als Typ der Variable 2-kleiner-gleich-4 implementiert. Nun hat man links und rechts des ≤ jeweils einen Nachfolger stehen, daher kann nur der Konstruktor s≤s in Frage kommen. Das Argument von s≤s ist aber vom Typ her nicht mehr die ursprüngliche Ungleichung, sondern beide Seiten um eins vermindert (1 ≤ 3). Nun kann man noch einmal s≤s einsetzen. Dessen inneres Argument ist aber vom Typ (0 ≤ 2). Das entspricht aber dem Konstruktor z≤n, welcher keine weiteren Argumente hat und damit die Rekursion beendet. Die Aussage ist durch den Typ repräsentiert und der Beweis durch eine Variable dieses Typs.

Um natürliche Zahlen nicht nur als zero oder suc zu erzeugen, kann man auch ein sog. Pragma (eine Compiler-Anweisung) verwenden, hier

{-# BUILTIN NATURAL ℕ #-}

Damit könnte man die Variable 2-kleiner-gleich-4 von oben auch wie folgt definieren:

2-kleiner-gleich-4' : 2 ≤ 4
2-kleiner-gleich-4' = s≤s (s≤s z≤n)

Ein anderes Beispiel für eine Aussage in Form eines indizierten Datentyps ist das aller geraden natürlichen Zahlen . Da man hier nur eine Teilmenge der natürlichen Zahlen anschaut, braucht man nur einen Typindex:

data IsEven : ℕ → Set where
  zeroIsEven   : IsEven zero
  sucsucIsEven : {n : ℕ} → IsEven n → IsEven (suc (suc n))

Auch hier kann man wieder einen Beweis dafür, dass 4 gerade ist, führen:

4-iseven : IsEven 4
4-iseven = sucsucIsEven (sucsucIsEven zeroIsEven)

Die Argumentation läuft ähnlich wie oben: 4 ist der Nachfolger-Nachfolger von 2, daher muss man mit dem Konstruktor sucsucIsEven starten. Das Argument von sucsucIsEven ist dann aber vom Typ IsEven 2. 2 ist aber Nachfolger-Nachfolger von 0, und daher muss man wieder sucsucIsEven verwenden. Dessen Argument hat aber dann den Typ IsEven 0, was nur durch den Konstruktor zeroIsEven abgedeckt wird. Dieser hat keine Argumente mehr und beendet die Rekursion. Versucht man das mit einer ungeraden Zahl, landet man irgendwann beim Typ IsEven 1. Den kann man aber nicht konstruieren.

Typindizes zur Präzisierung von Daten

Typindizes benutzt man auch, um Datentypen zu präzisieren. Hier ein Beispiel über Speisen und ihren Zuckergehalt.

data ZuckerSalz : Set where
  zucker : ZuckerSalz
  salz   : ZuckerSalz

data Speise : ZuckerSalz → Set where
  kuchen     : Speise zucker
  butterbrot : Speise salz
  dessert    : Speise zucker

data Gewicht : Set where
  _g : ℕ → Gewicht

zuckergehalt : Speise zucker → Gewicht
zuckergehalt kuchen  = 100 g
zuckergehalt dessert = 20 g

Speisen werden durch Zucker oder Salz präzisiert. Während Kuchen und Dessert Zucker enthalten, wird das Butterbrot mit Salz gereicht. Die Funktion zuckergehalt bekommt dann nur eine Speise mit dem Typindex zucker übergeben (daher wird das butterbrot im Patternmatching gar nicht abgefragt) und gibt ein Gewicht zurück.

Typparameter

Eine andere Typkonstruktion ist eine (typ-)homogene Liste. Eine Liste ist entweder eine leere Liste oder eine Zusammensetzung von erstem Element und hinterer Liste:

data List (A : Set) : Set where
  []  : List A                   -- leere Liste: kann direkt angelegt werden
  _∷_ : A → List A → List A      -- sog. Cons-Liste: braucht als Argument ein vorderes Listenelement (head) und eine hintere Liste (tail)

infixr 2 _∷_                     -- _∷_ ist rechtsassoziativ mit Priorität 2

liste1 : List ℕ
liste1 = 3 ∷ 4 ∷ 1 ∷ 0 ∷ []

liste2 : List Bool
liste2 = true ∷ false ∷ false ∷ []

Der Typparameter A (hier der Typ der Listenelemente) ist eine globale Konstante in der data-Definition. Im Beispiel wurde _∷_ rechtsassoziativ gewählt. Damit ist 3 ∷ 4 ∷ 1 ∷ 0 ∷ [] eigentlich (3 ∷ (4 ∷ (1 ∷ (0 ∷ [])))). Andersherum (also linksassoziativ) ergäbe es keinen Sinn, da 3 ∷ 4 keine sinnvolle Liste wäre.

Typparameter und Typindizes kombiniert

Will man nun das erste Element einer Liste erhalten, kann es passieren, dass die Liste leer ist. In dem Fall muss man sich um das Abfangen von Fehlern kümmern. Agda bietet aber die Möglichkeit, eine Liste zu definieren, die in ihrer Typdefinition ihre Länge mitführt. Hier wird dann eine Mischung aus Typparameter (für den homogenen Typ) und Typindex (für die Länge) genutzt:

data Vec (A : Set) : ℕ → Set where
  []  :                         Vec A 0
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

vec1-len3 : Vec ℕ 3
vec1-len3 = 3 ∷ 1 ∷ 4 ∷ []

vec2-len5 : Vec Bool 5
vec2-len5 = true ∷ false ∷ false ∷ true ∷ true ∷ []

head : {A : Set} → {n : ℕ} → Vec A (suc n) → A
head (x ∷ xs) = x

Man sieht, dass Vec entsprechend seiner Definition immer zwei Parameter hat, nämlich A, was innerhalb des data-Blocks gleich bleibt und n, was sich ändern kann. vec1-len3 und vec2-len5 haben definierte Typen und Längen. Alle Abweichungen davon bei der Zuweisung würden Typfehler nach sich ziehen. head zeigt in seiner Typsignatur, dass der Vektor, auf den es angewandt wird, die Länge suc n hat und dementsprechend nicht Null sein kann. Daher hat die Fallunterscheidung in der Definition auch keinen Fall, wo der leere Vektor [] auftaucht. Demzufolge muss head keinen Fehler abfangen, wenn der Vektor leer ist.

Π- und Σ-Typen

Π-Typen sind Funktionstypen, bei denen der Typ des Ergebnisses von der Eingabe abhängt. Im Grunde benutzt man solche Konstruktionen in Agda dauernd, entweder implizit oder explizit, auf jeden Fall aber in Beweisen. Der Π-Typ (für Set) ist wie folgt definiert:

Π : (A : Set) → (A → Set) → Set  -- Π ist eine Funktion, die einen Typ und eine Typfunktion aus diesem Typ in Set nach Set abbildet (also einen Typ erzeugt)
Π A B = (x : A) → B x            -- Der erzeugte Typ ist ein Funktionstyp, dessen benanntes Argument (x : A) in einen Typ, der vom Argument abhängt (B x), abgebildet wird

Π-Typen sind fest in Agda verankert und der Kern der Programmierung mit Typen, die von Werten abhängen. Das Π spielt hier darauf an, dass man informell von einem unendlichen kartesischen Produkt reden könnte. Nutzt man für B eine Funktion, die für true einen Typ A zurückgibt und für false einen Typ B, erhält man das klassische kartesische Produkt .

_×'_ : Set → Set → Set  -- Das kartesische Produkt ist eine Abbildung von Set und Set nach Set
A ×' B = Π Bool λ { true → A ; false → B }
-- Der unabhängige Teil ist Bool und der abhängige Teil macht aus dem Bool zwei verschiedene Typen (A und B)

bsp1 : ZuckerSalz ×' ℕ  -- bsp1 ist ein kartesisches Produkt aus ZuckerSalz und ℕ
bsp1 true = salz        -- mit "true" im Argument spricht man den ersten "Faktor" an und setzt ihn auf "salz" (Typ ZuckerSalz)
bsp1 false = 5          -- mit "false" im Argument spricht man den zweiten "Faktor" an und setzt ihn auf "5" (Typ ℕ)

Das λ { true → A ; false → B } steht hier für eine anonyme Funktion, in der die beiden Fälle für true und false verschiedene Ergebnisse nach sich ziehen. Im vorliegenden Fall liefert diese Funktion allerdings keine Werte zurück, sondern Typen.

Σ-Typen sind (geordnete) Paare, in denen der Typ des zweiten Elements vom ersten Element abhängt. In Agda wird das mit einem record modelliert.

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_      -- Konstruktor durch _,_ (etwa: 1 , 2 oder true , 2)
  field
    proj₁ : A          -- erstes Feld hat Typ A
    proj₂ : B proj₁    -- zweites Feld hat Typ (B proj₁)

_×_ : Set → Set → Set  -- kartesisches Produkt
A × B = Σ A λ _ → B    -- ist ein Σ-Typ, in dem der rechte Teil unabhängig vom linken ist

bsp2 : ZuckerSalz × ℕ
bsp2 = salz , 5

Das λ _ → B steht hier für eine anonyme Funktion, deren einziger Parameter unberücksichtigt bleibt, was durch einen Unterstrich _ angezeigt wird. Die Felder proj₁ und proj₂ werden Projektionen genannt. Das hier definierte kartesische Produkt modelliert in der Curry-Howard-Korrespondenz die Konjunktion. Definiert man noch, dass _,_ und _×_ linksassoziativ sind, kann man kartesische Produkte und ihre Konstruktoren auch hintereinanderschalten und so z. B. Tupel wie in Python simulieren:

infixl 4 _×_  -- die 4 ist hier willkürlich gewählt
infixl 4 _,_

bsp3 : ZuckerSalz × ℕ × Bool
bsp3 = zucker , 3 , true

Das schlägt sich automatisch auch im Pattern-Matching in Funktionen nieder. Formuliert man Σ A B von oben in eine etwas „ergonomischere“ Form eines abhängigen kartesischen Produkts mit Linksassoziativität um,

_×ᵈ_ : (A : Set) → (A → Set) → Set
A ×ᵈ B = Σ A B
infixl 4 _×ᵈ_

kann man solche Tupel so verallgemeinern, dass man von links nach rechts mehr und mehr Abhängigkeiten aufsammelt, die den Typ verfeinern. Das hochgestellte „d“ steht für „dependent“. Beispiele:

funnytypeᵃ : Set
funnytypeᵃ = ℕ ×ᵈ (λ _  → Bool) ×ᵈ λ { (n , true) → ZuckerSalz ; (n , false) → IsEven n }
-- natürliche Zahl × Bool × (ZuckerSalz oder IsEven der natürlichen Zahl)

funnytypeᵇ : Set
funnytypeᵇ = ℕ ×ᵈ (λ _ → ℕ) ×ᵈ (λ (n , m) → IsEven m) ×ᵈ (λ { (n , m , zeroIsEven) → ZuckerSalz
                                                            ; (n , m , sucsucIsEven p) → (n + m) ≤ 6 } )
-- natürliche Zahl n × natürliche Zahl m × IsEven m × (ZuckerSalz oder (n + m) ≤ 6)

x₁ : funnytypeᵃ
x₁ = 5 , true , salz
-- true im zweiten Eintrag fordert ZuckerSalz im dritten, ob die 5 gerade ist, ist egal
x₂ : funnytypeᵃ
x₂ = 2 , false , sucsucIsEven zeroIsEven
-- false im zweiten Eintrag fordert im dritten einen Beweis, dass die Zahl im ersten gerade ist

y₁ : funnytypeᵇ
y₁ = 3 , 2 , sucsucIsEven zeroIsEven , s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))
-- der dritte Eintrag ist ein Beweis, dass die zweite Zahl gerade ist,
-- der vierte, dass die Summe der beiden ersten Einträge kleiner gleich 6 ist.
y₂ : funnytypeᵇ
y₂ = 5 , 0 , zeroIsEven , zucker
-- falls der zweite Eintrag Null ist, ist der dritte "zeroIsEven" und der vierte vom Typ "ZuckerSalz"

Während Π-Typen kartesische Produkte verallgemeinern, verallgemeinern Σ-Typen Summentypen bzw. disjunkte Vereinigungen.

data _⊎_ (A B : Set) : Set where -- disjunkte Vereinigung (oder Summe von A und B)
  inj₁ : A → A ⊎ B               -- A ⊎ B "ist ein" inj₁ mit Argument aus A oder
  inj₂ : B → A ⊎ B               -- ein inj₂ mit Argument aus B

bsp1sum : ZuckerSalz ⊎ ℕ
bsp1sum = inj₂ 5

bsp2sum : Σ Bool λ { true → ZuckerSalz ; false → ℕ }
bsp2sum = false , 5

Die beiden Konstruktoren in _⊎_ werden Injektionen genannt. Die disjunkte Vereinigung modelliert in der Curry-Howard-Korrespondenz die Disjunktion oder das ausschließende Oder.

Π-Typen werden in der Curry-Howard-Korrespondenz für All-Quantoren verwendet und Σ-Typen für Existenzquantoren (wobei aber das, was existiert auch tatsächlich angegeben werden muss).

ex-n-kleiner-gleich-3 : Σ ℕ (λ n → n ≤ 3)
ex-n-kleiner-gleich-3 = 2 , (s≤s (s≤s z≤n))

Hier steht im linken Teil des abhängigen Paares die Zahl, deren Existenz man angenommen hat, und im rechten Teil des Paares der Beweis, dass diese auch tatsächlich die Forderung erfüllt. Also „Es existiert eine natürliche Zahl n ≤ 3. Beweis: n = 2 mit (s≤s (s≤s z≤n)).“.

alle-n-groesser-gleich-0 : Π ℕ (λ n → 0 ≤ n)  -- eigentlich (n : ℕ) → 0 ≤ n
alle-n-groesser-gleich-0 n = z≤n              -- wird schon durch einen Konstruktor abgedeckt

Hier steht eigentlich „Für alle gilt . Beweis: durch Konstruktor z≤n.“

Logik

In der Logik wird zur Definition der Negation der leere Typ (engl. Bottom) benötigt:

data ⊥ : Set where  -- keine Konstruktoren vorhanden

Dann kann man die Negation wie folgt als Abbildung einer Aussage auf Bottom auffassen. Denn falls man eine solche Abbildung findet, muss die Aussage A auch leer sein:

¬ : Set → Set  -- Negation macht aus einem Typ einen anderen Typ
¬ A = A → ⊥    -- Negation ist zu verstehen als "aus A folgt der leere Typ" (dann ist auch A leer und demzufolge logisch falsch)
infix 20 ¬     -- Negation hat Priorität 20

Nun kann man zur Formulierung logischer Aussagen entsprechend der Curry-Howard-Korrespondenz den Folgepfeil als Funktionspfeil definieren:

_⇒_ : Set → Set → Set
A ⇒ B = A → B          -- Folgepfeil = Funktionspfeil

Ein „genau dann, wenn“ wird als kartesisches Produkt (UND-Verknüpfung) zweier Folgepfeile aufgefasst:

_⇔_ : Set → Set → Set
A ⇔ B = (A ⇒ B) × (B ⇒ A)  -- A gdw. B = (aus A folgt B) und (aus B folgt A)

Nun kann man logische Aussagen beweisen, denn Typen sind Aussagen und Beweise sind „Programme“ (oder hier Funktionen):

id : {A : Set} → A ⇒ A  -- aus A folgt A
id = λ a → a            -- anonyme Funktion mit a : A als Parameter gibt a zurück

trivial : {A : Set} → A ⇔ A  -- (aus A folgt A) und (aus A folgt A)
trivial = id , id            -- Beweis durch Paar von id-Funktionen

aussage1 : {A B : Set} → (A ⇒ B) ⇒ (¬ B ⇒ ¬ A) -- (aus A folgt B) daraus folgt (aus nicht B folgt nicht A)
aussage1 A→B ¬B = λ a → ¬B (A→B a)

Man sieht, dass die Beweise durch typpolymorphe Funktionen gegeben sind. Implizit steht bei jeder Funktion: Für alle Aussagen A bzw. für alle Aussagen A und B folgt .... id ist der Beweis der Aussage (des Funktionstyps) „Aus A folgt A“. trivial ist durch den Pfeil in beide Richtungen ein kartesisches Produkt und muss in jedem Eintrag id enthalten. aussage1 ist interessanter: Hier wird ein logischer Schluss für beliebige Aussagen A und B bewiesen. Alle Argumente der Funktion aussage1 sind Voraussetzungen, um die man sich nicht kümmern muss. Aus diesen muss man den geforderten Ergebnistyp (hier Bottom) konstruieren.

• Zuerst kann man durch die Rechtsassoziativität des Folgepfeils die Klammern rechts weglassen.
• Dann kann man den mittleren Folgepfeil nach den Klammern von (A ⇒ B) als UND lesen (Beweis durch Schönfinkeln).
• Nun steht nur noch ein Folgepfeil da, nämlich der zwischen ¬ B und ¬ A.
• D. h., die Funktion (Schlussfolgerung) A→B und die Funktion ¬ B sind beide gegeben. Gesucht ist ein Element des Typs ¬ A.
• ¬ A ist eine Funktion von A auf ⊥, demzufolge muss man mit einer anonymen Funktion starten, die ein a : A als Argument hat.
• Nun muss man einen leeren Typ erzeugen. Die einzige Möglichkeit dazu ist, ¬ B zu nutzen.
• Das Argument von ¬ B ist vom Typ B, man hat allerdings nur ein a : A im Kontext.
• Demzufolge muss man die Funktion A→B mit a als Argument innerhalb von ¬ B aufrufen.

Beweise

Mit den vorhandenen Mitteln kann man zeigen, dass ≤ von oben eine Halbordnung ist:

refl≤ : (x : ℕ) → x ≤ x        -- Für alle x aus ℕ folgt x ≤ x
refl≤ zero    = z≤n            -- Null: 0≤0 folgt aus z≤n
refl≤ (suc x) = s≤s (refl≤ x)  -- Nachfolger: suc x ≤ suc x geht durch s≤s in x ≤ x über, wo man einfach refl≤ einsetzt

trans≤ : {x y z : ℕ} → x ≤ y → y ≤ z → x ≤ z      -- Für alle x, y, z aus ℕ folgt aus x ≤ y und y ≤ z, dass x ≤ z
trans≤       z≤n       y≤z = z≤n                  -- Fallunterscheidung in x ≤ y (Ziel: 0 ≤ z)
trans≤ (s≤s x≤y) (s≤s y≤z) = s≤s (trans≤ x≤y y≤z) -- Fallunterscheidung auch in y ≤ z (Ziel: suc x ≤ suc z)

In der zweiten Zeile bei trans≤ müssen die suc durch Verwendung von s≤s beseitigt werden, wobei x und z nur implizit in den Variablen x≤y und y≤z vorkommen. Ein erneuter Aufruf von trans≤ x≤y y≤z (Induktionsschritt) löst das Problem.

Damit ist gezeigt, dass ≤ erst einmal reflexiv und transitiv ist. Die Verwendung von s≤s im Nachfolger-Fall zusammen mit der Anwendung der Funktion (des Beweises) auf ein Argument ohne suc entspricht dem Induktionsschritt in der vollständigen Induktion. Es fehlt noch die Antisymmetrie. Diese braucht aber die Gleichheit zweier Ausdrücke.

Um Gleichheitsbeweise führen zu können, braucht man einen Gleichheitsbegriff. Die sog. propositionale Äquivalenz wird wie folgt definiert:

data _≡_ {A : Set} : A → A → Set where  -- homogene, zweistellige Relation
  refl : {a : A} → a ≡ a                -- ein Konstruktor, wenn links und rechts "das Gleiche" steht

Sie ist per Definition eine homogene, zweistellige Relation, reflexiv (Konstruktor), aber auch symmetrisch und transitiv:

sym≡ : {A : Set} {x y : A} → x ≡ y → y ≡ x  -- Für alle A und für alle x, y : A folgt aus x ≡ y, dass y ≡ x
sym≡ refl = refl                            -- Einsetzen von refl macht aus x ≡ y ein x ≡ x und wird durch refl gelöst

trans≡ : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z  -- Für alle x, y, z aus A folgt aus x ≡ y und y ≡ z, dass x ≡ z
trans≡ refl y≡z = y≡z                                   -- Einsetzen von refl im ersten Argument fordert y ≡ z als Ziel

Daher ist sie eine Äquivalenzrelation und man kann mit ihr Gleichheitsbeweise führen (engl. equational reasoning). Einfaches Beispiel: Gesucht wird eine natürliche Zahl, deren Nachfolger 3 ist:

n+1≡3 : Σ ℕ (λ n → suc n ≡ 3)
n+1≡3 = 2 , refl

Oder man kann das Assoziativgesetz der Addition natürlicher Zahlen beweisen. Dazu braucht man zuerst aber die Funktion cong (für engl. congruence), mit welcher man schlussfolgern kann, dass wenn x = y dann auch f x = f y.

cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

assoc-+ : (n m p : ℕ) → (n + m) + p ≡ n + (m + p)
assoc-+ zero m p = refl                             -- Ziel: m + p ≡ m + p Lösung: refl, weil 0 + n per Definition ≡ n ist
assoc-+ (suc n) m p = cong suc (assoc-+ n m p)      -- Ziel: suc ((n + m) + p) ≡ suc (n + (m + p)) Lösung: "cong suc"

Der Beweis erfolgt wieder durch Fallunterscheidung zwischen Null und Nachfolger. Im ersten Schritt kann man den Beweis per Reflexivität erbringen. Im zweiten Schritt in assoc-+ erfolgt der Beweis per Induktionsschritt. In beiden Fällen ist die Lösung deshalb so einfach, weil die Definition von _+_ einfach von Agda eingesetzt werden kann und zu den beiden einfachen Zielen führt. Hätte man eine Fallunterscheidung im zweiten oder dritten Argument vorgenommen, hätten etliche sym≡ und trans≡ miteinander „verschaltet“ werden müssen.

Nun kann man auch die Antisymmetrie von ≤ zeigen:

antisym≤ : {n m : ℕ} → n ≤ m → m ≤ n → n ≡ m  -- Für alle n, m aus ℕ folgt aus n ≤ m und m ≤ n, dass n ≡ m
antisym≤       z≤n       z≤n = refl
antisym≤ (s≤s n≤m) (s≤s m≤n) = cong suc (antisym≤ n≤m m≤n)

Hier wird der s≤s-Konstruktor auf der rechten Seite im Nachfolger-Schritt durch cong suc ersetzt, da man eine Gleichung bekommt, in der auf beiden Seiten suc steht.

Gleitkommazahlen, gebrochen rationale Zahlen und reelle Zahlen

In Agda gibt es auch die Möglichkeit, mit Gleitkommazahlen zu arbeiten, die über die Standardbibliothek eingebunden werden können:

{-# OPTIONS --guardedness #-}
module wiki-floats where
open import IO
open import Data.Float using (Float ; _*_ ; _+_; atan2) renaming (show to showFloat)

x : Float
y : Float

x = 1.2
y = 5.7

main : Main
main = run do
  putStrLn ("Die Werte von x = " ++ (showFloat x) ++ " und y = " ++ (showFloat y))
  putStrLn ("ergeben die Summe x + y = " ++ (showFloat (x + y)))
  putStrLn ("und das Produkt x * y = " ++ (showFloat (x * y)) ++ ".")
  putStrLn ("Der Arcustangens von y/x = " ++ (showFloat (atan2 y x)) ++ ".")

Mit und über Gleitkommazahlen beweisbare Aussagen zu treffen ist aus verschiedenen Gründen schwierig. Als Beispiel sei nur genannt, dass sie weder Distributiv- noch Assoziativgesetz für Multiplikation und Addition erfüllen.

Agda bietet jedoch Implementierungen der ganzen Zahlen und der rationalen Zahlen über die Standardbibliothek an. Die Implementierung reeller Zahlen erweist sich durch die intuitionistische Logik auch als schwierig.

Universalhierarchie

Agda bietet, wie oben schon angedeutet, eine unendliche Hierarchie von Typen. Bool : Set aber Set : Set₁ und Set₁ : Set₂ usw. Die einzelnen Sets werden als Sorten, Arten (engl. sorts) oder Universen (engl. universes) bezeichnet. Oben wurde schon das Beispiel der Liste, hier als SmallList bezeichnet, implementiert:

data SmallList (A : Set) : Set where  -- Beachte: "A : Set" und "SmallList : Set → Set"
  []  : SmallList A
  _∷_ : A → SmallList A → SmallList A

infixr 4 _∷_

open import Data.Bool using (Bool ; true ; false)

sl₁ : SmallList Bool
sl₁ = true ∷ false ∷ false ∷ true ∷ []

Das ist in Ordnung, weil Bool ein kleiner Typ ist und A in der Definition von SmallList auch. Beide sind vom Typ Set. Würde man dort aber versuchen, eine Liste von Typen darzustellen, wäre die Folge ein Typgrößenfehler:

-- sl₂ : SmallList Set  -- Fehler: Typgrößenfehler
-- sl₂ = Bool ∷ ℕ ∷ []

Das funktioniert nicht, weil Set kein kleiner Typ ist. Agda bemerkt: „Set₁ != Set when checking that the expression Set has type Set“. Man kann sich behelfen, indem man eine neue Liste definiert, die „BigList“ genannt wird:

data BigList (A : Set₁) : Set₁ where  -- Beachte: "A : Set₁" und "BigList : Set₁ → Set₁"
  []  : BigList A
  _∷_ : A → BigList A → BigList A

mit

open import Data.Nat using (ℕ)

bl₁ : BigList Set
bl₁ = Bool ∷ ℕ ∷ []  -- Liste von Typen

Die Implementierung von BigList sieht (bis auf die 1 am Set) genauso aus, wie die Implementierung von SmallList. Wenn man nun aber Werte aus Set₂ in einer Liste haben wollte, müsste man wiederum eine neue Liste, genau wie BigList und auch SmallList, implementieren. Dadurch, dass die Typhierarchie aber unendlich ist, tut man sich damit keinen Gefallen. In Agda kann man Typen daher mit Hilfe sog. Ebenen (engl. Levels) universalpolymorph implementieren:

open import Level renaming (zero to lzero ; suc to lsuc)

data List {ℓ : Level} (A : Set ℓ) : Set ℓ where  -- Beachte: "A : Set ℓ" und "List : Set ℓ → Set ℓ"
  []  : List A
  _∷_ : A → List A → List A

Hier tritt implizit ein neuer Parameter ℓ vom Typ Level auf. Der Parameter ist implizit, weil Agda ihn aus der Parameterangabe von List schlussfolgern kann. Demzufolge ist List jetzt in dem Sinne universell, dass der Typparameter beliebig „groß“ werden kann:

sl : List Bool
sl = true ∷ false ∷ false ∷ []

bl : List Set
bl = Bool ∷ ℕ ∷ ℕ ∷ Bool ∷ []

List ist insofern ein Sonderfall, weil sich die Universalebene durch den Typparameter auf den finalen Typ des data-Blocks überträgt. Hat man allerdings in einem Konstruktor z. B. einen direkten Set ℓ-Parameter, muss sich die Ebene des data-Blocks mindestens um Eins erhöhen:

data Bla {ℓ : Level} : Set (lsuc ℓ) where
  blub : Set ℓ → Bla

Es gibt noch eine andere, wichtige Art und Weise, wie man „große“ Typen erzeugen kann, nämlich über einen record. Als Beispiel kann man sich die mathematische Struktur eines Monoids anschauen:

record SmallMonoid : Set₁ where
  field
    träger : Set
    _·_    : träger → träger → träger  -- auch hier: Typ hängt vom vorhergehenden Feld ab
    e      : träger
    -- Assoziativgesetz und Neutralelement unterdrückt

Hier sorgt „träger : Set“ dafür, dass „SmallMonoid : Set₁“ ist, weil damit eines der Felder keinen konkreten Typ trägt, sondern gesagt wird, „träger“ kann ein beliebiger (kleiner) Typ sein. Z. B. könnte man aus

_and_ : Bool → Bool → Bool
true  and y = y
false and y = false

ein Monoid über Bool für and und true konstruieren:

boolMonoid : SmallMonoid
boolMonoid .SmallMonoid.träger = Bool
boolMonoid .SmallMonoid._·_ = _and_
boolMonoid .SmallMonoid.e = true

Auch ein Monoid über die natürlichen Zahlen mit 0 als Neutralelement wäre möglich. Was aber nicht möglich ist, ist wenn träger = Set sein sollte. Dann müsste es nämlich vom Typ Set₁ sein. Demzufolge muss man auch die Monoiddefinition universell gestalten:

record Monoid {ℓ : Level} : Set (lsuc ℓ) where
  field
    träger : Set ℓ
    _·_    : träger → träger → träger
    e      : träger
  -- Assoziativgesetz und Neutralelement unterdrückt

Im Falle von ℓ = 0 erhält man SmallMonoid zurück. Dann ist boolMonoid : Monoid {lzero} : Set₁. Es ist aber jetzt auch möglich, träger = Set zu setzen.

boolMonoid' : Monoid  -- implizit: ℓ = 0
boolMonoid' .Monoid.träger = Bool
boolMonoid' .Monoid._·_ = _and_
boolMonoid' .Monoid.e = true

open import Data.Product using (_×_)
open import Data.Unit using (⊤)

setMonoid : Monoid  -- implizit: ℓ = 1
setMonoid .Monoid.träger = Set
setMonoid .Monoid._·_ = _×_
setMonoid .Monoid.e = ⊤

(Streng genommen ist setMonoid nur dann ein Monoid, wenn man als Äquivalenzrelation in den Gesetzen „isomorph“ und nicht mehr „gleich“ annimmt. Das beeinträchtigt aber die Diskussion hier nicht.)

Modulsystem

Agda hat ein sehr flexibles Modulsystem. Jede Datei ist für sich schon ein Modul, man kann jedoch auch Untermodule definieren.

module UnterModulA where
  a : ℕ
  a = 1

module UnterModulB where
  b : ℕ
  b = 2

c₁ c₂ : ℕ
c₁ = UnterModulA.a  -- 1
c₂ = UnterModulB.b  -- 2

Öffnet man die Module, entfernt man den vorderen Teil des vollständig qualifizierten Bezeichners und holt die Bezeichner in den aktuellen Namensraum. Das wurde oben schon mit den Imports durchgeführt, kann aber auch für Untermodule oder records gemacht werden.

c₃ = a -- 1
  where open UnterModulA

Module können auch parametrisiert werden:

open import Data.Nat using (_+_)

module UnterModulC (n : ℕ) where
  h : ℕ
  h = n + 7

  i : ℕ → ℕ
  i x = n + x

c₅ = h 8  -- 15
  where open UnterModulC
c₆ = h  -- 15
  where open UnterModulC 8  -- Untermodul mit Parameter
c₇ = UnterModulC.h 8  -- 15
c₈ = i 8 9 -- 17
  where open UnterModulC
c₉ = i 9 -- 17
  where open UnterModulC 8  -- Untermodul mit Parameter
c₁₀ = UnterModulC.i 8 9 -- 17

Module können auch anonym sein. Das bietet sich dann an, wenn man z. B. Funktionen hat, die immer dieselben Argumente brauchen.

module _ {ℓ : Level} {A B : Set ℓ} where
  const₁ : A → B → A
  const₁ a _ = a

  const₂ : A → B → B
  const₂ _ b = b

Anonyme Module führen keine zusätzliche Namensraumhierarchieebene ein:

c₁₁ = const₁ 10 20  -- 10

Module können genutzt werden, um Postulate zu vermeiden. Diese werden verwendet, um Aussagen über eine Typspezifikation zu deklarieren ohne sie zu implementieren (also zu beweisen). Postulate bergen aber das Risiko, das logische System inkonsistent zu machen.

Agda unterstützt z. B. keinen Satz vom ausgeschlossenen Dritten (engl. Law of Excluded Middle). Diesen kann man aber auf Modulebene trotzdem einführen. Damit wird er als Argument für jede Funktion innerhalb des Moduls verlangt. Aber die Verantwortung, ihn auch tatsächlich bereitzustellen, liegt damit beim Aufrufer. Hier wird der Satz beispielsweise genutzt, um zu beweisen, dass ¬ ¬ A ⇒ A.

open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥)

case⊥ : {A : Set} → ⊥ → A  -- aus Falschem folgt Beliebiges
case⊥ ()                   -- das ist absurd

module LEM (lem : {A : Set} → A ⊎ ¬ A) where
  double-negation-elimination : {B : Set} → ¬ ¬ B → B
  double-negation-elimination {B} f with lem {B}
  -- man muss eine Fallunterscheidung über `lem` machen
  ... | inj₁ b = b  -- entweder man hat den Beweis für B, dann ist man fertig
  ... | inj₂ ¬B = case⊥ (f ¬B) -- oder nur für „nicht B“, ¬B, dann führt man das zum Widerspruch.

Der Typ von LEM.double-negation-elimination ist damit ({A : Set} → A ⊎ ¬ A) → {B : Set} → ¬ (¬ B) → B und man sieht, dass als erstes Argument der Typ von lem erscheint. Normalerweise ruft man solche Funktionen nicht aus dem übergeordneten Modul auf, gerade weil man das erste Argument nicht ausfüllen kann. Es reicht, im inneren Modul zu arbeiten und dort „so zu tun“, als hätte bereits jemand den Parameter übergeben. Der Vorteil ist, dass man die Logik ggf. nur innerhalb eines Moduls inkonsistent macht:

module Inconsistent (nonsense : {A : Set} → ¬ A → A) where  -- nonsense: aus ¬ A folgt A
  open import Relation.Binary.PropositionalEquality using (_≡_)
  _ : 0 ≡ 1
  _ = nonsense λ () -- Beweis, dass 0 ≡ 1 mit Hilfe von `nonsense`

Module können auch geschachtelt werden und tragen damit zur Organisation und Wiederverwendbarkeit des Codes bei.

module UnterModulD where
  module UnterunterModul where
    a₁ : ℕ
    a₁ = 3

c₁₂ = UnterModulD.UnterunterModul.a₁  -- 3
c₁₃ = a₁  -- 3
  where open UnterModulD.UnterunterModul

Jeder record ist ein eigenes Modul.

record MyRecord : Set where
  -- Beachte: Kein "field"
  a₂ : ℕ
  a₂ = 1

c₁₄ = a₂  -- 1
  where open MyRecord

Hier ist der Typ geöffnet worden. Oft ist jedoch eine bestimmte Instanz gemeint, insbesondere wenn man die Felder eines records adressieren will:

record MyRecord' : Set where
  a₃ : ℕ
  a₃ = 2
  field
    myfield : ℕ
  a₄ : ℕ
  a₄ = myfield + 3

myrecord' : MyRecord'
myrecord' = record { myfield = 2 }

c₁₅ = a₄  -- 5, Instanz myrecord'
  where open MyRecord' myrecord'
c₁₆ = a₄  -- λ r → MyRecord'.myfield r + 3, keine konkrete Instanz r
  where open MyRecord'
c₁₇ = c₁₆ myrecord'  -- 5, Instanz wird konkret, wenn man ein Argument in c₁₆ verwendet.

Literatur

• Sandy Maguire (2023). Certainty by Construction
• Phil Wadler, Wen Kokke, and Jeremy G. Siek (2019). Programming Languages Foundations in Agda