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 an 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 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

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

When the return value of a 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 becomes a building block for mathematics.