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 integers always results in an even integer.

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

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

Then we look at the function that adds two integers:

add(integer, integer) ->| integer

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

2 is a member of the type integer:

2(integer) ->| 2

which is equal to:

2: integer

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

There are also infinite sums of two integers, so we just define that these atomic 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 integers always give an even integer.

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

Then we can put the [even] [:] in front to make it shorter:

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

We have expressed a mathematical idea!

One last rule: When writing [even] [:] X, one can also choose to write [:] [even] X. These two ways corresponds to two different ways of interpreting the path. The paths needs to commute in order to be used correctly:

[F] [:] X == [:] [F] X

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