A Type Inferencer for ML in 200 Lines of Scala

Transcript

1. A Type Inferencer for ML In 200 Lines of Scala Ionuț G. Stan — igstan.ro — ionut@eloquentix.com
2. • Software Developer at • Worked with Scala for the past 5 years • FP, programming languages, compilers • Mostly-tech blog at igstan.ro About Me
3. Plan
4. Plan • Compilers Overview
5. Plan • Compilers Overview • Vehicle Language: µML
6. Plan • Compilers Overview • Vehicle Language: µML • Wand's Type Inference Algorithm
7. Plan • Compilers Overview • Vehicle Language: µML • Wand's Type Inference Algorithm • Intuition
8. Plan • Compilers Overview • Vehicle Language: µML • Wand's Type Inference Algorithm • Intuition • Code
9. Compilers Overview
10. Compiler Compilers Overview
11. Compiler Compilers Overview Source Language
12. Target Language Compiler Compilers Overview Source Language
13. Target Language Compiler (fn a => a) 2 Compilers Overview Source Language
14. Target Language Compiler (fn a => a) 2 (function(a){return a})(2) Compilers Overview Source Language
15. Compilers Overview uage T Compiler ) 2 (funct
16. Parsing T Compiler ) 2 Parser uage (funct
17. Abstract Syntax Tree T Compiler ) 2 Parser APP FUN a VAR a INT 2 Abstract Syntax Tree (AST) uage (funct
18. Code Generation T Compiler ) 2 Parser CodeGen APP FUN a VAR a INT 2 Abstract Syntax Tree (AST) uage (funct
19. Many Intermediate Phases T Compiler ) 2 Parser CodeGen ... AST (funct uage
20. Type Checking T Compiler ) 2 Parser CodeGen Type Checker AST ... uage (funct
21. Today's Talk T Compiler ) 2 Parser CodeGen Type Checker AST Today's T alk ... uage (funct
22. Type Checking vs Type Inference
23. • 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
24. Vehicle Language: µML
25. • Surface Syntax • What does the language look like • Type System • What types the language supports Vehicle Language: µML
26. 1. Integers: 1, 23, 456, etc. µML — Surface Syntax
27. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters): inc, cond, a, etc. µML — Surface Syntax
28. 1. Integers: 1, 23, 456, etc. 2. Identifiers (only letters): inc, cond, a, etc. 3. Booleans: true and false µML — Surface Syntax
29. 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
30. 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
31. 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
32. 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
33. 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
34. 9. Let blocks/expressions:
 
 let
 val name = ...
 in
 name
 end µML — Surface Syntax
35. Small Example let val inc = fn a => a + 1 in inc 42 end
36. µML — Language Types
37. 1. Integer type: int µML — Language Types
38. 1. Integer type: int 2. Boolean type: bool µML — Language Types
39. 1. Integer type: int 2. Boolean type: bool 3. Function type: int -> bool µML — Language Types
40. Today's Algorithm Overview
41. Wand's Algorithm Overview
42. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing AST
43. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing AST fn isZero => if isZero 1 then 2 else 3
44. 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
45. 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
46. 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
47. 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
48. 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
49. 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
50. 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
51. 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
52. 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
53. 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
54. 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
55. 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
56. 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
57. 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
58. 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
59. 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
60. 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
61. 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
62. 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
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 ≡ t5 → t4 ≡ int ≡ bool ≡ int ≡ int ≡ t3 ≡ t3 t1 t5 t4 t6 t7 t6 t7 Constraint Set
64. 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
65. 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
66. 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
67. 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
68. 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
69. 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
70. 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
71. 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
72. 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
73. 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
74. 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
75. 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
76. 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
77. 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
78. 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
79. 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
80. 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
81. 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
82. 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
83. 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
84. 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
85. 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
86. 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
87. 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
88. 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
89. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing AST fn isZero => if isZero 1 then 2 else 3 (int -> bool) -> int
90. • 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
91. • 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
92. github.com / igstan / typelevel-nyc-2017
93. Thank You!
94. Questions!