Tutorial 2: Paths

In the previous tutorial we described how types and members of types are connected.

true(bool) ->| true

false(bool) ->| false

Now is it time to learn how paths work.

Paths are the fundamental building block of how we express mathematical ideas in this notation. Some things will feel a bit familiar for mathematicians or programmers. It is based on a commonly used idea but extended for a more general case.

Before we can use it as a powerful tool, we need to look at how functions are interpreted. The end result is very much the same as in most programming languages, but it will give you a new insight.

Let us create another atomic function:

and(bool, bool) ->| bool

In most programming languages you would then add a function body.

In path semantics, a function body is a set of other functions related to a single function.

So, what is a path?

If we have bool, then we can call true(bool) and it will return true.

When we express that true has been called, we write [true] true.

If I give you bool, then you can give me back [true] true or [false] false.

With other words, there are only two possible "paths", one is [true] and another is [false].

A path is the stuff inside the square brackets!

If I give you and(bool, bool) -> bool, what can you give me back?

We insert all the paths that make up the and operations on values.

and([true] true, [true] true) ->| [true] true
and([false] false, [false] false) ->| [false] false
and([true] true, [false] false) ->| [false] false
and([false] true, [true] true) ->| [false] false

By using these definitions, and now corresponds to a normal function.

In the previous tutorial, you learned that a member of a type can be written true: bool.

When the return value of a atomic function leads back to itself, the path is implicitly known from the return value.

This means we can write:

and([:] true, [:] true) ->| [:] true
and([:] false, [:] false) ->| [:] false
and([:] true, [:] false) ->| [:] false
and([:] true, [:] true) ->| [:] false

Notice that only the first function returns [:] true.

Reading this from top to bottom, we can use pattern matching:

and([:] true, [:] true) ->| [:] true
and([:] _, [:] _) ->| [:] false

We can also factor out the [:] and write:

and [:] (true, true) ->| true
and [:] (_, _) ->| false

The _ character means "all other matches that so far has not matched yet".

When including the types, we can omit the name and simply write:

and(bool, bool) ->| bool
[:] (true, true) ->| true
[:] (_, _) ->| false

In the next tutorial, we will see how paths become a building block for mathematics.