Idris is a one of those programming languages that empowers its users with the possibility to express very strong guarantees about the code they write before running it. It does this by using something called “Dependent Typing”, which is a very expressive kind of type system.

One of the guarantees you can get is to have safe arithmetic with
natural numbers (0, 1, 2, 3…). The interesting bit with Natural
numbers is that they cannot be negative, so the substraction `a - b`

only works if `b ≤ a`

. Idris actually forces you to make sure of that
before trying to run your code.

# Playing around with Nat

Let’s look at some code:

```
foo : Nat
foo = 4 - 3
```

Idris will gladly compile, then you can ask the value of `foo`

at the REPL to evaluate the result:

```
λΠ> foo
1 : Nat
```

Now if we try another case where `a`

is smaller than `b`

, then idris will not be happy:

```
foo : Nat
foo = 2 - 3
- + Errors (1)
`-- fun.idr line 17 col 8:
When checking right hand side of foo with expected type
Nat
When checking argument smaller to function Prelude.Nat.-:
Can't find a value of type
LTE 3 2
```

So it fails to compile, and tells you it cannot prove that 3 is smaller than 2.

That’s pretty neat! Now how smart is idris then? Let’s try!

```
foo : Nat
foo = (2 + 2) - 3
```

Yup! That works! Neat, so Idris can figure out that `2 + 2 ≥ 3`

at
compile time. Let’s try something harder: can we abstract over one of
the parameters?

```
foo : Nat -> Nat
foo n = n - 3
- + Errors (1)
`-- fun.idr line 17 col 10:
When checking right hand side of foo with expected type
Nat
When checking argument smaller to function Prelude.Nat.-:
Can't find a value of type
LTE 3 n
```

Ok so that makes sense: Idris is not happy because it cannot prove
that given any natural number `n`

, `n`

is smaller than `3`

. (for
instance, if `n = 2`

then that’s not true).

But wait…

```
foo : Nat -> Nat
foo n = (3 + n) - 3
```

OMG! Yep that compiles! So Idris manages to figure out that given any
natural number `n`

, `3 + n ≥ 3`

! That’s really cool!

It does that just by itself, without me having to prove anything.

# How does that work?

Let’s look a bit closer at the `-`

function:

```
λΠ> :doc (-)
Prelude.Nat.(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
infixl 8
The function is Total
```

The first line is the type of the function, and wow, it’s a bit more complicated than I expected… Let’s look at it closer:

`(m : Nat)`

and `(n : Nat)`

are the two arguments to the functions, so
we can read `(m : Nat) -> (n : Nat) -> ...`

as “given any natural number `m`

and any natural number
`n`

, …”.

The next part is this big thingy: `{auto smaller : LTE n m}`

. Let’s
unpack this a bit.

The curly braces `{}`

in the type means it’s an implicit parameter:
it’s not passed explicitely, and should be derivable from
context. `auto`

is a keyword that tells Idris to automatically derive
that parameter from context. So if we removed all that fluff, we could
rewrite the type like this:

```
Prelude.Nat.(-) : (m : Nat) -> (n : Nat) -> (smaller : LTE n m) -> Nat
```

Which would read like:

Given a natural number `m`

, a natural number `n`

, and a proof
“`smaller`

” that `n`

is less than `m`

, you’ll get a natural number
out.

The magic happens when adding the curly-braces and the `auto`

keyword,
as this proof can be found by Idris automatically.

OK maybe that’s a bit too much… Perhaps the best way is to try to re-implement all of that ourselves from scratch.

# Let’s build numbers from scratch

Let’s first define natural numbers. We can define them recursively, by
saying it’s either `0`

or the successor of another natural number:

```
data MyNat : Type where
MZ : MyNat
MS : MyNat -> MyNat
```

So `0`

is `MZ`

, `1`

is `MS MZ`

, `2`

is `MS (MS MZ)`

… That’s actually
how natural numbers are implemented in idris (using the digits
representation is just sugar).

So we can implement addition like this. First we declare the type of addition:

```
mplus : MyNat -> MyNat -> MyNat
```

It says “given a natural number and another natural number I’ll give
you another natural number”. From that and from your text editor, you
can ask Idris to add a placeholder body for the function definition
(in emacs, `C-c C-s`

)

```
mplus : MyNat -> MyNat -> MyNat
mplus x y = ?mplus_rhs
```

The part with a question mark is what needs to be filled. If you evaluate that code in idris (`C-c C-l`

), Idris will tell you something like this:

```
Holes
This buffer displays the unsolved holes from the currently-loaded code. Press
the [P] buttons to solve the holes interactively in the prover.
- + Main.mplus_rhs [P]
`-- x : MyNat
y : MyNat
------------------------
Main.mplus_rhs : MyNat
```

What this says is that there is a “hole” (`mplus_rhs`

) in your program
of type `MyNat`

, and that to fill that hole you have 2 parameters at
your disposition (`x`

and `y`

) with a similar type. But this doesn’t
allow us to define addition, so we can ask Idris to do a case split on
the first argument to see if we can get more things at our disposal.

In emacs you do that by putting your cursor on the first argument and
pressing `C-c C-c`

, resulting in this:

```
mplus : MyNat -> MyNat -> MyNat
mplus MZ y = ?mplus_rhs_1
mplus (MS x) y = ?mplus_rhs_2
```

Which after you load (`C-c C-l`

) you get:

```
Holes
This buffer displays the unsolved holes from the currently-loaded code. Press
the [P] buttons to solve the holes interactively in the prover.
- + Main.mplus_rhs_1 [P]
`-- y : MyNat
--------------------------
Main.mplus_rhs_1 : MyNat
- + Main.mplus_rhs_2 [P]
`-- x : MyNat
y : MyNat
--------------------------
Main.mplus_rhs_2 : MyNat
```

If we look at the first case, the first argument is zero. In that case
we just need to return the second argument (`0 + y = y`

). Since nothing is ambiguous here, we can even ask idris to fill that for us by putting the cursor on `?mplus_rhs_1`

and performing a “proof search” (pressing `C-c C-a`

):

```
mplus : MyNat -> MyNat -> MyNat
mplus MZ y = y
mplus (MS x) y = ?mplus_rhs_2
```

This went like this: when performing the proof search, Idris looked at
the type of the hole, and whatever was available from context that
matched that type (in this case, only `y`

was available), and used
that to fill the hole!

Pretty neat eh?

Now the second bit if we do the same we get the same result:

```
mplus : MyNat -> MyNat -> MyNat
mplus MZ y = y
mplus (MS x) y = y
```

Obviously Idris cannot read our mind. If we ask Idris to fill a hole
with a given type, it just provides the simple possible answer for
that, in this case `y`

.

Fine, let’s just use our human brains. We can use the property that `(1 + x) + y = 1 + (x + y)`

:

```
mplus : MyNat -> MyNat -> MyNat
mplus MZ y = y
mplus (MS x) y = MS (mplus x y)
```

We can try it out at the REPL:

```
λΠ> mplus (MS (MS MZ)) (MS (MS MZ))
MS (MS (MS (MS MZ))) : MyNat
λΠ> mplus (MS (MS MZ)) MZ
MS (MS MZ) : MyNat
```

OK it hurts the eye a little but we can see that `2 + 2 = 4`

and ```
2 +
0 = 2
```

.

Now let’s move to substraction. First the type:

```
mminus : MyNat -> MyNat -> MyNat
```

Then add the body automatically:

```
mminus : MyNat -> MyNat -> MyNat
mminus x y = ?mminus_rhs
```

Case split on the second argument:

```
mminus : MyNat -> MyNat -> MyNat
mminus x MZ = ?mminus_rhs_1
mminus x (MS y) = ?mminus_rhs_2
```

OK `x - 0 = x`

so we can fill the first case:

```
mminus : MyNat -> MyNat -> MyNat
mminus x MZ = x
mminus x (MS y) = ?mminus_rhs_2
```

For the second case we need to split again on `x`

actually:

```
mminus : MyNat -> MyNat -> MyNat
mminus x MZ = x
mminus MZ (MS y) = ?mminus_rhs_1
mminus (MS x) (MS y) = ?mminus_rhs_3
```

OK last case we can use the fact that `(x + 1) - (y + 1) = x - y`

:

```
mminus : MyNat -> MyNat -> MyNat
mminus x MZ = x
mminus MZ (MS y) = ?mminus_rhs_1
mminus (MS x) (MS y) = mminus x y
```

But the middle case is actually annoying: what is the answer to ```
0 -
x
```

for natural numbers? That’s annoying because natural numbers do not
contain negative numbers!

So we need to somehow constrain the input in such a way that this case
is impossible, i.e. we need to have a proposition that given `x`

and
`y`

, `y`

is smaller than `x`

.

# Building math from scratch

How do we do that? Actually similarly to how we defined natural numbers:

- Any natural number is larger than zero
- If
`n ≤ m`

, then`(n + 1) ≤ (m + 1)`

In Idris that translates to something like this:

```
data MyLTE : (m : MyNat) -> (n : MyNat) -> Type where
MyLTEZero : MyLTE MZ right
MyLTESucc : MyLTE left right -> MyLTE (MS left) (MS right)
```

So if you want to write `0 ≤ 2`

, you would write:

```
zeroLessThanTwo : MyLTE MZ (MS (MS MZ))
zeroLessThanTwo = MyLTEZero
```

If you want to write `2 ≤ 3`

, you would write:

```
twoLessThanThree : MyLTE (MS (MS MZ)) (MS (MS (MS MZ)))
twoLessThanThree = (MyLTESucc (MyLTESucc MyLTEZero))
```

So `MyLTE (MS (MS MZ)) (MS (MS (MS MZ)))`

is the proposition that ```
2 ≤
3
```

, and `(MyLTESucc (MyLTESucc MyLTEZero))`

is the proof that it’s
true.

Given this, let’s start over our definition of minus, this time
requiring a proof that `m ≤ n`

:

```
mminus : (m : MyNat) -> (n : MyNat) -> MyLTE n m -> MyNat
```

Add body:

```
mminus : (m : MyNat) -> (n : MyNat) -> MyLTE n m -> MyNat
mminus m n x = ?mminus'_rhs
```

This time we split on the proof (`x`

):

```
mminus : (m : MyNat) -> (n : MyNat) -> MyLTE n m -> MyNat
mminus m MZ MyLTEZero = ?mminus'_rhs_1
mminus (MS right) (MS left) (MyLTESucc x) = ?mminus'_rhs_2
```

Cool! This is where the “dependent type” magic happens: case splitting
on the proof has an effect on the arguments `m`

and `n`

: if the proof
you provide is `0 ≤ m`

, then clearly `n = 0`

, and if the proof you
provide looks like `(1 + x) ≤ (1 + y)`

, then clearly `m`

and `n`

are
not zero.

So let’s fill in some of the logic:

```
mminus : (m : MyNat) -> (n : MyNat) -> MyLTE n m -> MyNat
mminus m MZ MyLTEZero = m
mminus (MS right) (MS left) (MyLTESucc x) = mminus right left ?prf
```

If we look at the hole left for the proof in the recursive part of this function, we see this:

```
- + Main.prf [P]
`-- right : MyNat
left : MyNat
x : MyLTE left right
-----------------------------
Main.prf : MyLTE left right
```

There’s a hole of type `MyLTE left right`

and a parameter `x`

of type `MyLTE left right`

! Cool, perhaps we can just ask Idris to fill that up for us! (`C-c C-a`

)

```
mminus : (m : MyNat) -> (n : MyNat) -> MyLTE n m -> MyNat
mminus m MZ MyLTEZero = m
mminus (MS right) (MS left) (MyLTESucc x) = mminus right left x
```

Neat!! Now let’s try to use that method a bit:

```
foo : MyNat
foo = mminus (MS (MS (MS MZ))) (MS MZ) ?prf
```

This is `3 - 1`

with a hole for the proof.

The hole looks like this:

```
- + Main.prf [P]
`-- MyLTE (MS MZ) (MS (MS (MS MZ)))
```

OK… So how do we proceed? Let’s just ask Idris to see if it can figure out something (`C-c C-a`

):

```
foo : MyNat
foo = mminus (MS (MS (MS MZ))) (MS MZ) (MyLTESucc MyLTEZero)
```

AAAH! That worked! How is that possible? Actually Idris can try to
find proof by looking a the constructors available for the type of the
hole (in our case, `MyLTEZero`

and `MyLTESucc x`

) and try to build a
value using those constructors.

Neat!

# Hide the math!

So can we make that process automatic then? Yes if we introduce
the proof as an implicit parameter and add the `auto`

keyword! Let’s try:

```
mminus : (m : MyNat) -> (n : MyNat) -> {auto smaller : MyLTE n m} -> MyNat
```

Add the body:

```
mminus : (m : MyNat) -> (n : MyNat) -> {auto smaller : MyLTE n m} -> MyNat
mminus m n = ?mminus_rhs
```

Wait… Where’s the proof in the body? OK actually with implict parameters, you have to explicitely say you need them:

```
mminus : (m : MyNat) -> (n : MyNat) -> {auto smaller : MyLTE n m} -> MyNat
mminus {smaller} m n = ?mminus_rhs
```

Case split on the proof:

```
mminus : (m : MyNat) -> (n : MyNat) -> {auto smaller : MyLTE n m} -> MyNat
mminus {smaller = MyLTEZero} m MZ = ?mminus_rhs_1
mminus {smaller = (MyLTESucc x)} (MS right) (MS left) = ?mminus_rhs_2
```

And fill the rest:

```
mminus : (m : MyNat) -> (n : MyNat) -> {auto smaller : MyLTE n m} -> MyNat
mminus {smaller = MyLTEZero} m MZ = m
mminus {smaller = (MyLTESucc x)} (MS right) (MS left) = mminus right left
```

And now we can try again our substraction:

```
foo : MyNat
foo = mminus (MS (MS (MS MZ))) (MS MZ)
```

Sweet! And if we do something more funky:

```
foo' : MyNat -> MyNat
foo' n = mminus (mplus (MS MZ) n) (MS MZ)
```

Yep that still works! Neato. Wait so how about this:

```
foo'' : MyNat -> MyNat
foo'' n = mminus (mplus n (MS MZ)) (MS MZ)
- + Errors (1)
`-- fun.idr line 48 col 17:
When checking right hand side of foo'' with expected type
MyNat
When checking argument smaller to function Main.mminus:
Can't find a value of type
MyLTE (MS MZ) (mplus n (MS MZ))
```

Ah noes! That didn’t work… The reason for that is that Idris has no
idea that `3 + n = n + 3`

, and we’ve defined addition by case
splitting on the first argument…

Well, that’s for another time!

# Conclusion

I hope this gave you some idea of how powerful and the kind of guarantees that can be expressed in Idris and gave some insights on how things can be made practical (not having to provide or carry proofs when those proofs can be derived from context).