Type checking recursive ML-style modules with fully applicative functors

Keiko Nakata

Institute of Cybernetics

Thursday, 6 November 2008, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: The ML module system supports flexible development of large software programs by offering nested structures, functors and signature constraints. In spite of this flexibility, recursion between modules is impossible since dependencies between modules must accord with the order of definitions. As a result of this constraint, programmers may have to consolidate conceptually separate components into a single module, intruding on modular programming. Introducing recursive modules is a natural way out of this predicament. Yet the combination of this rich module system and recursion introduces several issues to be considered.

In this talk I will examine and address some of difficulties in type checking ML-style modules supporting recursion and fully applicative functors.

Tarmo Uustalu
Last update 6.11.2008