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 :
Reports
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02102506
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 1:54:41 PM
Last modification on : Friday, April 19, 2019 - 1:38:17 AM

File

RR2005-22.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102506, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

9

Files downloads

9