Abstract least fixpoint computation
both Hindley’s and ML’s type inference algorithms do not try to compute the fixpoint and simply perform the widening (unification) at step 1
abstreq checks the two terms in the abstract values for variance
not always correct when there are free variables
solved in the next abstract domain
the abstract semantic evaluation function is left unchanged
we just add an external function which sets the widening parameter k
let sem1 (e:exp) (k:int) =
………
in sem e emptyenv
Previous slide
Next slide
Back to first slide
View graphic version