For this presentation, we keep the dependencies to a minimum.
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
A variable declaration allows us to use variables without binding
them explicitly. This means they are implicitly universally quantified
in the types where they occur.
variable
A B C : Set
x y z : A
k l m n : Nat
it : {{x : A}} → A
it {{x}} = x
(Unary) natural numbers are defined as the datatype Nat with two
constructors zero : Nat and suc : Nat → Nat.
_ : Nat
_ = zero + 7 * (suc 3 - 1)
We can define polymorphic types and functions by pattern matching on
them. For example, here is the equivalent of Haskell's Maybe type.
data Maybe (A : Set) : Set where
just : A → Maybe A
nothing : Maybe A
mapMaybe : (A → B) → (Maybe A → Maybe B)
mapMaybe f (just x) = just (f x)
mapMaybe f nothing = nothing
Note how A and B are implicitly quantified in the type of
mapMaybe!
Under the Curry-Howard correspondence, we can interpret logical propositions (A ∧ B, ¬A, A ⇒ B, ...) as the types of all their possible proofs.
A proof of 'A and B' is a pair (x , y) of a proof x : A and an
proof y : B.
record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
open _×_
A proof of 'A or B' is either inl x for a proof x : A or inr y
for a proof y : B.
data _⊎_ (A B : Set) : Set where
inl : A → A ⊎ B
inr : B → A ⊎ B
mapInl : (A → B) → A ⊎ C → B ⊎ C
mapInl f (inl x) = inl (f x)
mapInl f (inr y) = inr y
mapInr : (B → C) → A ⊎ B → A ⊎ C
mapInr f (inl x) = inl x
mapInr f (inr y) = inr (f y)
A proof of 'A implies B' is a transformation from proofs x : A to
proofs of B, i.e. a function of type A → B.
'true' has exactly one proof tt : ⊤.
record ⊤ : Set where
constructor tt -- no fields
'false' has no proofs.
data ⊥ : Set where -- no constructor
'not A' can be defined as 'A implies false'.
¬_ : Set → Set
¬ A = A → ⊥
-- “If A then B implies A”
ex₁ : A → (B → A)
ex₁ = λ z _ → z
-- “If A and true then A or false”
ex₂ : (A × ⊤) → (A ⊎ ⊥)
ex₂ = λ z → inl (fst z)
-- “If A implies B and B implies C then A implies C ”
ex₃ : (A → B) → (B → C) → (A → B)
ex₃ = λ z _ → z
-- “Either A or not A”
--ex₄ : A ⊎ (¬ A)
--ex₄ = {!!}
-- “It is not the case that not (either A or not A)”
ex₅ : ¬ (¬ (A ⊎ (¬ A)))
ex₅ {A = A} = λ (x : ¬ (A ⊎ (¬ A))) → x (inr (λ y → x (inl y)))
To state many properties of our programs, we need the notion of
equality. In Agda, equality is defined as the datatype _≡_ with one
constructor refl : x ≡ x.
_ : x ≡ x
_ = refl
subst : (P : A → Set) → x ≡ y → P x → P y
subst P refl p = p
sym : x ≡ y → y ≡ x
sym {x = x} {y = y} x≡y = subst (λ z → z ≡ x) x≡y refl
trans : x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
cong : (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl
The standard ordering on natural numbers can be defined as an indexed
datatype with two indices of type Nat:
module Nat-≤ where
data _≤_ : Nat → Nat → Set where
≤-zero : zero ≤ n
≤-suc : m ≤ n → suc m ≤ suc n
≤-refl : n ≤ n
≤-refl {n = zero} = ≤-zero
≤-refl {n = suc k} = ≤-suc ≤-refl
≤-trans : k ≤ l → l ≤ m → k ≤ m
≤-trans ≤-zero l≤m = ≤-zero
≤-trans (≤-suc k≤l) (≤-suc l≤m) = ≤-suc (≤-trans k≤l l≤m)
≤-antisym : m ≤ n → n ≤ m → m ≡ n
≤-antisym ≤-zero ≤-zero = refl
≤-antisym (≤-suc m≤n) (≤-suc n≤m) = cong suc (≤-antisym m≤n n≤m)
We define separate 'instance' versions of the constructors to help us
later on. A definition inst : A that is marked as an 'instance' will
be used to automatically construct arguments to functions of type
{{x : A}} → B.
So : Bool → Set
So false = ⊥
So true = ⊤
instance
≤-dec : {p : So (m < suc n)} → m ≤ n
≤-dec {m = zero} {n = n} = ≤-zero
≤-dec {m = suc m} {n = suc n} {p = p} = ≤-suc (≤-dec {p = p})
test : 3 ≤ 3
test = it
We'd like to talk not just about orderings on concrete types like
Nat, but also about the general concept of a 'partial order'.
record Ord (A : Set) : Set₁ where
field
_≤_ : A → A → Set
≤-refl : x ≤ x
≤-trans : x ≤ y → y ≤ z → x ≤ z
≤-antisym : x ≤ y → y ≤ x → x ≡ y
_≥_ : A → A → Set
x ≥ y = y ≤ x
open Ord {{...}}
instance
Ord-Nat : Ord Nat
_≤_ {{Ord-Nat}} = Nat-≤._≤_
≤-refl {{Ord-Nat}} = Nat-≤.≤-refl
≤-trans {{Ord-Nat}} = Nat-≤.≤-trans
≤-antisym {{Ord-Nat}} = Nat-≤.≤-antisym
instance
Ord-⊤ : Ord ⊤
_≤_ {{Ord-⊤}} = λ _ _ → ⊤
≤-refl {{Ord-⊤}} = tt
≤-trans {{Ord-⊤}} = λ _ _ → tt
≤-antisym {{Ord-⊤}} = λ _ _ → refl
module Example (A : Set) {{A-≤ : Ord A}} where
cycle : {x y z : A} → x ≤ y → y ≤ z → z ≤ x → x ≡ y
cycle x≤y y≤z z≤x = ≤-antisym x≤y (≤-trans y≤z z≤x)
For working with binary search trees, we need to be able to decide for any two elements which is the bigger one, i.e. we need a total, decidable order.
data Tri {{_ : Ord A}} : A → A → Set where
less : x ≤ y → Tri x y
equal : x ≡ y → Tri x y
greater : x ≥ y → Tri x y
record TDO (A : Set) : Set₁ where
field
{{Ord-A}} : Ord A
tri : (x y : A) → Tri x y
open TDO {{...}} public
triNat : (x y : Nat) → Tri x y
triNat zero zero = equal refl
triNat zero (suc y) = less Nat-≤.≤-zero
triNat (suc x) zero = greater Nat-≤.≤-zero
triNat (suc x) (suc y) with triNat x y
... | less x≤y = less (Nat-≤.≤-suc x≤y)
... | equal x≡y = equal (cong suc x≡y)
... | greater x≥y = greater (Nat-≤.≤-suc x≥y)
instance
TDO-Nat : TDO Nat
Ord-A {{TDO-Nat}} = Ord-Nat
tri {{TDO-Nat}} = triNat
In a dependently typed language, we can encode invariants of our data structures by using indexed datatypes. In this example, we will implement binary search trees by a lower and upper bound to the elements they contain.
Since the lower bound may be -∞ and the upper bound may be +∞, we start by providing a generic way to extend a partially ordered set with those two elements.
data [_]∞ (A : Set) : Set where
-∞ : [ A ]∞
[_] : A → [ A ]∞
+∞ : [ A ]∞
variable
lower upper : [ A ]∞
module Ord-[]∞ {A : Set} {{ A-≤ : Ord A}} where
data _≤∞_ : [ A ]∞ → [ A ]∞ → Set where
-∞-≤ : -∞ ≤∞ y
[]-≤ : x ≤ y → [ x ] ≤∞ [ y ]
+∞-≤ : x ≤∞ +∞
[]∞-refl : x ≤∞ x
[]∞-refl { -∞} = -∞-≤
[]∞-refl {[ x ]} = []-≤ ≤-refl
[]∞-refl { +∞} = +∞-≤
[]∞-trans : x ≤∞ y → y ≤∞ z → x ≤∞ z
[]∞-trans -∞-≤ _ = -∞-≤
[]∞-trans ([]-≤ x≤y) ([]-≤ y≤z) = []-≤ (≤-trans x≤y y≤z)
[]∞-trans _ +∞-≤ = +∞-≤
[]∞-antisym : x ≤∞ y → y ≤∞ x → x ≡ y
[]∞-antisym -∞-≤ -∞-≤ = refl
[]∞-antisym ([]-≤ x≤y) ([]-≤ y≤x) = cong [_] (≤-antisym x≤y y≤x)
[]∞-antisym +∞-≤ +∞-≤ = refl
instance
Ord-[]∞ : {{_ : Ord A}} → Ord [ A ]∞
_≤_ {{Ord-[]∞}} = _≤∞_
≤-refl {{Ord-[]∞}} = []∞-refl
≤-trans {{Ord-[]∞}} = []∞-trans
≤-antisym {{Ord-[]∞}} = []∞-antisym
open Ord-[]∞ public
Again we define 'instance' versions of the constructors.
module _ {{_ : Ord A}} where
instance
-∞-≤-I : {y : [ A ]∞} → -∞ ≤ y
-∞-≤-I = -∞-≤
+∞-≤-I : {x : [ A ]∞} → x ≤ +∞
+∞-≤-I = +∞-≤
[]-≤-I : {x y : A} {{x≤y : x ≤ y}} → [ x ] ≤ [ y ]
[]-≤-I {{x≤y = x≤y}} = []-≤ x≤y
Now we are (finally) ready to define binary search trees.
data BST (A : Set) {{_ : Ord A}} (lower upper : [ A ]∞) : Set where
leaf : {{l≤u : lower ≤ upper}} → BST A lower upper
node : (x : A)
→ BST A lower [ x ]
→ BST A [ x ] upper
→ BST A lower upper
_ : BST Nat -∞ +∞
_ = node 42
(node 6 leaf leaf)
(node 9000 leaf leaf)
module Weaken {A : Set} {{_ : Ord A}} where
weaken : ∀ {lower upper upper'} → upper ≤ upper'
→ BST A lower upper → BST A lower upper'
weaken u≤u' leaf = leaf {{l≤u = ≤-trans it u≤u'}}
weaken u≤u' (node x t₁ t₂) = node x t₁ (weaken u≤u' t₂)
Note how instances help by automatically filling in the proofs!
Next up: defining a lookup function. The result of this function is not just a boolean true/false, but a proof that the element is indeed in the tree.
module Lookup {{_ : TDO A}} where
data _∈_ {lower} {upper} (x : A) : (t : BST A lower upper) → Set where
here : ∀ {t₁ t₂} → x ≡ y → x ∈ node y t₁ t₂
left : ∀ {t₁ t₂} → x ∈ t₁ → x ∈ node y t₁ t₂
right : ∀ {t₁ t₂} → x ∈ t₂ → x ∈ node y t₁ t₂
lookup : ∀ {lower} {upper}
→ (x : A) (t : BST A lower upper) → Maybe (x ∈ t)
lookup x leaf = nothing
lookup x (node y t₁ t₂) with tri x y
... | less x≤y = mapMaybe left (lookup x t₁)
... | equal x≡y = just (here x≡y)
... | greater x≥y = mapMaybe right (lookup x t₂)
Similarly, we can define an insertion function. Here, we need to enforce the precondition that the element we want to insert is between the bounds.
module Insert {{_ : TDO A}} where
insert : (x : A) {{l≤x : lower ≤ [ x ]}} {{x≤u : [ x ] ≤ upper}}
→ (t : BST A lower upper) → BST A lower upper
insert x leaf = node x leaf leaf
insert x (node y t₁ t₂) with tri x y
... | less x≤y =
let instance _ = x≤y
in node y (insert x t₁) t₂
... | equal x≡y = node y t₁ t₂
... | greater x≥y =
let instance _ = x≥y
in node y t₁ (insert x t₂)
To prove correctness of insertion, we have to show that
y ∈ insert x t is equivalent to x ≡ y ⊎ y ∈ t.
module Insert-Correct where
open Lookup
insert-sound : (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}}
→ (t : BST A lower upper)
→ (x ≡ y) ⊎ (y ∈ t) → y ∈ insert x t
insert-sound x t (inl refl) = insert-sound₁ x t
where
insert-sound₁ : (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}}
→ (t : BST A lower upper)
→ x ∈ insert x t
insert-sound₁ x leaf = here refl
insert-sound₁ x (node y t₁ t₂) with tri x y
insert-sound₁ x (node y t₁ t₂) | less x≤y =
let instance _ = x≤y
in left (insert-sound₁ x t₁)
insert-sound₁ x (node y t₁ t₂) | equal x≡y = here x≡y
insert-sound₁ x (node y t₁ t₂) | greater x≥y =
let instance _ = x≥y
in right (insert-sound₁ x t₂)
insert-sound x t (inr y∈t) = insert-sound₂ x t y∈t
where
insert-sound₂ : (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}}
→ (t : BST A lower upper)
→ y ∈ t → y ∈ insert x t
insert-sound₂ x (node y t₁ t₂) y∈t with tri x y
insert-sound₂ x (node y t₁ t₂) (here refl) | less x≤y = here refl
insert-sound₂ x (node y t₁ t₂) (left y∈t₁) | less x≤y =
let instance _ = x≤y
in left (insert-sound₂ x t₁ y∈t₁)
insert-sound₂ x (node y t₁ t₂) (right y∈t₂) | less x≤y = right y∈t₂
insert-sound₂ x (node y t₁ t₂) (here refl) | equal x≡y = here refl
insert-sound₂ x (node y t₁ t₂) (left y∈t₁) | equal x≡y = left y∈t₁
insert-sound₂ x (node y t₁ t₂) (right y∈t₂) | equal x≡y = right y∈t₂
insert-sound₂ x (node y t₁ t₂) (here refl) | greater x≥y = here refl
insert-sound₂ x (node y t₁ t₂) (left y∈t₁) | greater x≥y = left y∈t₁
insert-sound₂ x (node y t₁ t₂) (right y∈t₂) | greater x≥y =
let instance _ = x≥y
in right (insert-sound₂ x t₂ y∈t₂)
insert-complete : (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}}
→ (t : BST A lower upper)
→ y ∈ insert x t → (x ≡ y) ⊎ (y ∈ t)
insert-complete x leaf (here refl) = inl refl
insert-complete x (node y t₁ t₂) y∈t' with tri x y
insert-complete x (node y t₁ t₂) (here refl) | less x≤y = inr (here refl)
insert-complete x (node y t₁ t₂) (left y∈t₁') | less x≤y =
let instance _ = x≤y
in mapInr left (insert-complete x t₁ y∈t₁')
insert-complete x (node y t₁ t₂) (right y∈t₂) | less x≤y = inr (right y∈t₂)
insert-complete x (node y t₁ t₂) (here refl) | equal x≡y = inl x≡y
insert-complete x (node y t₁ t₂) (left y∈t₁) | equal x≡y = inr (left y∈t₁)
insert-complete x (node y t₁ t₂) (right y∈t₂) | equal x≡y = inr (right y∈t₂)
insert-complete x (node y t₁ t₂) (here refl) | greater x≥y = inr (here refl)
insert-complete x (node y t₁ t₂) (left y∈t₁) | greater x≥y = inr (left y∈t₁)
insert-complete x (node y t₁ t₂) (right y∈t₂') | greater x≥y =
let instance _ = x≥y
in mapInr right (insert-complete x t₂ y∈t₂')