Principal Type Schemes for Gradual Programs
- 14 January 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Abstract
Gradual typing is a discipline for integrating dynamic checking into a static type system. Since its introduction in functional languages, it has been adapted to a variety of type systems, including object-oriented, security, and substructural. This work studies its application to implicitly typed languages based on type inference. Siek and Vachharajani designed a gradual type inference system and algorithm that infers gradual types but still rejects ill-typed static programs. However, the type system requires local reasoning about type substitutions, an imperative inference algorithm, and a subtle correctness statement. This paper introduces a new approach to gradual type inference, driven by the principle that gradual inference should only produce static types. We present a static implicitly typed language, its gradual counterpart, and a type inference procedure. The gradual system types the same programs as Siek and Vachharajani, but has a modular structure amenable to extension. The language admits let-polymorphism, and its dynamics are defined by translation to the Polymorphic Blame Calculus. The principal types produced by our initial type system mask the distinction between static parametric polymorphism and polymorphism that can be attributed to gradual typing. To expose this difference, we distinguish static type parameters from gradual type parameters and reinterpret gradual type consistency accordingly. The resulting extension enables programs to be interpreted using either the polymorphic or monomorphic Blame Calculi.Keywords
Funding Information
- National Science Foundation (1360694)
- Natural Sciences and Engineering Research Council of Canada
This publication has 27 references indexed in Scilit:
- Operational semantics for multi-language programsACM Transactions on Programming Languages and Systems, 2009
- Exploring the Design Space of Higher-Order CastsLecture Notes in Computer Science, 2009
- Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!Published by Springer Science and Business Media LLC ,2008
- Gradual Typing for ObjectsLecture Notes in Computer Science, 2007
- Practical type inference for arbitrary-rank typesJournal of Functional Programming, 2007
- Simple imperative polymorphismHigher-Order and Symbolic Computation, 1995
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994
- Automatic mode inference for logic programsThe Journal of Logic Programming, 1988
- A theory of type polymorphism in programmingJournal of Computer and System Sciences, 1978
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965