The Haskell programmer is used to the pleasure of collaborating with a nice type system. Haskell itself hits quite a sweet spot of expressivity and manageability—type inference is (mostly) decidable, no subtyping, etc. However, in the past 30 years, new systems have been emerging that allow the user to encode many more properties at the type level. In fact, these systems are so expressive that they are often used as logical frameworks for mathematics rather than to write programs, and are thus often called “theorem provers” rather than “programming languages.” Thanks to a notorious correspondence, we know that these two activities are really the same.1
Agda is one of the most prominent systems of this kind at the moment. Many Haskell programmers like it because it has very functional slant, doing everything without recurring to mechanised transformation of terms (of which Coq is the most famous offender). In this blog I will try to give some examples that will hopefully make you interested. This first post explains how sorting algorithms can be proven correct. The implementation is largely inspired by a presentation by Conor McBride.
This blog post was generated from a literate Agda file, that you can find here. I’m not going to explain how to install Agda here, you can refer to the wiki or the wonderful freenode channel. While I go over all concepts presented I won’t go in depth to keep things reasonably brief: this is intended to get a taste of what Agda is capable of rather than explaining all its features. If you want to read a document meant to be a more comprehensive introduction, you can refer to the many tutorials available—personally I recommend Ulf Norell’s Dependently Typed Programming in Agda.
Let’s get started!
Lists #
module AgdaSort where
After the module declaration, let’s warm up by defining a data type dear to functional programmers:
infixr 5 _∷_
data List (X : Set) : Set where
[] : List X
_∷_ : X → List X → List X
The syntax to declare this type resembles the syntax for GADTs in Haskell. Here X is the parametrised type—what Agda calls Set is more or less what Haskell calls , the type of types, or “kind” in Haskell parlance. List is a type constructor which takes a type and “returns” a new type, List : Set → Set, much like Haskell’s [] :: → *.
Then we have two constructors, [] for an empty list and ∷ to cons an element to an existing list. Agda gives us great flexibility in the syntax: arbitrary operators can defined where indicates an argument, and identifiers are not limited to the usual mix of alphanumeric characters plus a few of symbols. In this case ∷_ is a binary operator. The fixity declaration is similar to what we would find in Haskell.
Let’s define foldr:
foldr : ∀ {A} {B : Set} → (A → B → B) → B → List A → B
foldr f b [] = b
foldr f b (a ∷ as) = f a (foldr f b as)
Nothing surprising here, apart from the fact that in the type signature we have to take the trouble of bringing the type variables into scope manually. In Agda, parameters in curly braces are implicit and the type checker will try to infer them by unification. This procedure can fail—term inference is predictably undecidable—in which case the implicits can be explicitly provided, also with curly braces. Here we are also omitting the type of the parameter A by using ∀. We can do this since A appears as an argument to List later in the signature. For the converse reason we must provide a type for B.
Now another “boring” type, Either, plus the associated destructor (either in Haskell):
data Either (A : Set) (B : Set) : Set where
left : A → Either A B
right : B → Either A B
[_,_] : ∀ {A B} {C : Set} → (A → C) → (B → C) → Either A B → C
[ f , g ] (left x) = f x
[ f , g ] (right x) = g x
Now for a type with no inhabitants—no constructors:
data Empty : Set where
What is Empty useful for? Well, if the user provides a term of type Empty, we can give back anything he might want, corresponding to the logical ex falso quodlibet:
absurd : {X : Set} → Empty → X
absurd ()
The () is what is called an empty pattern: Agda knows that no closed term will be of type Empty, and thus lets us leave out the body of functions with arguments of that type. Note that in Haskell we can easily get terms of any type in various ways, the most straightforward being general recursion:
undefined :: forall a. a
undefined = undefinedAgda makes sure that this is not possible,2 thus keeping the system consistent. This has very pleasant consequences, the most prominent being that all programs terminate. For this reason consistent systems must be Turing-incomplete (we can’t write an infinite loops!), and thus Agda lets us step out of these checks if we want to, although it is rarely needed—most algorithms we write are quite easily provably terminating. Note that consistency wasn’t put in Agda only to please mathematicians: given the expressivity of the type system type checking and evaluation are tightly intertwined, and thus we can send the compiler in an infinite loop if we can write one.
We use Empty to define something close to negation in logic:
infix 3 ¬_
¬_ : Set → Set
¬ X = X → Empty
For example we would expect terms of type ¬ (3 > 4) to exist. Here it starts being clear that types are very first class in Agda; functions can work on them as they do with ordinary values: in this case ¬ takes a type and forms another one.
Relations #
We need one last ingredient before we can start sorting. We could write our sort for some specific data type, say integers, but why would we do that considering that we have a language that lets us express abstract structures very naturally?
Instead, we can give a general definition for a binary relation on a type X:
Rel : Set → Set₁
Rel X = X → X → Set
The Set₁ indicates that a relation between two Sets is “larger” than a Set itself—this is nothing to worry about now, but it follows a tradition in set theory that goes back to Russell to avoid paradoxes.3 Set is in fact a shorthand for Set₀ and represents the type of types of values: Empty : Set₀ : Set₁ : Set₂ : ….
Then we define the type of decidable relations—we would expect relations like “less than” on natural numbers or “sortedness” on lists to be decidable:
Decidable : ∀ {X} → Rel X → Set
Decidable R = ∀ x y → Either (R x y) (¬ (R x y))
That is, a decidable relation has a function that tells us if any x and y are related or not.
Now the interesting part. To sort a list, we need two relations on the elements of the list: some notion of equality and some ordering on the elements (in fact the latter requires the former). More formally, the equality will be an equivalence relation. To express abstract properties over types we can use a record, much like type classes are used in Haskell—only more flexible but without the big advantage of having automatic instance resolution:
record Equivalence {X} (_≈_ : Rel X) : Set₁ where
field
refl : ∀ {x} → x ≈ x
sym : ∀ {x y} → x ≈ y → y ≈ x
trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
The definition on Wikipedia translates literally to Agda. Same story for our ordering, which will need to be total:
record TotalOrder {X} (_≈_ : Rel X) (_≤_ : Rel X) : Set₁ where
field
antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≈ y
trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
total : ∀ x y → Either (x ≤ y) (y ≤ x)
reflexive : ∀ {x y} → x ≈ y → x ≤ y
equivalence : Equivalence _≈_
We can finally begin to sort. To do this we will define a module parametrised over a type and an ordering. Agda has a very flexible module system—in fact we have already been using it by defining records, which are implicitly modules.
module Sort {X} {_≈_ _≤_ : Rel X}
(_≤?_ : Decidable _≤_) (ord : TotalOrder _≈_ _≤_) where
open TotalOrder ord using (total; equivalence)
open Equivalence equivalence using (refl)
We require the ordering relation to be decidable, and we bring in scope some fields of the records using open, so that we can use them directly.
We want to represent bounded lists, but we also want the bounds to be possibly open. For this purpose we lift our type X in a data type that contains a top and bottom elements, that are respectively greater or equal and lower or equal than all the other elements.
data ⊥X⊤ : Set where
⊤ ⊥ : ⊥X⊤
⟦_⟧ : X → ⊥X⊤
For ⊥X⊤ to be useful, we lift our ordering to work with it, following our considerations about the top and bottom elements:
data _≤̂_ : Rel ⊥X⊤ where
⊥≤̂ : ∀ {x} → ⊥ ≤̂ x
≤̂⊤ : ∀ {x} → x ≤̂ ⊤
≤-lift : ∀ {x y} → x ≤ y → ⟦ x ⟧ ≤̂ ⟦ y ⟧
Note that this data type is different from what we have defined before: the parameters to the type constructor can vary between data constructors—much like in GADTs in Haskell. In Agda, “changing” (more formally “non linear”) parameters are known as indices, as opposed to non-changing parameters. Parameters are named and to the left of the colon, while the type to the right of the colon will determine the number and type of indices—in this case two ⊥X⊤s (remember, Rel ⊥X⊤ = ⊥X⊤ → ⊥X⊤ → Set). This kind of data type is known as inductive family.4
We can now define the type of bounded, ordered lists:
data OList (l u : ⊥X⊤) : Set where
nil : l ≤̂ u → OList l u
cons : ∀ x (xs : OList ⟦ x ⟧ u) → l ≤̂ ⟦ x ⟧ → OList l u
nil will work with any bounds, provided that the lower l is less or equal than the upper u. cons will cons an element x to a list with x as a lower bound, and return a list with lower bound l, provided that l ≤̂ ⟦ x ⟧. It’s clear from how cons work that the elements in OList will be ordered according to the ≤ relation.
We can easily get a plain list back from an OList:
toList : ∀ {l u} → OList l u → List X
toList (nil _) = []
toList (cons x xs _) = x ∷ toList xs
With the right data types, writing and proving correct5 an insertion sort is a breeze—I encourage you to try and writing yourself checking the goals as you pattern match, the only non-trivial case being the last one:
insert : ∀ {l u} x → OList l u → l ≤̂ ⟦ x ⟧ → ⟦ x ⟧ ≤̂ u → OList l u
insert y (nil _) l≤y y≤u = cons y (nil y≤u) l≤y
insert y (cons x xs l≤x) l≤y y≤u with y ≤? x
insert y (cons x xs l≤x) l≤y y≤u | left y≤x = cons y (cons x xs (≤-lift y≤x)) l≤y
insert y (cons x xs l≤x) l≤y y≤u | right y>x =
cons x (insert y xs ([ ≤-lift , (λ y≤x → absurd (y>x y≤x)) ] (total x y)) y≤u) l≤x
Insertion sort is just a fold, where we use the type OList ⊥ ⊤ to represent a sorted list with open bounds:
isort′ : List X → OList ⊥ ⊤
isort′ = foldr (λ x xs → insert x xs ⊥≤̂ ≤̂⊤) (nil ⊥≤̂)
isort : List X → List X
isort xs = toList (isort′ xs)
Now for something more efficient, a tree sort. Firstly we’ll define a bounded, ordered binary tree:
data Tree (l u : ⊥X⊤) : Set where
leaf : l ≤̂ u → Tree l u
node : (x : X) → Tree l ⟦ x ⟧ → Tree ⟦ x ⟧ u → Tree l u
The technique is similar to that employed in OList. Then we need a procedure to insert an element in an existing tree:
newLeaf : ∀ {l u} → (x : X) → Tree l u → l ≤̂ ⟦ x ⟧ → ⟦ x ⟧ ≤̂ u → Tree l u
newLeaf x (leaf _) l≤x x≤u = node x (leaf l≤x) (leaf x≤u)
newLeaf x (node y ly yu) l≤x x≤u with x ≤? y
newLeaf x (node y ly yu) l≤x x≤u | left x≤y =
node y (newLeaf x ly l≤x (≤-lift x≤y)) yu
newLeaf x (node y ly yu) l≤x x≤u | right x>y =
node y ly (newLeaf x yu ([ (λ x≤y → absurd (x>y x≤y)) , ≤-lift ] (total x y)) x≤u)
Again, the only tricky bit is the last one, where we need to convince Agda that y ≤ x given that ¬ (x ≤ y).
Similar to isort′, turning a List into a Tree is a simple fold:
fromList : List X → Tree ⊥ ⊤
fromList = foldr (λ x xs → newLeaf x xs ⊥≤̂ ≤̂⊤) (leaf ⊥≤̂)
Now we can define OList concatenation, with the twist of inserting a new element in the middle; and finally flatten:
_⇒_++_ : ∀ {l u} x → OList l ⟦ x ⟧ → OList ⟦ x ⟧ u → OList l u
x ⇒ nil l≤u ++ xu = cons x xu l≤u
x ⇒ cons y yx l≤y ++ xu = cons y (x ⇒ yx ++ xu) l≤y
flatten : ∀ {l u} → Tree l u → OList l u
flatten (leaf l≤u) = (nil l≤u)
flatten (node x lx xu) = x ⇒ flatten lx ++ flatten xu
Then we are good with yet another fold.
treeSort′ : List X → OList ⊥ ⊤
treeSort′ xs = flatten (foldr (λ x xs → newLeaf x xs ⊥≤̂ ≤̂⊤) (leaf ⊥≤̂) xs)
treeSort : List X → List X
treeSort xs = toList (treeSort′ xs)
Now lets put our module to work. We will need a type equipped with the appropriate relations: in this post I am going to use natural numbers.
For what concerns equality, we can actually define an inductive family that relates equal terms:
module PropositionalEquality where
data _≡_ {X} : Rel X where
refl : ∀ {x} → x ≡ x
It’s worth mentioning what equal means here. I have mentioned earlier that “evaluation and typechecking are intertwined”: when the type checker has to decide if two types, or more generally two terms, are “the same”, it simply reduces them as far as possible (to their normal form) and then compares them syntactically, plus some additional laws.6 Remember, every Agda term is terminating, so this procedure itself is guaranteed to terminate. Thus, refl : ((λ x → x) 1) ≡ 1 is acceptable, and so on.
This notion of equality is often called definitional equality, as opposed to the user-level equality expressed by the inductive family we have just defined, which takes the name of propositional equality. Note that having a prop. equality in scope does not imply definitional equality for the related terms, unless the prop. equality is a closed term.7 In the general case we might have prop. equalities in scope that do not necessarily hold or involve abstracted variables, think of λ (p : 3 ≡ 1) → ….
Let’s prove that ≡ is an equivalence relation, and a congruence law which will be useful later:
sym : ∀ {X} {x y : X} → x ≡ y → y ≡ x
sym refl = refl
trans : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
equivalence : ∀ {X} → Equivalence {X} _≡_
equivalence = record { refl = refl; sym = sym; trans = trans }
cong : ∀ {X} {x y : X} → (f : X → X) → x ≡ y → f x ≡ f y
cong _ refl = refl
Here we use pattern matching in a new way: since the value of the indices of ≡ depends on the constructors, matching on a constructor refines the context with the new information. For example in sym pattern matching refl will unify y and x, turning them into the same variable in the context for the body of sym, and thus letting us invoke refl again. Pattern matching is a much more powerful notion in Agda that is in in most (even dependently typed) programming languages—it can not only change the context, but it will also constraint the possible constructors of other parameters, if they are of a type with indices and those indices have been refined. This collection of techniques is known as dependent pattern matching.
module Nat where
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
The definition for naturals is the usual one—the pragmas are there so that we can use number literals.
Now for our ordering relation. Every number is greater or equal than zero, and if x ≤ y then x + 1 ≤ y + 1:
data _≤_ : Rel ℕ where
z≤n : ∀ {x} → zero ≤ x
s≤s : ∀ {x y} → x ≤ y → suc x ≤ suc y
With the help of the dual of s≤s, we can write our decision function for ≤:
≤-suc : ∀ {x y} → suc x ≤ suc y → x ≤ y
≤-suc (s≤s x≤y) = x≤y
_≤?_ : Decidable _≤_
zero ≤? _ = left z≤n
suc _ ≤? zero = right λ()
suc x ≤? suc y with x ≤? y
... | left x≤y = left (s≤s x≤y)
... | right x>y = right (λ sx≤sy → x>y (≤-suc sx≤sy))
And the required laws to make a total order out of ≤:
open PropositionalEquality using (_≡_; refl; cong; equivalence)
antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y
antisym z≤n z≤n = refl
antisym (s≤s x≤y) (s≤s y≤x) = cong suc (antisym x≤y y≤x)
trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
trans z≤n _ = z≤n
trans (s≤s x≤y) (s≤s y≤z) = s≤s (trans x≤y y≤z)
total : ∀ x y → Either (x ≤ y) (y ≤ x)
total zero _ = left z≤n
total (suc x) zero = right z≤n
total (suc x) (suc y) with total x y
... | left x≤y = left (s≤s x≤y)
... | right y≤x = right (s≤s y≤x)
reflexive : ∀ {x y} → x ≡ y → x ≤ y
reflexive {zero} refl = z≤n
reflexive {suc _} refl = s≤s (reflexive refl)
totalOrder : TotalOrder _≡_ _≤_
totalOrder = record
{ antisym = antisym
; trans = trans
; total = total
; reflexive = reflexive
; equivalence = equivalence
}
Finally, we can import the sorting functions. We’re done!
open Sort _≤?_ totalOrder using (isort; treeSort)
We can test our function:
willIBeSorted? : List ℕ
willIBeSorted? = treeSort (12 ∷ 3 ∷ 7 ∷ 4 ∷ 40 ∷ 5 ∷ 0 ∷ [])
A tap on C-c C-n willIBeSorted? will give the expected result:
0 ∷ 3 ∷ 4 ∷ 5 ∷ 7 ∷ 12 ∷ 40 ∷ []This is my first decently-sized blog post, so please complain on Reddit!
For the interested, the logical core of most of said systems is an intensional Intuitionistic Type Theory.↩︎
Specifically:
data Mu f = Mu (f (Mu f)) in Haskell.
In type theory this is known as Girards’ paradox, you can find an Agda (with Set : Set enabled) rendition here.↩︎
Some might ask why Agda doesn’t treat all parameters uniformly, simply allowing indices at will. This is definitely an option (taken by other programming languages, and GHC’s GADTs) but separating them brings more clarity in the interface and lets Agda deal with inductive families more straightforwardly.↩︎
Some might rightfully complain that actually we are only proving half of the story, since we need to guarantee that the result list is a permutation of the input list to prove a sorting algorithm correct. That is doable but a bit more involved.↩︎
For example partial applications are expanded, so that if f : A -> B, then f ≡ λ x → f x. Similary, if we have a record Tuple (A B : Set) : Set with fields fst : A and snd : B, and constructor ,; if x : Tuple A B then x ≡ fst x , snd x. Apart from these η laws, other additions can be made to have more terms deemed as equal by the type checker, details vary from system to system.↩︎
This is the reason why we did not just use ≡ from the beginning and we instead chose to parametrise our equality relation: sometimes propositional equality does not cut it, for example when working with functions.↩︎