Dynamic Path Semantics

Assume we have the following function in a dynamically typed language:

fn append(a, b) -> { ... }

We know that the function append returns a list with a length equal to the sum of the lists a and b.

Would it not be nice if the program checked this while executing?

This can be expressed with a dialect of path semantics called "Dynamic Path Semantics":

// Returns length of a list.
fn len(a) -> { ... }

// Check that `append` returns a list which length is the sum of its inputs.
fn append [len] ([len] a, [len] b) -> { a + b }

You could also check a specific case:

fn append [len] ([len] 2, [len] 3) -> { 5 }

Motivation

Dynamic path semantics is useful in dynamically typed scripting languages when:

• You want to design by contract
• Check that a program carries out the intended action
• Simulate type checking
• Disprove some mathematical theorem by experiment
• Prove some mathematical theorem by trying all inputs

Properties of Dynamic Path Semantics

These are the properties that distinguishes this variant from the general research topics on path semantics.

Asymmetric:

In symmetric path semantics, a function f [g] enforces [g] as a path on both inputs and output. Symmetric path semantics is useful to express identity equivalences such as f [g] = h.

One could solve the earlier problem using symmetric path semantics:

fn append [len] (a, b) -> { a + b }

However, for practical programming symmetric path semantics can be limiting.

Asymmetric path semantics allows you to express more powerful relations, such as "all men are mortal":

fn mortal(a) -> { ... }
fn man(a) -> { ... }
// Check that all men are mortal.
fn mortal([man] true) -> true

Non-propagating:

In a propagating path semantics, the paths are part of the return value. This is useful when you want to compute with the paths to predict what properties a program has by execution on the same source.

For example:

fn f([h] x) -> [h] { ... }
fn g([h] x) -> [h] { ... }

f(g([h] x))

It executes g([h] x) and puts a [h] in front of the return value on the stack. This "propagates" to the execution of f such that f([h] x) is used instead of f(x).

With other words, paths are first class citizens in a language with propagating path semantics.

The downside is that it requires a pattern matching stack machine, which is different from how normal scripting languages executes. Dynamic Path Semantics is therefore non-propagating.

Non-termed:

In termed path semantics functions as you know them in normal programming emerges from pattern matching on lower order functions. It is useful for working with the foundations of path semantics and foundations of mathematics.

// Starting at type level without paths.
// There is only one possible input and one possible output.
fn append(vec, vec) -> { u32 }
// Implementation of a function is equal to a pattern of inputs.
fn append([:] X, [:] Y) -> [:] { ... }
fn append([len] [:] X, [len] [:] Y) -> [len] [:] { add([:] X, [:] Y) }

In termed path semantics, instances of types are defined as lower order functions taking its type as argument and returning itself:

fn vec[1, 2, 3](vec) -> { vec[1, 2, 3] }

Therefore, when the value of X in [:] X is known to be vec[1, 2, 3], the [:] can be inferred to [vec[1, 2, 3]].

In dynamically typed languages, a type can be thought of as an property of a variable instead of an instance of a type.

fn typeof(x) -> { ... }

Therefore, if we want to express that a function returns a given type, we can write:

fn append [type_of] ([type_of] "array", [type_of] "array") -> { "array" }

Execution of Dynamic Path Semantics

In mathematical terms, we want to prove that for some input of a and b, there is some property that holds for append.

When we execute:

append(a, b)

it does the following check:

append [len] (len(a), len(b)) == len(append(a, b))

There is a safety requirement: The left side of == can have no side effects. Since len is without side effects, it is also safe to compute the right side by reusing the value of append(a, b).

Conditions and nested paths

A check is only active when the condition for the check holds.

For example:

fn append [len] ([len] a, [is_zero] true) -> { a }

If b has not a length 0, the condition of the first check fails. Since the condition fails, we do not know whether the expression on the right side holds.

Nested paths can be supported:

fn append [len] [is_zero] ([len] [is_zero] a, [len] [is_zero] b) -> { !a || !b }

Unsolved problems

• f [g] is ambiguous syntax with array indexing. Is there an alternative? Is not a problem when used in function declaration, though.
• Some arguments might be mutated, making it more difficult to express before/after.