A practical mode system for recursive definitions
View / Open Files
Authors
Reynaud, A
Scherer, G
Yallop, Jeremy
Publication Date
2021-01-04Journal Title
Proceedings of the ACM on Programming Languages
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Volume
5
Issue
POPL
Language
English
Type
Conference Object
This Version
VoR
Metadata
Show full item recordCitation
Reynaud, A., Scherer, G., & Yallop, J. (2021). A practical mode system for recursive definitions. Proceedings of the ACM on Programming Languages, 5 (POPL) https://doi.org/10.1145/3434326
Abstract
In call-by-value languages, some mutually-recursive value definitions can be
safely evaluated to build recursive functions or cyclic data structures, but
some definitions (let rec x = x + 1) contain vicious circles and their
evaluation fails at runtime. We propose a new static analysis to check the
absence of such runtime failures.
We present a set of declarative inference rules, prove its soundness with
respect to the reference source-level semantics of Nordlander, Carlsson, and
Gill (2008), and show that it can be (right-to-left) directed into an
algorithmic check in a surprisingly simple way.
Our implementation of this new check replaced the existing check used by the
OCaml programming language, a fragile syntactic/grammatical criterion which let
several subtle bugs slip through as the language kept evolving. We document
some issues that arise when advanced features of a real-world functional
language (exceptions in first-class modules, GADTs, etc.) interact with safety
checking for recursive definitions.
Identifiers
External DOI: https://doi.org/10.1145/3434326
This record's URL: https://www.repository.cam.ac.uk/handle/1810/296005
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The following licence files are associated with this item: