Unita' di Genova, Linguaggi Funzionali

• (1.1 persone): Moggi, Belle', Calcagno
• (1.1 compito) Si studieranno semantiche intensionali per modellare una varieta' di aspetti (p.e. distinzione di fase, struttura dei tipi di dato), che saranno poi utilizzate per lo sviluppo di linguaggi intermedi a due livelli (adottati nell'ambito della ottimizzazione basata sulla tecnica della "partial evaluation") e come fondamento per tecniche di analisi statica di programmi ad alto livello per architetture paralleli.
• (1.1 obbiettivi primo anno) Semantica dei linguaggi a due livelli per "partial evalutation", ed applicazioni alla verifica di correttezza della fase di specializzazione.
• (1.1 obbiettivi secondo anno) Tecniche di analisi statica degli errori di shape e tecniche di ottimizzazione di programmi che sfruttano l'informazione statica sulle shape.

Risultati di maggior rilievo conseguiti nel corso dell'attivita di ricerca

Relazione con la tempistica iniziale del programma

Corrispondenza con i criteri di verificabilita` enunciati nella proposta originale

A seguito di cio' si e' deciso di ridirigere il campo di applicazione, cio' ha dato luogo ad una collaborazione con OGI, che ha portato a vari articoli [MTBS99, BMTS99, CMT99] rappresentano un importante contributo alla comprensione dei linguaggi per la programmazione multi-stage (in particolare MetaML).

I lavori [JBM98] e [MBJ99] sono preliminari agli obbiettivi che erano stati indicati originariamente per la seconda fase. Tsli obbiettivi non saranno raggiunti prima della fine del progetto.

Carattere innovativo in rapporto allo stato dell'arte nel campo

Resoconto secondo Anno (01/02/1999 - 15/02/2000)

Riferimenti Bibliografici (ordine cronologico inverso)

• [CMT99] Mini-MetaML with References, Calcagno, C., Moggi, E., Taha, W., Tech. Report, DISI, University of Genova, DISI-TR-99-17, 1999, http://www.disi.unige.it/person/MoggiE/ftp/TR-99-17,
         MetaML extends core SML with multi-stage programming constructs. Previous studies of the formal semantics and type systems for multi-stage programming languages do not explain how computational effects, e.g. state, can be safely used in MetaML. At the level of the untyped operational semantics, introducing references can lead to scope extrusion of lambda bound variables. Because of scope extrusion, a naive extension of the type systems with a type constructor for references invalidates type safety. The approach we propose here uses the Closed type constructor -- introduced elsewhere for typing MetaML's Run -- to ensure type safety by allowing only the storage of closed values. We expect this approach to work also with other computational effects.
• [MP99] Monadic Encapsulation of Effects: a Revised Approach, Moggi, E., Palumbo, F., HOOTS '99, Elsevier, ENTCS, 26, 1999, http://www.disi.unige.it/person/MoggiE/ftp/hoots99,
         Launchbury and Peyton-Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the bogus type parameter of the original proposal. The second contribution is a stronger type safety result, namely encapsulation of strict state in higher-order lambda-calculus. We formalise the intended implementation as a very simple big-step operational semantics on untyped terms, which captures interesting implementation details not captured by the reduction semantics proposed previously.
• [BMTS99] Logical Modalities and Multi-Stage Programming, Benaissa, Z., Moggi, E, Taha, W., Sheard, T., IMLA, FLoC'99 Workshop 1999, http://www.disi.unige.it/person/MoggiE/ftp/imla99,
         Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. This paper makes a case for multi-stage programming with open code and closed values. We argue that a simple language exploiting interactions between two logical modalities is well suited for multi-stage programming, and report the results from our study of categorical models for multi-stage languages.
• [MBJ99] Monads, Shapely Functors and Traversals, Moggi, E., Bellè, G., Jay, C. B., CTCS '99, Elsevier, ENTCS, 29, 1999, http://www.disi.unige.it/person/MoggiE/ftp/ctcs99,
         This paper demonstrates the potential for combining the polytypic and monadic programming styles, by introducing a new kind of combinator, called a traversal. The natural setting for defining traversals is the class of shapely data types. This result reinforces the view that shapely data types form a very natural domain for polytypism: they include most of the data types of interest, while to exceed them would sacrifice a very smooth interaction between polytypic and monadic programming.
• [MTBS99] An Idealized MetaML: Simpler, and More Expressive, Moggi, E, Taha, W., Benaissa, Z., Sheard, T., ESOP '99, Springer Verlag, LNCS, 1576, 1999, http://www.disi.unige.it/person/MoggiE/ftp/esop99,
         MetaML is a multi-stage functional programming language featuring three constructs that can be viewed as statically-typed refinements of the back-quote, comma, and eval of Scheme. Thus it provides special support for writing code generators and serves as a semantically-sound basis for systems involving multiple interdependent computational stages. In previous work, we reported on an implementation of MetaML, and on a small-step semantics and type-system for MetaML. In this paper, we present An Idealized MetaML (AIM) that is the result of our study of a categorical model for MetaML. An important outstanding problem is finding a type system that provides the user with a means for manipulating both open and closed code. This problem has eluded efforts by us and other researchers for over three years. AIM solves the issue by providing two type constructors, one classifies closed code and the other open code, and describing how they interact.

• [Cal98] Two-Level Languages for Program Optimization, Calcagno, C., submitted to the special issue of TCS for MFPS XIV, 1998, http://www.disi.unige.it/person/MoggiE/ftp/mfps14,
         Two-level languages incorporate binding tim information inside types, that is, whether a piece of code is completely known at compile-time, or needs some more inputs and can be evaluated only at run-time. We consider the use of 2-level languages in the framework of partial evaluation, and use a 2-level version of the simply typed lambda-calculus with recursion. We give an operational semantics, an equational theory and a denotational semantics, that give an account of the distinction between compilation and execution phases. An adequacy theorem is given to relate the two semantics, showing in particular how they agree on non-termination at compile-time. We finally give a more refined model using functor categories.
• [Mog98] Functor Categories and two-level Languages, Moggi, E., FoSSaCS '98, Springer Verlag, LNCS, 1378, 1998, http://www.disi.unige.it/person/MoggiE/ftp/fossacs98,
         We propose a denotational semantics for the two-level language lambda-mix, and prove its correctness w.r.t. a standard denotational semantics. Other researchers have claimed correctness for lambda-mix (or extensions of it) based on denotational models, but the proofs of such claims rely on imprecise definitions and are basically flawed. At a technical level there are two important differences between our model and more naive models inCpo: the domain for interpreting dynamic expressions is more abstract, the semantics of"newname" is handled differently (we exploit functor categories). The key idea is tointerpret a two-level language in a suitable functor category rather than Cpo. The semantics of "newname" follows the ideas pioneered by Oles and Reynolds for modelingthe stack discipline of Algol-like languages. Correctness is proved using Kripke logicalrelations.
• [MBJ98] Monads, Shapely Functors and Traversals, Moggi, E., Bellè, G., Jay, C. B., DISI - University of Genova, No. DISI-TR-98-06, 1998, http://www.disi.unige.it/person/MoggiE/ftp/TR-98-06,
         This paper demonstrates the potential for combining the polytypic and monadic programming styles, by introducing a new kind of combinator, called a traversal. The natural setting for defining traversals is the class of shapely data types. This result reinforces the view that shapely data types form a very natural domain for polytypism: they include most of the data types of interest, while to exceed them would sacrifice a very smooth interaction between polytypic and monadic programming.
• [JBM98] Functorial ML, Jay, B., Belle', G., Moggi, E., JFP, 8, No. 6, 1998, http://www.disi.unige.it/person/MoggiE/ftp/jfp98,
         We present an extension of the Hindley-Milner type system that supports a generous class of type constructors called functors, and provide a parametrically polymorphic algorithm for their mapping, i.e. for applying a function to each datum appearing in a value of constructed type. The algorithm comes from shape theory, which provides a uniform method for locating data within a shape. The resulting system is Church-Rosser and strongly normalizing, and supports type inference. Several different semantics are possible, which affects the choice of constants in the language, and are used to illustrate the relationship to polytypic programming.

• [BM97] Typed intermediate languages for shape analysis, Belle', G., Moggi, E., TLCA '97, Springer Verlag, LNCS, 1210, 1997
• [Mog97] A categorical account of two-level languages, Moggi, E., MFPS XIII, Elsevier, ENTCS, 1997