Tutorial 3: Mathematics

In the previous tutorial you learned that paths can express function bodies.

We can also use paths to express mathematical ideas.

Let us do this with the following:

Adding two even numbers always results in an even number.

First we write a function that defines what we mean about "even":

even(number) -> bool
[:] (X) -> ( X % 2 == 0 )

Then we look at the function that adds two numbers:

add(number, number) -> number

In the first tutorial, you learned how types and members of types are related.

2 is a member of the type number:

2(number) -> 2

which is equal to:

2: number

Even there are infinite numbers, we pretend that for every value, a member function exists.

There are also infinite sums of two numbers, so we just define that these functions exist too!

Let us try some values with add:

add([:] 2, [:] 3) -> [:] 5
add([:] 2, [:] 4) -> [:] 6
add([:] 2, [:] 5) -> [:] 7
add([:] 3, [:] 4) -> [:] 7
add([:] 3, [:] 5) -> [:] 8

Notice that adding two even numbers always gives an even number.

How do we express this with paths?

If we use even as a path, we get the following:

add([even] bool, [even] bool) -> [even] bool

We can also use this trick more than once!

You can replace bool with [:] true or [:] false, right?

So, if I give you a number, you can give back [even] [:] true or [even] [:] false.

We can write:

add([even] [:] true, [even] [:] true) -> [even] [:] true

We have expressed a mathematical idea!

In the next tutorial we will expand on this technique to equivalence.