9/5/21
We can run Normal Order Reduction, and Expression Type, together. Some insights might be gleaned from this (that a (not further reducible) normal form might not have a type, that an expression without a type might reduce to one with a type, that a starting expression with a type will reduce, and stop, to an expression with a type, etc. But there will be some peculiarities also.
The unexpected
There are some oddities that arise from our implementation of Mini-ML, Let Polymorphism, annotation, when there is also reduction.
Consider (λy:B.(y 7) λx.x ). It is ill-typed; it does not have a type. The annotation tells us that y is to be a Boolean. But internal application (y 7) requires that the type of y is a function (i.e. has an arrow in it), and moreover has type I (Integer) to the left of the arrow i.e. I->? . That just cannot be done. But when that expression is reduced by one step λx.x goes in for y and the expression becomes (λx.x 7). Now, it might be argued, the lambda sub-expression of that (i.e. λx.x) should have type B if the annotation is followed i.e. it should be something like [λx.x]:B (putting the square brackets in for clarity). But we don't have any annotations like that— we have annotations of the variable in a lambda (or the variable within a let). We could annotate the variable e.g. λx:?.x . But the ? cannot be B, for it is the whole expression λx.x that needs to be B, not just the variable x on its own. In short, we have no way of making the desired annotation. Alright, so omit annotation, then we are left with λx.x . But this is well-typed, with type a->a . In a manner of speaking, what has happened here is that the initial annotation has been forgotten and left behind on reduction.
Something similar can happen with 'lets'. The variable in a let can have a universally quantified type-scheme as its type annotation. No other expressions can be annotated like that, and the intention of the annotation can be lost during reduction.
The type evaluation works using as input only the formula presented (and it will provide the correct type for that input (assuming no slips in the algorithms and code)). It will correctly type all the individual steps in a reduction (normal order or otherwise). But the way our MiniML has written, some of the initial annotation may disappear during reduction.
Most implementations of MiniML omit annotation altogether. They avoid the sticky territory that we have got ourselves into.