Agda: What Even is Propositional Equality?

I would like to apologise in advance for the inevitable semantic satiation you will experience when reading the word “type” in this post. Sorry.

If you ever read or write Agda, you will come across the following import statement in practically every piece of code you read:


open import Relation.Binary.PropositionalEquality

Followed by things like:


1+1≡2 : 1 + 1 ≡ 2
1+1≡2 = refl

Equality in Agda is a fundamental part of its proof system, but the definition can be a bit mind-warping. So, let’s explore what it means for things to be equivalent in Agda.

Function signatures and types

To understand what equality means and how it is written in Agda, we must first understand how type signatures work in functional languages. If you are already familiar with them, you can skip this section.

Most programmers come from a procedural background, and procedural languages tend to use a syntax for functions descended from either C or Pascal.


int add(int a, int b);


function add(a: int, b: int): int;

Sometimes the terms imperative and procedural are used interchangeably. They are, however, two distinct paradigms of programming, albeit with a large overlap.
Imperative programming refers to the use of sequential statements to change a program’s state. It focuses on describing exactly how the program works, step-by-step.
Procedural programming refers to languages that use procedures (a.k.a. functions (a.k.a. subroutines (a.k.a. methods (a.k.a. …)))) Each procedure contains a sequence of instructions to be executed.
Many languages are both.

Let’s compare and contrast quickly.

It follows from those last two points that the return type of the function goes either before or after the name, the same as with parameters and variables. Furthermore, when making function calls in these languages, one has to provide all the parameters at once.

In addition to function signatures, these languages also often have associated function types:


typedef int int_2adic(int, int);


type Int2Adic = function(a: int, b: int) : int;

These function types follow the same pattern as the signatures themselves.

The procedural way is not the only way Within functional programming, there are also two main styles — Haskell-style, and ML-style.


add :: int -> int -> int


let add (a: int) (b: int): int = a + b

Again, let’s compare these.

The ML-style function requires a body because the signature is inseparable from it. By comparison, the Haskell-style one does not; we can just declare a function of some type.

As well as signatures, functions in functional languages also have types — and this is far more important in these languages, where higher-order functions are extremely common. Both of them use the same syntax, derived from mathematics:


int -> int -> int

This is exactly what is on the right-hand side of the :: in Haskell-style syntax. In fact, :: in Haskell descendants just specifies the type of the term to its left. add :: int -> int -> int is just declaring a value named add with the given type, which happens to be a function. The ML-based languages use this too, but do not display it as explicitly in every function definition.

There’s a key difference with functions in functional languages compared to procedural ones, and it’s hinted to by these arrows. In the procedural languages, the parameters were all grouped together. In the functional languages, the parameters are separated by arrows.

To explain further, let’s consider a 1-adic function:


int -> int

This function takes one parameter and returns a result. You may notice that it looks like the end of 2-adic function signature, too.


int -> int -> int
       int -> int

That’s because it is — the 2-adic function is curried. Curried functions take their parameters one at a time, yielding a new function that takes the next until finally all the parameters have been given and the function can return its result.

There are advantages to this style of function which I won’t go into here (maybe another time?) but are very interesting in their own right.

Agda’s signatures are very similar to

Now that that’s out of the way, we can move on to the interesting concepts that follow from it in Agda.

Types and functions in Agda

In Agda, types are defined by using the keyword data. Being from a mathematical background, Agda refers to a type as Set. If you prefer, you can just think of every instance of Set as saying Type instead. For example, here’s a definition of bools:


data Bool : Set where
  true false : Bool

This is defining two constructors for Bool. Each of these has type Bool — no additional information is needed to construct the type. true and false can be used straight away as two values belonging to the type Bool.

Note that we have not defined any behaviour for Bool yet! That is up to us to do — things like Boolean algebra aren’t magically granted to any type with constructors called true and false, but they do exist in the standard library.

Functions can be defined in a similar method to languages like Haskell:


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

Here, the underscores represent where the operands will go. The function is defined by pattern matching on the first operand, to cover all possible cases.

Parametric types

Types in Agda can be more complex, too. Just as functions in functional languages can take parameters, so can types in Agda. As a basic example, here’s the popular Maybe (or Option) type:


data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

Our types just got more advanced! This one takes a parameter, A, which is another Set, and produces a Set. The type on the left-hand side of that colon indicates that it is an input to this type; in a way, Maybe is a Set → Set function. Furthermore, A is the name bound to this parameter, which lets us use it later.

The nothing constructor isn’t too dissimilar from true or false; by this point, all the required information has been provided, so it is just a value.

just is more involved — it needs a value of type A to make a Maybe A. In other words, just is a function from A to Maybe A, hence the signature. We can create instances of this type by using the constructors, just as with Bool:


nothing-Bool : Maybe Bool
nothing-Bool = nothing


just-true : Maybe Bool
just-true = just true


just-false : Maybe Bool
just-false = just false

Going even further beyond

So far, our types have been based purely on other types at most. Bool, the simplest case, didn’t depend on anything. Maybe required another type to construct.

Types could depend on values, as well as types. This is what it means to be dependently-typed. As a dependently-typed language, Agda supports this kind of type.

Enter the definition of propositional equality (with some simplifications for the sake of introduction). Equality is a type that represents two things being identical. It is called propositional because for Agda to be able to check the type, the very definitions of the two sides must be the same.


data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

This is a pretty complex type, so the rest of the article will be explaining the collection of concepts going on here all at once, and what they entail.

Starting on the left, equality is called _≡_ in Agda; a triple equals symbol, with an operand either side. Then, we get the first parameter, {A : Set}. Compared to the parameters we have seen so far, this one is in braces! Braces around a parameter mark it as implicit, i.e., the type checker will attempt to infer the relevant type. There is almost always enough information present for this to happen when the type is being used in its intended fashion.

The next parameter is (x : A). A is a type, so that means that x is a member of A — it is a value, not another type. This is what makes equality dependently-typed in Agda.

Given these two inputs, we are given the signature for the type itself, which is a function! A → Set means that we must be given a second value of type A to complete the construction of this type. Just as providing one parameter to a function in a functional language produces a new function that takes the rest of the parameters, giving a type A implicitly and a value x explicitly gives us a function to construct the type with.

In fact, the whole type can be thought of like a curried function. The first parameter is the implicit Set which is being tested, followed by the left-hand value. The last parameter is provided on the right-hand side of the ≡.

Now read there is a single constructor, called refl. The type of refl is x ≡ x. This means that to create an instance of this type, the type checker must prove that the value on the left-hand side of the ≡ is the same as the value on the right-hand side. In return for proving this, we are given an instance, refl, which serves as evidence that this is true — having a copy of refl somewhere in your inputs means you know two things must be the same. This evidence can then be used in other proofs without repeating the whole chain of reasoning that derives it, or knowing anything more about the values. I’ll be exploring the concept of evidence further in later posts.

Logically, it makes sense that the definition of equality is that any value is identical to itself. This property is called reflexivity, and is the reason that the constructor is called refl. If we have two values that look different at first, but can be shown to be equivalent, then refl can be used to construct equality. If they can’t, then we can’t use refl — so there is no evidence, and no proof!

While this may not seem like a useful tool at first, the real power comes from how we manipulate the left-hand side to create this instance. By applying properties known to the type checker, it can be guided through the steps to show that two different expressions are in fact the same.

A simple pair of examples

Let’s use our Bool type from earlier and prove something evident from the definition of _and_.


and-false-identity : ∀ {b : Bool} → (false and b) ≡ false
and-false-identity = refl

∀ means for all — the compiler must show this property holds for every possible value. Again, the braces mean that the value of b itself is implicit. This pattern of providing the values of types implicitly in Agda is common — more of the attention is given to the evidence that a property holds than the values themselves. It also helps avoid syntactic noise in proofs.

The proof of this property should be fairly easy to follow; we start by asserting what we want to prove. Then, we examine all the possible cases for the thing on the left, and check that they match the right.

Here, our left-hand side is false and b. Consulting the definition of _and_, we get false and _ = false. Hence, the left-hand side must be false, which is the same as false on the right, so we are allowed to use refl.

Similarly, we could show and identity for true:


and-true-identity : ∀ {b : Bool} → (true and b) ≡ b
and-true-identity = refl

This also follows straight from the definition of _and_.

So what?

While we haven’t done anything complicated logically yet, there’s a lot of syntax to unpack here. Using the dependent type system, we have managed to construct a type that represents two values being exactly equivalent. Much of the art of Agda involves applying properties in some order to show that two things are identical.

The advantage of this is formal verification.

Lots of code is testable. Lots of tests check for a few simple values or use a table of outcomes. We can assert that 1 + 1 == 2 and 1 + 2 == 3 and 1 + 3 == 4 and so on and so forth.

More sophisticated testing frameworks use something called property-based testing, which seeks to assert that some property holds for all inputs. However, most languages cannot exhaustively test all possibilities; it would simply take too long to be sensible. Instead, they generate random examples to try and cover a wide variety of cases. While better than hand-picked inputs, it would be better if any problems could be systematically ruled out, the same way compilers verify the types in statically-typed programs.

Enter Agda.

Agda allows for this to happen. Checking that properties hold is type checking, and uses the same machinery. Eliminating edge cases can be done by defining invariants and proving that they hold under all cases.

Types in Agda are almost always built inductively — there is a base case, and a step from one case to the next. If you can prove something holds for the base case, and it holds whenever you take that step, you have proved it holds for all possible values! This concept, induction, is so powerful that it is used widely for proofs in mathematics. I’ll be covering this in a later article, too.

Agda, and languages like it, bring that technique to computer science and programming. Via the Curry–Howard correspondence, mathematical proofs and things shown by Agda’s type system are isomorphic — one can be mapped to the other, and vice versa! With this power, it is possible to prove that code will always behave a certain way. No randomness, no human-generated examples, no untested edge cases. Just machine-verifiable properties.

Unfortunately, with great power come a great many problems.

First and foremost, interacting with the outside world is hard! Without going into huge detail, Agda asserts that programs must be total — they must terminate. Furthemore, reading files could theoretically yield an unbounded quantity of data; this is dealt with by special data types that allow for termination checking. These added complexities make it quite trickly to write an “interactive” (the Agda name for something that deals with the outside world) program. There are some resources for this class of problem, but it is not widespread among Agda programmers. I have been advised to try Idris for a similar language that is better oriented for programming in.

Secondly, the performance is not currently very good. The two current backends both have their limitations that hold it back. This is an area of active work, though, so there may be interesting developments soon!

Conclusion

Briefly, we have explored the definition of equality in Agda. This blog post serves as a primer to Agda materials that assume that you know what its version of equality is, but I also try to explain how it works.

If you’re interested in more Agda writing, watch this space — I plan to write more soon.

Some types in this post have been simplified slightly from their definitions in the standard library to avoid having to discuss the sort system and universe levels. If you are a set theorist who is worried about Russel’s paradox, don’t lament — Agda has a solution!
Furthermore, the type of equality presented here is known academically as Martin-Löf Identity.