Tutorial 2: Paths

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

true(bool) -> true

false(bool) -> false

Now is it time to learn how paths work.

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 others function 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".

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