Adjust the type checker for variables and exceptions

[maxkurze1]

Current type checking of Vars

Currently, the type checking works in the following way:

Take this action as an example:

let a := ... in
let b := ... in
a + b

which will create an AST similar to:

Bind "a" ... (Bind "b" ... (Add (Var "a") (Var "b")))

However, what is not shown here, each AST-element carries a list called sig which denotes all bound variables that it may access. In particular, each Bind adds its identifier to this list and each Var needs to contain a proof that its identifier is actually part of this list. (Other AST elements only pass the list on to its children)

Unfortunately, this structure is very unpleasant to type check. To empathize with the type checker, let's go through it step by step. First, we need to construct Var "a" and Var "b", however at this point the list of sig is still unknown so already at this point some magic is necessary to delay the construction of these terms. Add can be constructed easily ... let's suppose we leave its children as existential variables at first. Then the inner Bind "b" can be constructed with an unknown ?sig and passing ?sig :: "b" to its children. Finally, when we construct the outer Bind "a" (and for this one we are providing a sig of []) we can start to infer all other sigs. Only after this type checking, we have enough information to prove that "a" is in the sig of Var "a".

My suggestion

I would like to investigate a typed syntax where sig denote the set of free variables of a term instead.

By using this approach we can easily build and check smaller terms like Var "a" by simply adding their identifier to sig, normal terms would create the union set of their children and Binds would simply remove their identifier from the list. I would expect this change to reduce the complexity of the type checker, thereby enhancing its understandability and possibly also enabling the default coq typechecker to parse more complex term than currently supported.

Influence on exceptions

I would imagine exceptions as some kind of syntax sugar for if-then-else like this:

try (?a; if ?d then throw err; ?b) catch ?c => ?a; if ?d then ?c; else ?b

Here, one would have to make sure that every thrown exception is correctly caught, which basically boils down to the same mechanism as described for binding variables.

[sertel]

That is a very good suggestion. I like it but we still need to talk about the implications.

In Koika, the authors implemented Sigma via the type level. This is a known strategy to remove the complexity of maintaining Sigma at the term-level and guaranteeing that a variable is really defined inside the context.

It seems that you found a problem with this more general approach. And we need to clearly understand what that problem actually is. Let's chat about this in our sync.