dhess
commented
1 year ago 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.
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
EvalFullis very eager to reduce in annotations, for example after a BETA reduction of(Λa.Λb. t : ∀a.∀b. T) @x @ywe 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 twolets, 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 twolets. 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 bothlet bandlet athroughTin 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 https://github.com/hackworthltd/primer/pull/736#pullrequestreview-1526613940
Future work