A Type System for First-Class Recursive ML Modules

Abstract

Standard ML (SML), OCaml and other programming languages in the ML language family offer a particularly expressive module system. This ML module system provides hierarchical namespacing with structures, fine-grained interfaces with translucent signatures, implementation- side data abstraction with sealing as well as client side data-abstraction and generic programming with functors.

Languages with the ML module system are stratified into two levels: core ML and modules. There is extensive duplication of functionality between these levels: records and structures, types and signatures, functions and functors. The second-class nature of modules also limits expres- sivity as some features are available only in core ML or only in modules.

ML languages typically limit recursive definitions to very specific patterns: groups of mutually recursive functions or type definitions connected with and keywords. The restriction on type def- initions ensures that equirecursive types are not needed. The restriction on function definitions ensures that recursive values are well-founded, preventing runtime use of uninitialized values.

Recursive modules are not part of the Definition of Standard ML but are supported by language extensions in several SML compilers as well as OCaml. Just like mutually recursive functions and types, mutually recursive modules are invariably required to be syntactically grouped together. Implementations of recursive ML modules also struggle with the double vision and recursive link- ing problems. In double vision a recursive module implementing abstract types fails to equate its exported abstract types with their implementations that should not be hidden inside the module. The recursive linking problem is to find an elegant and statically well-founded method of recur- sively linking modules not defined in the same group of recursive definitions or maybe not even the same compilation unit.

The paper “1ML – Core and Modules United” successfully collapsed core ML and modules into one language with first-class modules. Recursive modules have been deployed in production compilers and several methods to avoid double vision are known from the literature. However first-class and recursive modules have not been combined despite the availability of intermedi- ate languages which can both act as targets of elaborating type systems like 1ML and support recursive modules.

This thesis develops Recursive 1ML (R1ML), a type system for recursive first-class modules. R1ML is an elaborating type system in the style of 1ML. R1ML targets a variant of System Fc , which was created as an intermediate language for the Glasgow Haskell Compiler (GHC). Haskell does not have ML modules but the parametric polymorphism and type equality coercions of Fc are general enough to support recursive first-class modules while avoiding the double vision problem. This thesis also proves that R1ML is sound and decidable but incomplete in several (tolerable) ways. There was no time nor space to consider the recursive linking problem.

Standard ML (SML), OCaml ja useat muut kielet ML-kieliperheessä omaavat erityisen ilmaisuvoimaisen moduulijärjestelmän. Tämä ML-moduulijärjestelmä tarjoaa hierarkkiset nimiavaruudet struktuureilla, hienojakoiset rajapinnat läpikuultavilla tunnisteilla, toteuttajan data-abstraktion sinetöinnillä ja käyttäjän data-abstraktion funktoreilla.

ML-moduuleilla varustetut kielet on kerrostettu kahteen kerrokseen: ydin-ML:ään ja moduuleihin. Näiden tasojen välillä esiintyy laajamittaista toiminnallisuuden toistoa: tietueet ja struktuurit, tyypit ja tunnisteet, funktiot ja funktorit. Myös moduulien toisluokkainen luonne rajoittaa ilmaisu- voimaa koska jotkin ominaisuudet ovat saatavilla vain ydin-ML:ssä tai vain moduuleissa.

Tyypillisesti ML-kielet rajoittavat rekursion vain tiettyihin muotoihin: and-avainsanalla yhdistettyjen keskinäisrekursiivisten funktio- tai tyyppimääritelmien ryhmiin. Tyyppimääritelmien rajoittaminen varmistaa, ettei ekvirekursiivisia tyyppejä tarvita. Funktiomääritelmien rajoittaminen varmistaa, että rekursiiviset arvot ovat hyvin perustettuja estäen ajonaikaisen alustamattomien arvojen käytön.

Rekursiiviset moduulit eivät ole osa Standard ML:n määritelmää mutta ovat tuettuja kielilaa- jennuksilla useissa SML-kääntäjissä kuten myös OCamlissa. Aivan kuten keskinäisrekursiiviset funktiot ja tyypit, keskinäisrekursiiviset moduulit täytyy poikkeuksetta ryhmitellä syntaktisesti yhteen. Rekursiivisten ML-moduulien toteutukset kamppailevat myös kaksinnäön ja rekursiivisen linkityksen ongelmien kanssa. Kaksinnäössä abstrakteja tyyppejä toteuttava moduuli epäonnistuu samaistamaan viemänsä abstraktit tyypit niiden toteutuksiin, joiden ei pitäisi olla olla kätkettyjä moduulin sisällä. Rekursiivisen linkityksen ongelma on elegantin ja staattisesti hyvin perustetun menetelmän löytäminen sellaiseen rekursiiviseen moduulien linkitykseen, jossa linkitettäviä moduuleja ei ole määritelty samassa rekursiivisten määritelmien ryhmässä tai ehkei edes samassa käännösyksikössä.

Artikkeli “1ML – Core and Modules United” luhisti menestyksekkäästi ydin-ML:n ja moduulit yhdeksi kieleksi, jossa on ensiluokkaiset moduulit. Rekursiiviset moduulit on otettu käyttön tuotantokääntäjissä ja kirjallisuudesta tunnetaan useita tapoja välttää kaksinnäkö. Ensiluokkaisia ja rekursiivisia moduuleja ei ole kuitenkaan yhdistetty vaikka saatavilla on välikieliä, jotka voivat sekä toimia 1ML:n tapaisten kehittelevien tyyppijärjestelmien kohteina että tukea rekursiivisia moduu- leja.

Tämä diplomityö kehittää Rekursiivisen 1ML:n (R1ML), joka on ensiluokkaisilla rekursiivisil- la moduuleilla varustettu tyyppijärjestelmä. R1ML on 1ML:n tyylinen kehittelevä tyypijärjestelmä. R1ML:n kehittelykohde on GHC:tä (Glasgow Haskell Compiler) varten kehitetty välikieli System Fc . Haskellissa ei ole ML-moduuleja, mutta System Fc :n parametrinen polymorfismi ja tyyppien yhtäläisyyspakotukset ovat riittävän yleisiä tukeakseen ensiluokkaisia rekursiivisia moduuleja vält- täen kaksinnäön. Tämä diplomityö myös todistaa, että R1ML on tyyppiturvallinen ja algoritmisesti ratkeava, mutta epätäydellinen useilla (siedettävillä) tavoilla. Rekursiivisen linkityksen ongelmien tarkasteluun ei ollut aikaa eikä tilaa.