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