A practical mode system for recursive definitions
View / Open Files
Authors
Reynaud, A
Scherer, G
Yallop, J
Publication Date
2021Journal 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.
Keywords
recursion, call-by-value, types, semantics, ML, functional programming
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 current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk
The following licence files are associated with this item: