Towards constraints
(wrong!) abstract operation
let rec makefun(ii,aa,r) = let d = newvar() in
let t = sem aa (bind(r,ii,d))) in
Mkarrow(d,t)
Fun(Id “x”, Sum(Var(Id “x”), Eint 1))
“x” is bound to a new variable Vvar “0” in the environment r
the expression Sum(Var(Id “x”), Eint 1)) is evaluated in r
the abstract Sum operation needs to instantiate the type variable Vvar “0” to Intero
abstraction of the concrete type checking
this can be achieved
by forcing abstract operations to return an abstract value and an abstract environment
changing the structure of the concrete semantic evaluation function
by extending the abstract domain to pairs consisting of a term (type) and a constraint on type variables
Previous slide
Next slide
Back to first slide
View graphic version