Last updated 12/02/1999
by Eugenio Moggi.
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
Si sono rispettate le tempistiche previste per la prima fase. Si
pensa di rivedere gli obbiettivi della seconda fase per continuare
l'attivita' iniziata con [MTBS98].
Corrispondenza con i criteri di verificabilita` enunciati nella
proposta originale
I lavori relativi agli obbiettivi per la prima fase sono:
[Mog98],
[Cal98].
Nel corso del primo anno ci si e' resi conto che le semantiche
sviluppate nel progetto potevano avere un impatto molto rilevante per
lo sviluppo di linguaggi multi-stage. 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 ad articolo
[MTBS98].
I seguenti lavori sono invece preliminari agli obbiettivi per la
seconda fase:
[BJM98],
[BJM98b].
Carattere innovativo in rapporto allo stato dell'arte nel campo
[Mog98] introduce un approccio innovativo alla
modellazione dei linguaggi a due-livelli, che evita i difetti delle
semantiche denotazionali proposte in precedenza.
[Cal98] affronta tematiche tradizionali, che non
erano state esaminate nel contesto dei linguaggi a due-livelli.
[MTBS98] e' altamente innovativo, e propone il
primo linguaggio in cui si puo' manipolare sia codice chiuso (p.e. per
run-time code generation) che codice aperto (con tecniche di partial
evaluation).
Resoconto primo Anno (01/02/1998 - 31/01/1999)
[Mog98] propone una semantica per linguaggi
a due-livelli basata sulle categorie di funtori. Rispetto ad altre
semantiche denotazioni si ha una maggiore astrazione (gli elementi del
tipo code sono programmi modulo alfa-conversione) e vale un
risultato di full-abstraction limitatamente ai tipi
dinamici. La dimostrazione di correttezza rispetto ad una
semantica standard usa le logical relations a la Kripke, ed
evita gli errori ed imprecisioni presenti nelle dimostrazioni di
correttezza pubblicate in precedenza.
Sebbene il linguaggio considerato e' particolarmente semplice (si
tratta di lambda-mix), la semantica sembra facilmente estendibile a
liguaggi piu' complessi.
[Cal98] analizza le relazioni tra semantica
operazionale, semantica denotazionale e calcolo equazionale per una
variante di PCF a due-livelli. Questo tipo di analisi e' tipica dei
linguaggi di programmazione. Nel contesto dei linguaggi a due-livelli
vi sono varie osservazioni possibili.
L'articolo prendere come osservazioni base due tipi di terminazione,
quella a tempo di compilazione e quella a tempo di esecuzione, e
dimostra che vale un risultato di adequatezza computazionale per due
semantica denotazionali, una in CPO e l'altra in CPO^2 (che ricade nel
framework proposto in [Mog97]).
[MTBS98] e' il frutto della collaborazione
con ricercatori dell'Oregon Graduate Center che da tempo si occupano
di linguaggi per computazioni multi-stage. Il linguaggio
proposto, AIM, e' il primo tra i linguaggi a due o piu' livelli che
permette di manipolare sia codice aperto che codice chiuso. Un
contributo essenziale per concepire il linguaggio ed il type system e'
venuto da una semantica categoriale (non descritta nell'articolo) che
generalizza quella proposta in [Mog97].
Precedenti lavori di Pfenning e Davies hanno stabilito delle
corrispondenze tra linguaggi multi-livello e logica modale e
temporale, sarebbe interessante verificare se tale corrispondenza
si estende ad AIM.
[BJM98] e [BJM98b]
descrivono Functorial ML e sue estensioni, studiandone sia gli
aspetti sintattici che semantici. Sebbene, tali articoli non sono
direttamente rilevanti agli obbiettivi del progetto, Functorial ML e'
un liguaggio che si presta ad essere analizzato in termini di
linguaggi a due livelli (vedi [BM97]), per
evidenziare il trattamento a tempo di compilazione delle informazioni
sulla struttura dei tipi di dato rappresentati da funtori.
Riferimenti Bibliografici
- [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
- [MTBS98]
An Idealized MetaML: Simpler, and More Expressive,
Moggi, E, Taha, W., Benaissa, Z., Sheard, T.,
Springer Verlag,
LNCS,
????,
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.
- [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.
- [BJM98]
Functorial ML,
Belle', G., Jay, B., 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.
- [BJM98b]
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.
- [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.