The gradualizer: a methodology and algorithm for generating gradual type systems
- 11 January 2016
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 51 (1), 443-455
- https://doi.org/10.1145/2914770.2837632
Abstract
Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.Keywords
Funding Information
- National Science Foundation (1518844)
This publication has 26 references indexed in Scilit:
- Session Types with Gradual TypingLecture Notes in Computer Science, 2014
- Gradual typing for SmalltalkScience of Computer Programming, 2014
- Understanding TypeScriptLecture Notes in Computer Science, 2014
- Gradual TypestateLecture Notes in Computer Science, 2011
- Space-efficient gradual typingHigher-Order and Symbolic Computation, 2010
- Well-Typed Programs Can’t Be BlamedPublished by Springer Science and Business Media LLC ,2009
- Exploring the Design Space of Higher-Order CastsLecture Notes in Computer Science, 2009
- Gradual Typing for ObjectsLecture Notes in Computer Science, 2007
- A typed foundation for directional logic programmingLecture Notes in Computer Science, 1993
- Automatic mode inference for logic programsThe Journal of Logic Programming, 1988