Navi's function are not guaranteed to be correct

[RunDevelopment]

In order for Navi to work, all functions (and function-like expressions) must guarantee the following property:

• Let A and B be valid inputs for a function f. If A ⊆ B, then f(A) ⊆ f(B).

This is a fundamental assumption I make, and it's currently not guaranteed.

The what

This is because match can be used to create the complement of a type. Example:

def compNumber(n: number) {
  match number { n => never, _ as c => c }
}
compNumber(number) // == never
compNumber(0..1) // == NaN | ..0 | 1..

Right now, this is limited by the limitations of match, but if we figure out a way to make the underlying without correct, then a true complement function will be as simple as this:

def comp(x: any) {
  match any { x => never, _ as c => c }
}

Obviously, set complement does not satisfy the above property.

The why

Why do we need this property in the first place?

This property guarantees that types and functions can be checked for correctness. With correctness, I mean that a type/function describes a valid program (all references can be resolved, functions calls are correct, no undefined types, etc.). The trick to verify them is very simple: given a function to validate, just run the function once with its input types as input. E.g. for a function def foo(a: number, b: string) { ... }, run foo(number, string). If all of Navi's functions have the above property, then this trick is enough to verify that the function will always return a valid output given valid inputs.

How to fix it

The condition for fixing this problem is the following: an expression is a valid match pattern iff it is not input-like. An expression is input-like if it is a function parameter or contains a reference to an input-like expression.

This condition is sufficient to ensure correctness.

However, this will be very annoying to implement. How references resolve, depends on the current scope, so we cannot verify this property without a scope. However, this property can (and should) be statically verified, not during evaluation.

I plan to add a more low-level AST some day. Navi is (an always be) an interpreted language, however, we interpret the parser AST pretty much as is, which has numerous downsides. Adding a more evaluation-focused AST format would make things easier. This AST format would resolve references when being created (instead of when being evaluated, so it should be relatively easy to do the static analysis for making functions correct.

[RunDevelopment]

@joeyballentine Could you please transfer this issue over to the Navi repo?