Type inference with constraints

A motivating problem

bondi and system FM

Constraints

Type inference with constraints

References

Type inference with constraints
Jose Vergara
University of Technology Sydney

Sydney Area Programming Languages INterest Group 2010

Jose Vergara Type inference with constraints

University of Technology Sydney

A motivating problem

bondi and system FM

ConstraintsType inference with constraints

References

1 A motivating problem

2 bondi and system FM

3 Constraints

4 Type inference with constraints

Jose Vergara Type inference with constraints

University of Technology Sydney

A motivating problem

bondi and system FM

Constraints

Type inference with constraints

References

Types and type Systems

A type is a formaldescription of the behavior of a program fragment. For example: plus : Int → Int → Int map : (a → b) → List a → List b select : (all a.a → List b) → c → List b The Damas-Milner type system [Milner, 1978] offers a restricted form of polymorphism and is at the heart of Standard ML and Objective Caml.

Jose Vergara Type inference with constraints

University of Technology Sydney

A motivating problembondi and system FM

Constraints

Type inference with constraints

References

The Dammas-Milner type system us capable to type functions like plus and map, but what about the select function?
let fun | z | y ;; e x t ( s e l e c t : ( a l l a . a −> L i s t b ) −> c −> L i s t b ) = f −> y −> append ( f ( z y ) ) ( append ( s e l e c t f z ) ( s e l e c t f y ) ) −> f y

It isnecessary to have: Local quantification and type application Type matching for the function of type ∀a.a → List b

Jose Vergara Type inference with constraints

University of Technology Sydney

A motivating problem

bondi and system FM

Constraints

Type inference with constraints

References

System FM
System FM extends system F with type matching.
t ::= xT tt λxT .t tT [∆]T → t (term)(variable) (application) (abstraction) (type application) (typecase) T ::= X T →T ∀T [∆].T (type) (variable) f unction) (typecase)

Let ∆ be a type context and let P and U be types. There is a match of P against U with respect to ∆ if f {U/[∆] P } is some substitution in which case is their most general (Jay; 2009).

Jose Vergara Type inference with constraints

University of TechnologySydney

A motivating problem

bondi and system FM

Constraints

Type inference with constraints

References

Type unification

Type unification for system FM is simple:
{X = X} {S = X} {X = T } {P → S = Q → T } = = = = {} {S/X}if X ∈ F V (S) / {T /X} if X ∈ F V (T ) / let υ1 = {P = Q} in let υ2 = {υ1 S = υ2 T } in υ2 ◦ υ1 let υ1 = {P = Q} in let υ2 = {υ1 S = υ2 T } in υ2 ◦ υ1 if thisavoids ∆ undef ined otherwise

{∀P [∆].S = ∀Q [∆].}

=

{S = T }

=

Jose Vergara Type inference with constraints

University of Technology Sydney

A motivating problem

bondi and system FM

Constraints

Type inference with constraints

References

Full type inference for System F is undecidable (Wells; 1999). In order to support first class polymorphism bondi relies onprovided type annotations to correctly type functions with polymorphic type arguments. It is also desirable to have an efficient type inference algorithm like those of the OCaml and Haskell compilers.

Jose Vergara Type inference with constraints

University of Technology Sydney

A motivating problem

bondi and system FM

Constraints

Type inference with constraints

References

So farwe have a specification of the problem, it remains to: Provide the proofs for type unification(in progress) and type matching. Define and implement type unification with constraints. Deal with type annotations when performing type inference with constraints on path polymorphic queries. What to do? As a first step, lets learn how to do type inference with constraints to support the Dammas-Milner type...