Imp: solving functions

Published 2020-04-29

This is a part of a series - start at the beginning.

Here is some imp code that does a reverse lookup on a table:

This is kind of verbose - worse even than the equivalent sql:

select name
from departments
where department = "marketing"

This is a problem, because one of the design goals of imp is to make it easy to work with data in 6NF where these key-value relations are all over the place.

There is a much nicer way to write this in imp:

This even reads nicely as "names such that the department for that name is marketing".

Unfortunately the type system cannot prove that this evaluates to something finite, so the repl refuses to evaluate it.

But it's easy to reason by looking at this expression that its value must be finite, because the body of the function is none whenever name does not exist in the first column of departments, and we know that departments is finite.

Let's tell the compiler to use the same kind of reasoning.

This ? operator is pronounced "solve", because it often appears in this kind of "find all names such that..." pattern. It tells the compiler to try to prove that the expression has a finite value using a more complex algorithm than the simple syntax-directed type system used elsewhere.

This algorithm only has access to the expression in question and to the types of everything in scope. This ensures that changes to upstream code that preserve the types can't break downstream uses of solve. (This is similar to the rationale for requiring top-level type annotations in Rust - global unconstrained type inference can be surprisingly unstable).

Ideally, there would be a clear set of rules defining when this algorithm will succeed and clear compile-time error messages when it doesn't. But I've been sitting on this post for months, so for now the algorithm is just:

I'll come back to this when it starts to annoy me.