Funktionale Programmierung in Agda

In dieser Datei werden wir einen kleinen Blick in funktionale Programmierung mit Agda wagen. Agda ist eine funktionale Programmiersprache wie Haskell, jedoch besitzt Agda ein deutlich ausdrucksstärkeres Typsystem durch sogenannte dependent types. Das sind Typen welche von Termen der Programmiersprache abhängen können, aber dazu in späteren Kapiteln mehr.

Warmup

Ziel dieses Kapitels ist es etwas Familiarität mit Agda zu gewinnen. Wir werden vor allem bekanntes Wissen aus ThProg anwenden und hier implementieren.

Recall: Lambda-Kalkül

Der (ungetypte) Lambda-Kalkül ist die Grundlage jeder funktionalen Programmiersprache. Ein Term des Lambda-Kalküls ist entweder - Eine Variable x ∈ V - Eine Applikation zweier Lambda Terme t₁t₂ - Eine Lambda-Abstraktion λx.t, wobei x ∈ V und t Term.

Diese drei Komponenten finden wir deshalb in jeder funktionalen Programmiersprache, wobei in der Regel Syntaxzucker für Lambda-Abstraktionen angeboten wird (die übliche Funktionsnotation).

Applikation in Agda ist klar, einfach das hintereinanderschreiben von Termen, Abstraktion wird geschrieben als ‘λ x → t’.

Aufgabe 1

Definiere die Identitätsfunktion.

id : ∀ {A : Type} → A → A
-- Erklärung des Typs:
-- Der Allquantor funktioniert wie in System F, nur hat der Typ über den wir quantifizieren ebenfalls einen Typ! (Den Typ 'Type' der Typen)
id = _

Aufgabe 2

Definiere die Komposition zweier Funktionen.

_∘_ : ∀ {A B C : Type} → (g : B → C) → (f : A → B) → A → C
_∘_ = _

Induktive Datentypen

Agda implementiert induktive Datentypen genau so wie wir sie in ThProg kennengelernt haben, d.h. wir definieren einen Datentypen, indem wir seine Konstruktoren angeben. Ein paar Beispiele:

Booleans

data 𝔹 : Type where
  tt : 𝔹
  ff : 𝔹
{-# BUILTIN BOOL  𝔹  #-}
{-# BUILTIN TRUE  tt #-}
{-# BUILTIN FALSE ff #-}

Aufgabe 3

Definiere die Funktion flip, welche einen logischen Wert invertiert.

flip : 𝔹 → 𝔹
flip b = _

Aufgabe 4

Definiere die Funktion and.

and : 𝔹 → 𝔹 → 𝔹
and b₁ b₂ = _

Aufgabe 5

Definiere die Funktion if then else.

if_then_else_ : ∀ {A : Type} → 𝔹 → A → A → A
if b then t else s = _

Aufgabe 6

Definiere die Fold-Funktion auf booleans.

foldb : ∀ {C : Type} → C → C → 𝔹 → C
foldb t s b = _

Natürliche Zahlen

data ℕ : Type where
  zero : ℕ
  succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-} -- Hierdurch können wir einfach '0, 1, 2, ...' statt 'zero, succ zero, succ (succ zero), ...' schreiben, wir bekommen aber **keine** Funktionen wie z.B. Addition geschenkt!

Aufgabe 7

Definiere die Additionsfunktion auf natürlichen Zahlen.

add : ℕ → ℕ → ℕ
add n m = _

Aufgabe 8

Definiere eine Subtraktionsfunktion.

sub : ℕ → ℕ → ℕ
sub n m = _

Aufgabe 9

Definiere die Fold-Funktion auf natürlichen Zahlen.

foldn : ∀ {C : Type} → C → (C → C) → ℕ → C
foldn c h n = _

Listen

data List (A : Type) : Type where
  nil : List A
  _∷_ : A → List A → List A
{-# BUILTIN LIST List #-}
infixr 5 _∷_

Aufgabe 10

Definiere die length Funktion.

length : ∀ {A : Type} → List A → ℕ
length xs = _

Aufgabe 11

Definiere die filter Funktion.

filter : ∀ {A : Type} → (A → 𝔹) → List A → List A
filter f xs = _

Aufgabe 12

Definiere die map Funktion.

map : ∀ {A B : Type} → (A → B) → List A → List B
map f xs = _

Aufgabe 13

Definiere die Fold-Funktion für Listen.

foldr : ∀ {C : Type} → C → (A → C → C) → List A → C
foldr c h xs = _