Type abstract interpreter 3
same abstract domain of interpreter 2
the essential feature
- the abstract values denoted by the recursive function name within the fixpoint computation need to be generalized
- and therefore correctly universally quantified
so as to allow different instantiations in each iteration of the evaluation of the function body
we have decided to generalize all the computed type schemes
- universally quantified types in the result
- no special handling of Let
- fresh variables used in the semantic of functional abstraction are still free variables