Principal type-schemes for functional programs

Transcript

1. Principal type-schemes for functional programs Luis Damas and Robin Milner (POPL `82)
2. Agenda • Slides • Code
3. ML • Meta Language for LCF • Type inference • Influence on Haskell, Rust, F#, OCaml, ... • “Sweet spot” in type system design
4. ML letrec f xs = if null xs then nil else snoc (f (tl xs)) (hd xs) What type does this function have? null : ∀ ( list → bool) snoc : ∀ ( list → → list) hd, tl : ∀ ( list → ) nil : ∀ ( list)
5. ML What about: let s x y z = x z (y z) ?
6. Type Inference f : ∀ ( list → list) • Given f, how can we infer this type? • What does it even mean for a value to have a type? • How can we be sure we have the most general type?
7. Lambda Calculus Expressions e: • Identifiers: , , … • Applications: e e’ • Abstractions: . e • Let bindings: let = e in e’
8. Lambda Calculus For example: . . . . let = . . in
9. Types Monotypes : • Variables: • Primitives: • Functions: →
10. Type Schemes Type schemes : • Monomorphic: • Polymorphic: ∀ . Type schemes are types with identifiers bound by ∀ at the front.
11. Substitutions Mappings from variables to types • Can instantiate type schemes using substitutions • Gives a simple subtyping relation on type schemes
12. Semantics Construct a semantic domain (CPO) V containing • Primitives • Functions • An error element and a semantic function : e → (Id → V) → V
13. Semantics Identify types with subsets of V Define the judgment A ╞ e : when (∀ ( : ’) ∈ A. ∈ ’) ⇒ e ∈
14. Declarative System Variable rule:
15. Declarative System Application rule:
16. Declarative System Abstraction rule:
17. Declarative System Let rule:
18. Declarative System Instantiation rule:
19. Declarative System Generalization rule:
20. Soundness If A e : then A ╞ e : “Static behavior determines dynamic behavior”
21. Example Prove: . : ∀ . ( → → ) → →
22. Algorithm W • The inference rules do not translate easily into an algorithm (why not?) • Introduce w : Exp → Env → (Env, )
23. Algorithm W • W attempts to build a substitution, bottom-up • W can fail with an error if there is no valid typing • Intuition: ◦ Collect constraints ◦ Then solve constraints • Reality: W is the fusion of these two steps • See the code!
24. Unification • Unification gives local information about types • We assemble a global solution from local information
25. Unification Example: ( → ) ~ (( → ) → ) ~ ( → ) ~ ~ ( → )
26. Occurs Check Prevents inference of infinite types w( . , nil) = error! Can’t unify ~ if occurs in the body of . E.g. ~ → ~ ((… → ) → ) →
27. Soundness If w(A, e) = (S, ) then A e : “Algorithm W constructs typing judgments”
28. Completeness If A e : then w(A, e) constructs a typing judgment for e which generalises the above. “Algorithm W constructs principal types”
29. Further Reading More type systems • System F, F⍵ • Rank-N types • Type Classes • Dependent Types • Refinement Types Other approaches • Constraints • Bidirectional typechecking • SMT See TAPL & ATAPL!
30. Acknowledgments DHM axioms reproduced from Wikipedia under the CC-3.0 Attribution/ShareAlike license