(WIP) FR: do not be so eager to reduce in types

[brprice]

• I have read the project's code of conduct, and by submitting this feature request, I agree to follow it.

Description

This is a feature request.

Our current evaluator implemented in #736 is a bit too eager to reduce inside types. If we want to stick to "normal order", we should relax this.

Dependencies

#736 should be finalised and merged.

Spec

Currently/after #736 EvalFull is very eager to reduce in annotations, for example after a BETA reduction of (Λa.Λb. t : ∀a.∀b. T) @x @y we obtain (let a=x in Λb. t : let a=x in ∀b. T) @y.
We now must reduce inside the LHS -- our two choices are the two lets, and we give higher priority to the one in the type, giving (let a=x in Λb. t : ∀b. let a=x in T) @y.
We still have two redexes, being the two lets. We currently reduce inside the annotation, fully removing the type-let, before considering reducing the term-let.
However, normal order would be to push the term-let once which would give (Λb. let a=x in t : ∀b. let a=x in T) @y, unlocking the next BETA redex.

We would do something similar for type applications -- in general we fully reduce inside type children before doing any reduction in term children.

The impact of this is fairly limited, since computation in types always halts.
However, it does impact efficiency: in particular since we push a stack of lets as one atomic unit, the current approach may traverse an annotation multiple times fully pushing one individual let through each time, whereas we could potentially only traverse once with a stack.
For example, if we continue the above example with the proposed order, we would do a BETA step to get let b=y in let a=x in t : let b=y in let a=x in T, which would enable us to push both let b and let a through T in one pass.

Implementation details

I don't currently have a particular implementation plan -- this needs fleshing out.

One idea is for each node in the AST to "say" either "I am a redex" or "I am in WHNF" or "I am stuck on these children:...". This would allow us to have a more subtle normalisation procedure than "reduce the root if possible, else recurse into children: types first then terms, secondarily ordered left-to-right".

Not in spec

Discussion

This was initially mentioned in #736 (review)

Future work

[dhess]

In our 2023-07-25 developer meeting, we decided there is no pressing reason to tackle this FR now. We can just state that we have normal-ish-order eval for the time being, and come back to this later when we start dealing with performance issues in the evaluator.