82 lines
No EOL
2.5 KiB
Markdown
82 lines
No EOL
2.5 KiB
Markdown
# 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.
|
||
|
||
<!--
|
||
```agda
|
||
module intro where
|
||
Type = Set
|
||
private
|
||
variable
|
||
A B C : Type
|
||
open import Agda.Primitive
|
||
```
|
||
-->
|
||
|
||
## 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
|
||
|
||
```agda
|
||
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
|
||
```agda
|
||
_∘_ : ∀ {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:
|
||
|
||
### Natürliche Zahlen
|
||
```agda
|
||
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 3
|
||
Definiere die Additionsfunktion auf natürlichen Zahlen
|
||
```agda
|
||
add : ℕ → ℕ → ℕ
|
||
add n m = _
|
||
```
|
||
|
||
Definiere die Prädezessorfunktion
|
||
#### Aufgabe 4
|
||
```agda
|
||
pred : ℕ → ℕ
|
||
pred n = _
|
||
```
|
||
|
||
#### Aufgabe 4
|
||
Definiere eine Subtraktionsfunktion
|
||
```agda
|
||
sub : ℕ → ℕ → ℕ
|
||
sub n m = _
|
||
``` |