# 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

imperativeandproceduralare used interchangeably. They are, however, two distinct paradigms of programming, albeit with a large overlap.

Imperativeprogramming 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.

Proceduralprogramming 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.

Both styles have all the parameters within parentheses

In C-style syntax, the types come first, followed by the name

In Pascal-style syntax, the names come first, and the types are separated by a colon

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.

In Haskell-style, the type signature and the names of the parameters are

*separate*ML-style is very similar to Pascal-style

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.