Upgrade to Pro — share decks privately, control downloads, hide ads and more …

A Type Inferencer for ML in 200 Lines of Scala

A Type Inferencer for ML in 200 Lines of Scala

Ionuț G. Stan

October 22, 2016
Tweet

More Decks by Ionuț G. Stan

Other Decks in Programming

Transcript

  1. A Type Inferencer for ML In 200 Lines of Scala

    Ionuț G. Stan — CODΞCΔMP Iași — October 2016
  2. • Software Developer at Eloquentix • I work mostly with

    Scala • I like FP, programming languages, compilers About Me
  3. • Software Developer at Eloquentix • I work mostly with

    Scala • I like FP, programming languages, compilers • I started the Bucharest FP meetup group About Me
  4. • Software Developer at Eloquentix • I work mostly with

    Scala • I like FP, programming languages, compilers • I started the Bucharest FP meetup group • I occasionally blog at igstan.ro About Me
  5. • Software Developer at Eloquentix • I work mostly with

    Scala • I like FP, programming languages, compilers • I started the Bucharest FP meetup group • I occasionally blog at igstan.ro • Happy to discuss tech stuff at [email protected] About Me
  6. Plan • Compilers Overview • Vehicle Language: µML • Wand's

    Type Inference Algorithm • Intuition • Code
  7. Abstract Syntax Tree T Compiler ) 2 Parser APP FUN

    a VAR a INT 2 Abstract Syntax Tree (AST) uage (funct
  8. Code Generation T Compiler ) 2 Parser CodeGen APP FUN

    a VAR a INT 2 Abstract Syntax Tree (AST) uage (funct
  9. • Type Checking • Ensures declared types are used consistently

    • All types must be declared • Traverse AST and compare def site with use site • Type Inference • Ensures consistency as well • Types need not be declared, though; are deduced! • Two main classes of algorithms • We'll see one instance today Type Checking vs Inference
  10. • Surface Syntax • What does the language look like

    • Type System • What types the language supports Vehicle Language: µML
  11. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. µML — Surface Syntax
  12. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. 3. Booleans: true and false µML — Surface Syntax
  13. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. 3. Booleans: true and false 4. Single-argument anonymous functions: fn a => a µML — Surface Syntax
  14. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. 3. Booleans: true and false 4. Single-argument anonymous functions: fn a => a 5. Function application: inc 42 µML — Surface Syntax
  15. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. 3. Booleans: true and false 4. Single-argument anonymous functions: fn a => a 5. Function application: inc 42 6. If expressions: if cond then t else f µML — Surface Syntax
  16. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. 3. Booleans: true and false 4. Single-argument anonymous functions: fn a => a 5. Function application: inc 42 6. If expressions: if cond then t else f 7. Addition and subtraction: a + b, a - b µML — Surface Syntax
  17. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters):

    inc, cond, a, etc. 3. Booleans: true and false 4. Single-argument anonymous functions: fn a => a 5. Function application: inc 42 6. If expressions: if cond then t else f 7. Addition and subtraction: a + b, a - b 8. Parenthesized expressions: (a + b) µML — Surface Syntax
  18. 1. Integer type: int 2. Boolean type: bool 3. Function

    type: int -> bool µML — Language Types
  19. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  20. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  21. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  22. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  23. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  24. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  25. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  26. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  27. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  28. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN isZero IF APP VAR isZero INT 1 INT 2 INT 3 fn isZero => if isZero 1 then 2 else 3
  29. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN IF APP AR ero INT 1 INT 2 INT 3 FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3
  30. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUN IF APP AR ero INT 1 INT 2 INT 3 FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3
  31. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 Constraint Set
  32. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 t1 Constraint Set
  33. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int t1 t5 Constraint Set
  34. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool t1 t5 t4 Constraint Set
  35. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool ≡ int t1 t5 t4 t6 Constraint Set
  36. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int t1 t5 t4 t6 t7 Constraint Set
  37. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int ≡ t3 t1 t5 t4 t6 t7 t6 Constraint Set
  38. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 t1 t5 t4 t6 t7 t6 t7 Constraint Set
  39. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ t1 → t3 t1 t5 t4 t6 t7 t6 t7 t2 Constraint Set
  40. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ t1 → t3 t1 t5 t4 t6 t7 t6 t7 t2 Constraint Set
  41. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ t1 → t3 t1 t5 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  42. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : t5 → t4 t1 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ t1 → t3 t5 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  43. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : t5 → t4 t1 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ t1 → t3 t5 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  44. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : t5 → t4 t1 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ (t5 → t4) → t3 t5 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  45. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : t5 → t4 : int t1 t5 ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ (t5 → t4) → t3 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  46. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : t5 → t4 : int t1 t5 ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ (t5 → t4) → t3 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  47. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → t4 : int t1 t5 ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 ≡ (int → t4) → t3 t4 t6 t7 t6 t7 t2 Constraint Set Solution Map
  48. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → t4 : int : bool t1 t5 t4 ≡ int ≡ int ≡ t3 ≡ t3 ≡ (int → t4) → t3 t6 t7 t6 t7 t2 Constraint Set Solution Map
  49. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → t4 : int : bool t1 t5 t4 ≡ int ≡ int ≡ t3 ≡ t3 ≡ (int → t4) → t3 t6 t7 t6 t7 t2 Constraint Set Solution Map
  50. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool t1 t5 t4 ≡ int ≡ int ≡ t3 ≡ t3 ≡ (int → bool) → t3 t6 t7 t6 t7 t2 Constraint Set Solution Map
  51. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int t1 t5 t4 t6 ≡ int ≡ t3 ≡ t3 ≡ (int → bool) → t3 t7 t6 t7 t2 Constraint Set Solution Map
  52. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int t1 t5 t4 t6 ≡ int ≡ t3 ≡ t3 ≡ (int → bool) → t3 t7 t6 t7 t2 Constraint Set Solution Map
  53. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int t1 t5 t4 t6 ≡ int ≡ t3 ≡ t3 ≡ (int → bool) → t3 t7 int t7 t2 Constraint Set Solution Map
  54. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int t1 t5 t4 t6 t7 ≡ t3 ≡ t3 ≡ (int → bool) → t3 int t7 t2 Constraint Set Solution Map
  55. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int t1 t5 t4 t6 t7 ≡ t3 ≡ t3 ≡ (int → bool) → t3 int t7 t2 Constraint Set Solution Map
  56. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int t1 t5 t4 t6 t7 ≡ t3 ≡ t3 ≡ (int → bool) → t3 int int t2 Constraint Set Solution Map
  57. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int : int t1 t5 t4 t6 t7 t3 ≡ t3 ≡ (int → bool) → t3 int t2 Constraint Set Solution Map
  58. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int : int t1 t5 t4 t6 t7 t3 ≡ t3 ≡ (int → bool) → t3 int t2 Constraint Set Solution Map
  59. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int : int t1 t5 t4 t6 t7 t3 ≡ int ≡ (int → bool) → int int t2 Constraint Set Solution Map
  60. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int : int t1 t5 t4 t6 t7 t3 ≡ int ≡ (int → bool) → int int t2 Constraint Set Solution Map
  61. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int : int t1 t5 t4 t6 t7 t3 ≡ (int → bool) → int t2 Constraint Set Solution Map
  62. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST : int → bool : int : bool : int : int : int : (int → bool) → int t1 t5 t4 t6 t7 t3 t2 Constraint Set Solution Map
  63. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3 : int → bool : int : bool : int : int : int : (int → bool) → int t1 t5 t4 t6 t7 t3 t2 Solution Map
  64. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing

    AST fn isZero => if isZero 1 then 2 else 3 (int -> bool) -> int
  65. • As I said, there are two main classes. •

    Constraint-based: we've just seen one example — Wand's algorithm. • Substitution-based: all phases are interleaved, e.g., Algorithm W. Type Inference Algorithms
  66. • Sunil Kothari and James L. Caldwell. Type Reconstruction Algorithms

    - A Survey • Mitchell Wand. A simple algorithm and proof for type inference • Bastiaan Heeren, Jurriaan Hage and Doaitse Swierstra. Generalizing Hindley-Milner Type Inference Algorithms • Oleg Kiselyov and Chung-chieh Shan. Interpreting Types as Abstract Values • Shriram Krishnamurthi. Programming Languages: Application and Interpretation, chapter 15 • Shriram Krishnamurthi. Programming Languages: Application and Interpretation, lecture 24 • Shriram Krishnamurthi. Programming Languages: Application and Interpretation, lecture 25 • Bastiaan Heeren. Top Quality Type Error Messages • Stephen Diehl. Write You a Haskell, chapter 6 • Andrew Appel. Modern Compiler Implementation in ML, chapter 16 • Benjamin Pierce. Types and Programming Languages, chapter 22 • Martin Odersky. Scala by Example, chapter 16 • Danny Gratzer. https://github.com/jozefg/hm • Arlen Cox. ML Type Inference and Unification! • Radu Rugină. CS 312, Type Inference Resources