Skip to Main content Skip to Navigation
Journal articles

A practical mode system for recursive definitions

Abstract : In call-by-value languages, some mutually-recursive 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 sourcelevel semantics of Nordlander, Carlsson, and Gill [2008], and show that it can be directed into an algorithmic backwards analysis 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 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. CCS Concepts: • Software and its engineering → General programming languages; Recursion.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-03125031
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Friday, January 29, 2021 - 10:51:56 AM
Last modification on : Friday, October 22, 2021 - 4:32:30 AM
Long-term archiving on: : Friday, April 30, 2021 - 6:36:15 PM

File

letrec.pdf
Files produced by the author(s)

Identifiers

Citation

Alban Reynaud, Gabriel Scherer, Jeremy Yallop. A practical mode system for recursive definitions. Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), pp.1-29. ⟨10.1145/3434326⟩. ⟨hal-03125031⟩

Share

Metrics

Les métriques sont temporairement indisponibles