Compile time evaluation of paths

[bvssvni]

Using ty syntax from PistonDevelopers/dyon#636

By extending ty with support for paths and a new keyword chk, one can create a language that supports a subset of path semantics.

For example:

even(a: nat) = (a % 2) == 0

add(a: nat, b: nat) -> nat {...}
ty [even](false, false) = true
chk even(add(1, 3))

This works because:

even(add(1, 3))
even(add([even] false, [even] false))
even(add[even, even -> id](false, false))
add[even, even -> even](false, false)
add[even](false, false)
true

The output is compared to evaluating even(add(1, 3)).

Another example:

len(a: list) = { ... }
ty [:]([]) = 0

concat(a: list, b: list) = { ... }
ty [len](0, 0) = 0
chk len(concat([], []))

Another example:

even(a: nat) = (a % 2) == 0
eq(a: bool, b: bool) = a == b

add(a: nat, b: nat) -> nat {...}
ty [even] = eq
chk even(add(1, 3))

[bvssvni]

The theorem prover can first evaluate even(add(1, 3)) and then look for [_, _ -> even] which returns true. Then it evaluates (even(1), even(3)) and finds the case (false, false).

[bvssvni]

It could be required to cover every type information with some test, and cover every test with some type information.

The ty [even] = eq does not require checking this for every input of eq, but only for some input.

This only requires evaluation and comparing results, but gives a stronger guarantee than dynamic types. In addition the type information can be used to e.g. reduce add[even] to eq.