A right-to-left type system for mutually-recursive value definitions
Gabriel Scherer, Inria
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 static analysis to check the absence of such runtime failures.
We present a set of declarative inference rules, prove its soundness with respect to a reference source-level semantics, 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