Principal Type Schemes
for Modular Programs
Derek Dreyer and Matthias Blume
Toyota Technological Institute at Chicago
ESOP 2007
Braga, Portugal
Principal Type Schemes for
Functional Programs
• Damas and Milner’s classic POPL’82 paper about
implicit ML-style “let-polymorphism”
• Declarative semantics:  ` e : 
– Clean, but non-deterministic: e may have many types 
• Algorithm W:  ` e ) ( ; )
– Computes the principal, “most general” type of e
Principal Type Schemes for
Modular Programs?
• Definition of Standard ML joins Damas-Milner’s
declarative rules with the rules of the ML module system
• Implementations of SML employ various generalizations
of Algorithm W to work in the presence of modules
• Is Damas-Milner being generalized properly?
– Does SML have principal types?
Contributions of This Work
• A set of example programs on which no SML typechecker
accurately matches the Definition
– Illustrate why the Definition is difficult to implement
• A novel declarative system for ML-style polymorphism in
the presence of modules that is easy to implement
– Principal types theorem proved
– Backward-compatible with SML
– Elegant application of previous ideas/techniques
Example (a)
Example (a)
• Value restriction: f’s type cannot be polymorphically
generalized because id id is not a syntactic value.
Example (a)
Example (a)
Example (a)
Example (a)
Example (a)
Example (a) is Well-Typed
According to the Definition
What Went Wrong?
MacQueen’s Gambit
• SML/NJ’s policy (according to Dave MacQueen):
– Core and module languages should not mix
– Reject module-level bindings where r.h.s. is not a value
and is not uniquely typed, e.g. val f = id id.
MacQueen’s Gambit
• SML/NJ’s policy (according to Dave MacQueen):
– Core and module languages should not mix
– Reject module-level bindings where r.h.s. is not a value
and is not uniquely typed, e.g. val f = id id.
• Disadvantages:
– Rejects perfectly good, noncontrived examples, too.
E.g. val L = ref nil.
– May not scale to languages where module and core are
intertwined (e.g. 1st-class modules, modular type classes)
Our Solution
Our Solution
• Need a way of generalizing  at the functor binding
Our Solution
• Idea: Generalized Functor Signatures (GFS)
– Allow functors to take implicit type arguments in
addition to their explicit module arguments
Our Solution
• Idea: Generalized Functor Signatures (GFS)
– Allow functors to take implicit type arguments in
addition to their explicit module arguments
Our Solution
• Idea: Generalized Functor Signatures (GFS)
– Allow functors to take implicit type arguments in
addition to their explicit module arguments
• Implicit functors were also useful for modular type classes
Our Solution
Our Solution
Our Solution
…
Our Solution
…
Example (a) Typechecks!
…
Still Typechecks!
…
Problem#1Solved!
Example (b)
Example (b) is Well-Typed
According to the Definition
Example (b) Using a GFS
Example (b) Using a GFS
Example (b) Rejected!
Not in scope!
Our Solution
• Idea:
– Expand the definition of “in scope”
– Allow inferred types to mention abstract types that are
not defined until later in the program
Example (b) Accepted!
No problem!
Our Solution
• Idea:
– Expand the definition of “in scope”
– Allow inferred types to mention abstract types that are
not defined until later in the program
• How does that work and is it sound?
Our Solution
• Idea:
– Expand the definition of “in scope”
– Allow inferred types to mention abstract types that are
not defined until later in the program
• How does that work and is it sound?
– Using Dreyer’s RTG type system (ICFP 05), which was
designed as a foundation for recursive modules
– Soundness proved via progress/preservation
Isn’t It Complicated?
Isn’t It Complicated?
• No
Isn’t It Complicated?
• No
• Typing judgment for terms essentially same as Definition’s:
Isn’t It Complicated?
• No
• Traditional Definition-style typing judgment (a la Russo):
Isn’t It Complicated?
• No
• Our new declarative typing judgment:
Isn’t It Complicated?
• No
• Our new declarative typing judgment:
• Moreover, type inference becomes much simpler
Example (c)
Example (c) is Not Well-Typed
According to the Definition
Not in scope!
Distinguishing (b) and (c)
• Involves tracking dependencies between abstract types and
unification variables
– Only 1.5 out of 9 SML implementations get it right
• Russo’s thesis (2000) gives an inference algorithm based
on Miller’s technique of unification under a mixed prefix
– But does not prove that it works
– Algorithm doesn’t accept Example (a)
In Our System,
Example (c) is Well-Typed
No problem!
What Else Is In the Paper
• Full formalization of declarative semantics and inference
algorithm
– Hybrid of Definition and Harper-Stone semantics
– Type soundness proven by reduction to RTG
(reduction in tech report)
• Principal types theorem stated (proof in tech report)
“Benchmarks”
• Reject All: SML/NJ, ML-Kit, TILT, SML.NET, Hamlet
• Mixed Bag: Poly/ML, Alice, Moscow ML (interactive mode)
• MLton: Success relies on whole-program compilation,
defunctorization coupled with typechecking
“Benchmarks”
• Reject All: SML/NJ, ML-Kit, TILT, SML.NET, Hamlet
• Mixed Bag: Poly/ML, Alice, Moscow ML (interactive mode)
• MLton: Success relies on whole-program compilation,
defunctorization coupled with typechecking
Obrigado!
Descargar

Document