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

Principal type-schemes for functional programs

Principal type-schemes for functional programs

Phil Freeman

June 28, 2017
Tweet

More Decks by Phil Freeman

Other Decks in Programming

Transcript

  1. ML • Meta Language for LCF • Type inference •

    Influence on Haskell, Rust, F#, OCaml, ... • “Sweet spot” in type system design
  2. 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)
  3. 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?
  4. Lambda Calculus Expressions e: • Identifiers: , , … •

    Applications: e e’ • Abstractions: . e • Let bindings: let = e in e’
  5. Type Schemes Type schemes : • Monomorphic: • Polymorphic: ∀

    . Type schemes are types with identifiers bound by ∀ at the front.
  6. Substitutions Mappings from variables to types • Can instantiate type

    schemes using substitutions • Gives a simple subtyping relation on type schemes
  7. Semantics Construct a semantic domain (CPO) V containing • Primitives

    • Functions • An error element and a semantic function : e → (Id → V) → V
  8. Semantics Identify types with subsets of V Define the judgment

    A ╞ e : when (∀ ( : ’) ∈ A. ∈ ’) ⇒ e ∈
  9. Soundness If A e : then A ╞ e :

    “Static behavior determines dynamic behavior”
  10. Algorithm W • The inference rules do not translate easily

    into an algorithm (why not?) • Introduce w : Exp → Env → (Env, )
  11. 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!
  12. Unification • Unification gives local information about types • We

    assemble a global solution from local information
  13. Occurs Check Prevents inference of infinite types w( . ,

    nil) = error! Can’t unify ~ if occurs in the body of . E.g. ~ → ~ ((… → ) → ) →
  14. Soundness If w(A, e) = (S, ) then A e

    : “Algorithm W constructs typing judgments”
  15. Completeness If A e : then w(A, e) constructs a

    typing judgment for e which generalises the above. “Algorithm W constructs principal types”
  16. 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!