
arXiv: 1811.08134
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 source-level 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.
FOS: Computer and information sciences, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer Science - Programming Languages, functional programming, ML, 004, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], 46 Information and Computing Sciences, call-by-value, recursion, types, semantics, 4612 Software Engineering, Programming Languages (cs.PL)
FOS: Computer and information sciences, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer Science - Programming Languages, functional programming, ML, 004, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], 46 Information and Computing Sciences, call-by-value, recursion, types, semantics, 4612 Software Engineering, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
