Let's Write a Type Checker

Transcript

1. Let's Write a Type Checker Ionuț G. Stan — I T.A.K.E. — May 2015
2. • Part 1 • Compilers Overview • Type Checking vs Type Inference • Vehicle Language • Wand's Type Inference Algorithm • Part 2 • Live Demonstration The Plan
3. Compilers Overview
4. Compiler Compilers Overview
5. Source Code Compiler Compilers Overview
6. Source Code Compiler (fn a => a) 2 Compilers Overview
7. Source Code Target Language Compiler (fn a => a) 2 Compilers Overview
8. Source Code Target Language Compiler (fn a => a) 2 (function(a){return a;})(2); Compilers Overview
9. Source Code Target Language Compiler (fn a => a) 2 (function(a){return a;})(2); Interpreter Compilers Overview
10. Source Code Target Language Compiler (fn a => a) 2 (function(a){return a;})(2); Source Code Interpreter Compilers Overview
11. Source Code Target Language Compiler (fn a => a) 2 (function(a){return a;})(2); Source Code Interpreter (fn a => a) 2 Compilers Overview
12. Source Code Target Language Compiler (fn a => a) 2 (function(a){return a;})(2); Source Code Evaluation Result Interpreter (fn a => a) 2 Compilers Overview
13. Source Code Target Language Compiler (fn a => a) 2 (function(a){return a;})(2); Source Code Evaluation Result Interpreter (fn a => a) 2 2 Compilers Overview
14. Compilers Overview de T Compiler ) 2 (functi
15. Parsing de T Compiler ) 2 (functi Parser
16. Abstract Syntax Tree de T Compiler ) 2 (functi Parser Abstract Syntax Tree (AST)
17. Abstract Syntax Tree de T Compiler ) 2 (functi Parser APP FUN a VAR a INT 2 Abstract Syntax Tree (AST)
18. Code Generation de T Compiler ) 2 (functi Parser CodeGen APP FUN a VAR a INT 2 Abstract Syntax Tree (AST)
19. Many Intermediate Phases de T Compiler ) 2 (functi Parser CodeGen ... AST
20. Type Checking de T Compiler ) 2 (functi Parser CodeGen Type Checker AST Typed AST ...
21. Today's Talk de T Compiler ) 2 (functi Parser CodeGen Type Checker AST Typed AST Today
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
25. • Surface Syntax • What's the concrete syntax of the language • Type System • What types are supported by the language Vehicle Language
26. 1. Numbers: 1, 2, 3, ... 2. Booleans: true and false 3. Function expressions: fn a => a 4. Function application: inc 42 or 2 + 3 5. If expressions: if cond then t else f Surface Syntax1 1 — a subset of Standard ML
27. 1. Numbers: 1, 2, 3, ... 2. Booleans: true and false 3. Function expressions: fn a => a 4. Function application: inc 42 or 2 + 3 5. If expressions: if cond then t else f Surface Syntax1 1 — a subset of Standard ML
28. 1. Numbers: 1, 2, 3, ... 2. Booleans: true and false 3. Anonymous functions (lambdas): fn a => a 4. Function application: inc 42 or 2 + 3 5. If expressions: if cond then t else f Surface Syntax1 1 — a subset of Standard ML
29. 1. Numbers: 1, 2, 3, ... 2. Booleans: true and false 3. Anonymous functions (lambdas): fn a => a 4. Function application: inc 42 5. If expressions: if cond then t else f Surface Syntax1 1 — a subset of Standard ML
30. 1. Numbers: 1, 2, 3, ... 2. Booleans: true and false 3. Anonymous functions (lambdas): fn a => a 4. Function application: inc 42 5. If expressions: if cond then t else f Surface Syntax1 1 — a subset of Standard ML
31. 6. Let blocks/expressions:
 
 let
 val name = ...
 in
 name
 end Surface Syntax1 1 — a subset of Standard ML
32. Small Example let val inc = fn a => a + 1 in inc 42 end
33. 1. Integer type: int 2. Boolean type: bool 3. Function type: int -> bool 4. Generic type variables: 'a, 'b, 'c, etc. Language Types
34. 1. Integer type: int 2. Boolean type: bool 3. Function type: int -> bool 4. Generic type variables: 'a, 'b, 'c, etc. Language Types
35. 1. Integer type: int 2. Boolean type: bool 3. Function type: int -> bool 4. Generic type variables: 'a, 'b, 'c, etc. Language Types
36. 1. Integer type: int 2. Boolean type: bool 3. Function type: int -> bool 4. Generic type variables: 'a, 'b, 'c, etc. Language Types
37. Today's Algorithm Overview
38. Wand's Algorithm Overview
39. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing AST
40. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing AST fn isZero => if isZero 1 then 2 else 3
41. 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
42. 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
43. 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
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 IF APP AR ero INT 1 INT 2 INT 3 FUNt2 isZerot1 IFt3 APPt4 VARt1 isZero INTt5 1 INTt6 2 INTt7 3
52. 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
53. 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
54. 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
55. 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
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 ≡ t5 → t4 ≡ int ≡ bool t1 t5 t4 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 ≡ int ≡ bool ≡ int t1 t5 t4 t6 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 ≡ bool ≡ int ≡ int t1 t5 t4 t6 t7 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 ≡ int ≡ int ≡ t3 t1 t5 t4 t6 t7 t6 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 ≡ int ≡ t3 ≡ t3 t1 t5 t4 t6 t7 t6 t7 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 ≡ t3 ≡ t3 ≡ t1 → t3 t1 t5 t4 t6 t7 t6 t7 t2 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 ≡ t3 ≡ t1 → t3 t1 t5 t4 t6 t7 t6 t7 t2 Constraint Set
63. 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
64. 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
65. 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
66. 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
67. 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
68. 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
69. 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
70. 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
71. 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
72. 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
73. 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
74. 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
75. 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
76. 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
77. 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
78. 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
79. 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
80. Wand's Algorithm Overview Type Annotation Constraint Generation Constraint Solving Parsing AST fn isZero => if isZero 1 then 2 else 3 (int -> bool) -> int
81. • As I said, there are two main classes • Constraint-based ones. We've just seen one example — Wand's algorithm • Substitution-based ones, where constraint generation and solving are not two separate processes, they are interleaved. Example: the classic Hindley-Milner Algorithm W. Type Checking Algorithms
82. Live Demonstration
83. https://github.com/igstan/itake-2015
84. Thank You!
85. • 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