Agda

The best programming language ever made is Agda. I know that is a bold statement, but I will do my best to persuade.

Agda is a dependently typed programming language which also functions as a proof assistant, it’s special because the core type theory behind it is the most complete out of anything else out there.

Completeness is important because it means you don’t have to rely on assumptions and unsafe behavior, if you want to do something correct the language will not hold you back.

When learning type theory the first thing that blew my mind was the Curry-Howard correspondence which is an observation that types are equivalent to theories, and function bodies are equivalent to proofs.

Most programming languages have a type system that is not particularly useful for proofs. In languages like Java you can declare a valid function that returns types that can’t be constructed (with null or throwing an error):

public abstract class Foo { private Foo() {} }

Foo bar() { throw new RuntimeException(); }

This is bad because the definition of bar essentially says “Given nothing, I can create Foo”, a contradiction!

What makes a type system useful here is ensuring that you can only declare functions that can actually satisfy their output. The primary culprits to eliminate are side effects, recursion, null, and exceptions.

Essentially, if you have a function that takes in A as a parameter and returns a B, you’ve proven that A implies B with formal logic.

Now that I’ve convinced you this is not just an elaborate way to ensure job security for mathematicians, I present you some of the reasons Agda is the best language ever made. :-)

Primer¶

Agda is extremely light on primitives, you start out with just Set aka types and Level which is a way to sort higher-order types (more on that later). Most of the other primitives implemented by the compiler are for performance and interactivity, but you can do just as much without them!

Let’s start with a basic data type:

-- A type for natural numbers
data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

-- We create numbers by applying `suc` to `zero` or another number
one = suc zero
two = suc one
three = suc two

The code above declares a new type Nat of type Set with two constructors, zero and suc.

The zero : Nat constructor has zero arguments, it’s essentially an enum value. The suc : Nat -> Nat constructor takes any Nat and returns a Nat.

What trips most people up here is that data in Agda consists of abstract terms and function calls, not real values in the traditional sense. You can think of the constructors as functions that don’t reduce, e.g. normalizing three gives us the term suc (suc (suc zero)).

To discriminate between numbers we do some pattern matching:

-- Check if a number is zero
isZero : Nat -> Bool
isZero zero = true
isZero (suc _) = false

You have probably only worked with types that are trivial to construct, “Nat implies Bool” doesn’t seem like a very useful proof because we can just create a Bool ourselves. Where formal proofs really come into play is with parameterized types:

-- A type for all proofs `NonZero n` where `n` is greater than zero.
data NonZero : Nat -> Set where
  nzOne : NonZero one
  nzSuc : {n : Nat} -> NonZero n -> NonZero (suc n)

Here we declare a type NonZero with a Nat parameter, but the way the constructors are set up means NonZero zero can never exist.

This is also an example of how to use implicit parameters (the ones surrounded in curly braces), they are like regular parameters but get filled in automatically with magic, kinda like type inference.

You can also think of parameters as a “for all”, so {n : Nat} -> NonZero n -> NonZero (suc n) can be interpreted as “for all n and 0 != n, 0 != n + 1”.

We can pattern match on implicit arguments too, here nz converts a Nat to a NonZero:

-- Create a NonZero for any `suc n`
nz : {n : Nat} -> NonZero (suc n)
nz {zero} = nzOne
nz {suc n} = nzSuc nz

The compiler is smart enough to take an expected return type like NonZero (suc (suc (suc zero))) and pass suc (suc zero) to n:

-- Proof that 3 != 0
threeNz : NonZero three
threeNz = nz -- Equivalent to nz {two}

What if we want to prove something is not true? Well, something is false if it implies something that can never be true, like the bottom type.

The same mechanism Agda uses to determine if a pattern match is complete is also used to determine if a case is impossible (matches no constructors):

-- A type with no constructors that can never be created, aka the bottom type
data Never : Set where

-- Proof that 0 != 0 is impossible
zeroNz : NonZero zero -> Never
zeroNz () -- No constructors can possibly match so we use the absurd pattern `()`

If you want to play around some more I recommend reading PLFA, it’s a much more hardcore introduction though.

Operators¶

Declaring custom operators is stupidly simple, just add an underscore where the parameter sits:

_$_ : (A -> B) -> A -> B
f $ a = f a

There are very few restrictions on the characters you can use in an operator, the standard library is full of incomprehensible Unicode, it’s great!

This works on data and constructors:

data _*_ A B : Set where
  _,_ : A -> B -> A * B

Pair = _*_

example : Nat * Nat
example = 69 , 420

The way you apply arguments to an operator is pretty flexible too:

NatAnd : Set -> Set
NatAnd = _*_ Nat -- As function

natAndExample : NatAnd String
natAndExample = 69 , "Sixty Nine"

_AndNat : Set -> Set
_AndNat = _* Nat -- Partial operator application

andNatExample : String AndNat -- Suffix operator
andNatExample = "Four Twenty" , 420

Types are expressions¶

A type in Agda is also an expression, that means we can declare functions that return arbitrary types and use them anywhere:

Two : Set -> Set
Two a = a * a

example2 : Two Nat
example2 = 69 , 420

This isn’t just some limited subset of the language either, you can use any function to produce a type, even a brainfuck interpreter:

StrType' : List Set -> List Char -> Set
StrType' (t :: []) [] = t
StrType' s ('n' :: n) = StrType' (Nat :: s) n
StrType' s ('s' :: n) = StrType' (String :: s) n
StrType' (b :: a :: s) ('p' :: n) = StrType' (Pair a b :: s) n
StrType' (a :: s) ('l' :: n) = StrType' (List a :: s) n
StrType' _ _ = Never

-- Turns a string into a type, for example "nsp" becomes Pair Nat String
StrType : String -> Set
StrType code = StrType' [] (stringToChars code)

-- Run some brainfuck code that prints "nspl" and use StrType to turn that into List (Pair Nat String)
Foo : StrType (runBF ">++>++>+[>+[-<++++>]<<]>.+++++.---.----." "")
Foo = [ (69 , "Sixty Nine") , (420 , "Four Twenty") ]

The magical part is that dependent types allow the type signature of a function to depend on one of its parameters, for example:

someVal : (a : Bool) -> a then Nat else List Nat
someVal true = 69
someVal false = [ 420 ]

This works because the result type is lazily unified with constraints applied by the pattern match, allowing each case to return something different.

There are so many wonderful horrors you can create with dependent types, more to come.

Turing incomplete¶

I like following up “Agda can do more than any other language” with “Agda isn’t actually Turing complete” which causes everyone to lose their minds.

In all seriousness, this is an essential property of any formally verified code, and it doesn’t limit what you can do with the language either, as I will demonstrate.

The runBF function from before had a fixed number of iterations:

stepn : Nat -> State -> State
stepn 0 state = state
stepn (suc n) state with step state
... | nothing = state
... | just next = stepn n next

run' : Inst -> List Nat -> List Nat
run' inst input = reverse (State.output (stepn 10000000000000 (newState inst input)))

This looks scary but sort of works fine in practice, if you made that magic number big enough (larger than the amount of energy in the universe), Agda becomes just as Turing-capable as Java or C!

You can also cheat by telling the compiler a function terminates when it doesn’t:

-- Disable termination checking with an unsafe pragma
{-# TERMINATING #-}
stepForever : State -> State
stepForever state with step state
... | nothing = state
... | just next = stepForever next

-- We can prove anything using an infinite loop
{-# TERMINATING #-}
assumption : {A : Set} -> A
assumption = assumption

This fails to compile when you pass --safe for obvious reasons, you should always write your functions to appease the termination checker and only use {-# TERMINATING #-} as a last resort.

Termination checking is really simple, a function can only call itself if it passes a subset of its arguments:

stepn : Nat -> State -> State
stepn 0 state = state
stepn (suc n) state with step state
... | nothing = state
 -- This recursive call to stepn uses `n`, which is smaller than the argument `(suc n)`
... | just next = stepn n next

All programs in the real world are bound by address space so nothing is truly Turing complete, and the fact that we can do useful stuff without loops proves what I’ve been saying all along: Turing was wrong, loops aren’t real.

Universes¶

Classic set theory has a few paradoxes, the most famous of which is Russel’s paradox. I’m not going to bore you with the details but it’s a funny quirk that requires types (sets) to be ordered and not self-referential.

-- The type of Set is Set1, so a set can't contain itself
Set : Set1
Set1 : Set2
Set2 : Set3

What makes Agda unique among dependently typed languages is that arbitrary expressions can specify a universe level:

levelAdd : Nat -> Level -> Level
levelAdd 0 l = l
levelAdd (1+ n) l = levelSuc (levelAdd n l)

data Example (n : Nat) : Set (levelSuc (levelAdd n levelZero)) where
  example : Set (levelAdd n levelZero) -> Example n

example2 : Example 1
example2 = example (List Set)

The above example has a data type Example which is a universe level specified by a natural number, followed by an instance that proves it can be constructed.

But that isn’t enough, what if you wanted to pass Example to another type? Say hello to omega sets!

data OmegaExample : SetOmega1 where
  omegaExample : SetOmega -> OmegaExample

example3 : OmegaExample
example3 = omegaExample ((n : Nat) -> Example n)

Omega sets contain an infinite number of smaller sets, so function types like (l : Level) -> Set l are SetOmega, and types containing SetOmega are part of the higher infinite set SetOmega1, which also go on forever.

While we do have universe polymorphism and infinite universes, Agda is missing infinite universe polymorphism, truly unplayable, valve pls fix.

JavaScript¶

Agda supports JS as a backend, so the safest language ever made can run on top of the least safe language ever made!

The mapping from Agda to JS is pretty simple, here is a basic natural number with an add function:

data BigInt : Set where
  zero : BigInt
  suc : BigInt -> BigInt

add : BigInt -> BigInt -> BigInt
add zero y = y
add (suc x) y = suc (add x y)

This compiles to the following JS:

exports["BigInt"] = {};
exports["BigInt"]["zero"] = a => a["zero"]();
exports["BigInt"]["suc"] = a => b => b["suc"](a);
exports["add"] = a => b => a({
    "suc": c => exports["BigInt"]["suc"](exports["add"](c)(b)),
    "zero": () => b
});

Sum types are really functions that take a map of constructors to match, neat.

With pragmas we can replace this inefficient implementation with one that’s backed by a JavaScript BigInt:

{-# COMPILE JS BigInt = ((x, v) => {
    if (x == 0) {
        return v["zero"]();
    } else {
        return v["suc"](x - 1n);
    }
}) #-}
{-# COMPILE JS zero = 0n #-}
{-# COMPILE JS suc = n => n + 1n #-}
{-# COMPILE JS add = a => b => a + b #-}

Instance Arguments¶

Instance arguments are the Agda equivalent to Haskell typeclasses but a bit more flexible since they’re also implicit arguments.

When a function needs an instance argument the compiler looks for instances (marked with instance) in the current context that satisfy it.

Here we declare a record Num A with methods for doing basic arithmetic:

record Num (A : Set) : Set1 where
  field
    fold : {B : Set} -> B -> (B -> B) -> A -> B
    numZero : A
    numSuc : A -> A

-- Generic addition
_+_ : {A : Set} {{n : Num A}} -> A -> A -> A
_+_ {{n}} x y = Num.fold n x (Num.numSuc n) y

-- Generic multiplication
_*_ : {A : Set} {{n : Num A}} -> A -> A -> A
_*_ {{n}} x y = Num.fold n (Num.numZero n) (_+_ {{n}} x) y

These addition and multiplication operators will look for an instance of Num A when you call them, so to use them with natural numbers we just create a Num Nat:

-- Folds over a Nat
foldNat : {A : Set} -> A -> (A -> A) -> Nat -> A
foldNat t _ zero = t
foldNat t f (suc n) = f (foldNat t f n)

instance
  -- Our implementation of Num Nat
  numNat : Num Nat
  numNat = record
    { fold = foldNat;
      numZero = zero;
      numSuc = suc }

five : Nat
five = two + three

ten : Nat
ten = five * two

There’s much more you can do with it though, the implicit argument resolution algorithm is pretty advanced. It’s recursive and can even resolve implicit arguments containing higher-order types while satisfying an instance!

Reflection¶

Honestly the language is so powerful I have trouble even coming up with a simple use case for reflection.