Type Inference: How Does it Work?

http://bucharestfp.ro/2015/03/31/type-inference-how-does-it-work/

Transcript

1. Type Inference How Does it Work? Ionuț G. Stan — Bucharest FP #9 — March 2015
2. Organization • Compilers Overview • Overview of the Damas-Hindley-Milner Algorithm • Code • Limitations of Damas-Hindley-Milner
3. Compilers Overview
4. Compilers Overview Code Emitter Target Source
5. Compilers Overview Code Emitter Target Source Parser Code Emitter Target Source
6. Compilers Overview Code Emitter Target Source Parser Code Emitter Target Source AST (Abstract Syntax Tree)
7. Compilers Overview Code Emitter Target Source Parser Code Emitter Target Source Parser Type Checker Source Target Code Emitter AST (Abstract Syntax Tree)
8. Compilers Overview Code Emitter Target Source Parser Code Emitter Target Source Parser Type Checker Source Target Code Emitter Parser Type Checker Source Target Code Emitter ...
9. Today Parser Type Checker ... Source AST (Abstract Syntax Tree) Target
10. Algorithm Overview
11. Algorithm Overview • Phase 1: source code → parse → abstract syntax tree (AST) • Phase 2: AST → annotate → typed abstract syntax tree (TST) • Phase 3: TST → generate constraints → constraint list • Phase 4: constraint list → unify → solution list
12. Algorithm Overview • Phase 1: source code → parse → abstract syntax tree (AST) • Phase 2: AST → annotate → typed abstract syntax tree (TST) • Phase 3: TST → generate constraints → constraint list • Phase 4: constraint list → unify → solution list
13. Algorithm Overview • Phase 1: source code → parse → abstract syntax tree (AST) • Phase 2: AST → annotate → typed abstract syntax tree (TST) • Phase 3: TST → generate constraints → constraint list • Phase 4: constraint list → unify → solution list
14. Algorithm Overview • Phase 1: source code → parse → abstract syntax tree (AST) • Phase 2: AST → annotate → typed abstract syntax tree (TST) • Phase 3: TST → generate constraints → constraint list • Phase 4: constraint list → unify → solution list
15. Running Example let val inc = fn n => n + 1 in inc 42 end
16. Phase 1: Abstract Syntax Tree let val inc = fn n => n + 1 in inc 42 end LET inc FN n ADD VAR n INT 1 APP VAR inc INT 42
17. Phase 2: Explicit Type Annotations LET inc FN n ADD VAR n INT 1 APP VAR inc INT 42 LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42
18. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42
19. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42 t1 → int = int → t2
20. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42 t1 → int = int → t2 int = int
21. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42 t1 → int = int → t2 int = int t1 = int
22. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42 t1 → int = int → t2 int = int t1 = int t3 = t2
23. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42 t1 → int = int → t2 int = int t1 = int t3 = t2
24. Phase 4: Unification
25. Phase 4: Unification f(x) = f(g(y)) [x: g(y)]
26. Phase 4: Unification f(x) = f(g(y)) [x: g(y)] f(x, g(3)) = f(g(y), x) [x: g(y); y: 3]
27. Phase 3: Constraint Generation LETt3 inc FNt1 !int a ADDint VARt1 a INTint 1 APPt2 VARt1 !int inc INTint 42 t1 → int = int → t2 int = int t1 = int t3 = t2
28. Phase 4: Unification t1 → int = int → t2 int = int t1 = int t3 = t2
29. Phase 4: Unification t1 → int = int → t2 int = int t1 = int t3 = t2 3 = t2
30. Phase 4: Unification t1 → int = int → t2 int = int t1 = int 3 = t2
31. Phase 4: Unification t1 → int = int → t2 int = int 3 = t2 1 = int
32. Phase 4: Unification int → int = int → t2 int = int 3 = t2 1 = int
33. Phase 4: Unification int → int = int → t2 3 = t2 1 = int
34. Phase 4: Unification int → t2 int → int 3 = t2 1 = int
35. Phase 4: Unification int → t2 3 = t2 1 = int
36. Phase 4: Unification 3 = t2 1 = int 2 = int
37. Phase 4: Unification 3 = int 1 = int 2 = int
38. Code
39. https://github.com/igstan/damas-hindley-milner
40. Limitations
41. Limitations • doesn't work with OOP; subtyping breaks unification • restricted let-polymorphism with mutable references (ref) • polymorphic params (rank-n polymorphism) • algorithm complexity is exponential; not a problem in practice
42. Value Restriction in SML val r0 : 'a option ref = ref NONE val r1 : string option ref = r0 val r2 : int option ref = r0 val _ = r1 := SOME "foo" val v : int = valOf (!r2)
43. Value Restriction in SML val r0 : 'a option ref = ref NONE val r1 : string option ref = r0 val r2 : int option ref = r0 val _ = r1 := SOME "foo" val v : int = valOf (!r2) The string inside is used as an int. ERROR
44. Value Restriction in SML val r0 : 'a option ref = ref NONE val r1 : string option ref = r0 val r2 : int option ref = r0 val _ = r1 := SOME "foo" val v : int = valOf (!r2) Solved in OCaml using weak polymorphism. Type is polymorphic until first use; afterwards becomes monomorphic. ERROR
45. Rank-N Polymorphism fn id => (id 1, id true) Parameters are not polymorphic. Algorithm becomes undecidable. let val id = fn a => a in (id 1, id true) end OK ERROR
46. Exponential Time http://spacemanaki.com/blog/2014/08/04/Just-LOOK-at-the-humongous-type/ fn _ => let val id = fn a => a val d1 = (id, id) val d2 = (d1, d1) val d3 = (d2, d2) val d4 = (d3, d3) val d5 = (d4, d4) val d6 = (d5, d5) in d6 end
47. Exponential Time http://spacemanaki.com/blog/2014/08/04/Just-LOOK-at-the-humongous-type/ val it = fn : 'a -> (((((('b -> 'b) * ('c -> 'c)) * (('d -> 'd) * ('e -> 'e))) * ((('f -> 'f) * ('g -> 'g)) * (('h -> 'h) * ('i -> 'i)))) * (((('j -> 'j) * ('k -> 'k)) * (('l -> 'l) * ('m -> 'm))) * ((('n -> 'n) * ('o -> 'o)) * (('p -> 'p) * ('q -> 'q))))) * ((((('r -> 'r) * ('s -> 's)) * (('t -> 't) * ('u -> 'u))) * ((('v -> 'v) * ('w -> 'w)) * (('x -> 'x) * ('y -> 'y)))) * (((('z -> 'z) * ('ba -> 'ba)) * (('bb -> 'bb) * ('bc -> 'bc))) * ((('bd -> 'bd) * ('be -> 'be)) * (('bf -> 'bf) * ('bg -> 'bg)))))) * (((((('bh -> 'bh) * ('bi -> 'bi)) * (('bj -> 'bj) * ('bk -> 'bk))) * ((('bl -> 'bl) * ('bm -> 'bm)) * (('bn -> 'bn) * ('bo -> 'bo)))) * (((('bp -> 'bp) * ('bq -> 'bq)) * (('br -> 'br) * ('bs -> 'bs))) * ((('bt -> 'bt) * ('bu -> 'bu)) * (('bv -> 'bv) * ('bw -> 'bw))))) * ((((('bx -> 'bx) * ('by -> 'by)) * (('bz -> 'bz) * ('ca -> 'ca))) * ((('cb -> 'cb) * ('cc -> 'cc)) * (('cd -> 'cd) * ('ce -> 'ce)))) * (((('cf -> 'cf) * ('cg -> 'cg)) * (('ch -> 'ch) * ('ci -> 'ci))) * ((('cj -> 'cj) * ('ck -> 'ck)) * (('cl -> 'cl) * ('cm -> 'cm))))))
48. Exponential Time http://spacemanaki.com/blog/2014/08/04/Just-LOOK-at-the-humongous-type/
49. Thank You!