Claudio/check ir

[crusso]

A type-checker for IR.

Removes some unused effect annotations from syntax, adds a few more annotations on DotE, BlockE and DecE to enable checking. Lowers classes to object type def followed by constructor definition.

Derived from typing.ml, but could be simplified further.

Passes all existing test when run on desugared ir (the default).

[nomeata]

Got some comments. Overall gut feeling is that the ir check could be further refactored to be more of a checker and less of an inference code. Given that you have type annotations on all expressions and subexpressions, you always have all types of the typing rule at hand, so the distinction between checking and inferring should disappear.

In practice subtyping might make that a bit harder than it needs to be. I would not mind an explicit “cast” AST node to contain where subtyping happens.

[rossberg]

My main question is similar to the one Joachim raised re inference vs checking, especially wrt to even doing multiple passes. Is there a plan for simplifying this in a follow-up?

But I think it makes sense to go with this as a first step.

[nomeata]

That’s better, checking against the annotations. But I still find the code structure unnecessary non-local (and it’s probably an artifact of it descending from the type inference).

Since we have the annotations everywhere, there should be no need for a recursive function returning a type (like your infer_exp / check_exp). You have all information locally, i.e. something like this:

check_exp env e = match e.it with
  | BinE (ot, exp1, op, exp2) ->
    (* recurse *)
    check_exp env exp1;
    check_exp env exp1;
    (* typing rule for this constructor *)
    assert (T.sub env.cons ot (E.type e));
    assert (T.sub env.cons (E.type exp1)  ot);
    assert (T.sub env.cons (E.type exp2)  ot);
    assert (Operator.has_binop t op)
   (* no need to return anything *)

You maybe could even have one function (env -> exp -> ()) -> (prog -> ()) that simply traverses the tree, visits each node, updates the environment, and calls its argument, and that would be a non-recursive function that merely checks one AST node in isolation. The latter function is then a hopefully quite direct transliteration of the typing rules.

[crusso]

OK, thanks for taking a look. I'll have another go.

[nomeata]

This is getting very nice, I like it :-)