A practical type system for generalized recursion

Abstract : The ML language is equipped with a sophisticated module system, especially thanks to its notions of functor (higher-order functions on modules) and of controlled type abstraction (opaque or transparent types). Nevertheless, an important weakness of this system hinders modularization: the impossibility to define mutually recursive modules. In particular, mutually recursive functions must all reside in the same module. Recently, Leroy extended the OCaml language, a dialect of ML, with an unsafe notion of recursive modules. In this extension, one can define recursive modules, but the system does not check that they are well-founded. If not, the system throws an exception at runtime, which is annoying given the strong typing of ML. Powerful type systems have been proposed to tackle this issue, but they require rather deep modifications to the ML type system. This report presents a system requiring only local modifications to the ML type system. We prove its soundness by injection into one of the evoked more general formalisms.
Document type :
Complete list of metadatas

Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 1:54:41 PM
Last modification on : Friday, April 19, 2019 - 1:38:17 AM


Files produced by the author(s)


  • HAL Id : hal-02102506, version 1



Tom Hirschowitz, Serguei Lenglet. A practical type system for generalized recursion. [Research Report] Laboratoire de l'informatique du parallélisme. 2005, 2+50p. ⟨hal-02102506⟩



Record views


Files downloads