Tutorial 1: Types

Path semantics is a way of re-interpreting functions to express mathematical ideas.

What makes path semantics special is that type membership is replaced by a "path" mechanism. This mechanism allows for expressing more flexible relationships between functions. The meaning, or semantics, is such that many mathematical statements can be expressed in a short and concise form.

A "path" can be formal in mathematics, but also informal. It can be hard to wrap your head around this idea, because it is very powerful. There are not just one kind of paths, but many.

Explaining what a "path" means in general is kind of like explaining Zen. In fact, many religions started out naming themselves "The Way", or something like that, before choosing another name. When studying mathematics, paths occur everywhere and yet there is no single best method to describe them. This is a problem that only can be solved by more research.

This tutorial introduces a notation using path semantics, showing how to describe type membership, logical gates and equivalence. The approach used here is to arrive at formal reasoning through informal means.

A bool type has two members, true and false:

bool = { true, false }

What does it mean that a type has members?

First, it is useful to learn about the idea of exponential objects. An exponential object A -> B is an arrow from one object A to another object B. There can be several kinds of exponential objects in a language. It is common to use different symbols for different kinds of arrows.

An atomic function is an exponential object, similar to a function, which only has one input and one output. To avoid confusion between atomic functions and normal functions, I will use ->| for atomic functions.

Path semantics defines this meaning as each member being an atomic function taking the type as argument returning itself:

true(bool) ->| true

false(bool) ->| false

Type members are atomic functions, because there can only be only one type per member.

Atomic functions prevent a member from belonging to different types, e.g:

true(bool) ->| true
true(nat) ->| true

This is not valid since true is defined multiple times with different inputs.

To prevent Burali-Forti's paradox, the following convention is used for types:

bool(type{0}) ->| bool

type{n}(type{n+1}) ->| type{n}  where n(nat) ->| n

An alternative way is to write:

true: bool
false: bool

If I tell you X: bool then you know that X must be either true or false.

After all, true and false are the only atomic functions that take bool and return themselves.

Given true, it is known that true has the form (bool) ->| true.

In the second part we will create paths from one function to another.