A.A. 2000-01

Linguaggi di Programmazione I: Paradigmi

“esonero”

data di assegnazione: 17 novembre 2000 data di consegna: 1 dicembre 2000

1 Mini-ML

Considerare il seguente sottoinsieme del linguaggio ML. Usiamo le metavariabili T, T_{1} … per i tipi e M, N … per i termini:

T ::= Nat | T_{1} → T_{2}
M ::= 0 | 1 | … | x | fn x : T ⇒ M | M N

1. Definire un sistema dei tipi per Mini-ML.

2. Definire una semantica operazionale call-by-value per Mini-ML che sia in accordo con la semantica di ML.

Suggerimenti. Il sistema dei tipi è lo stesso definito in classe per F1. Semantica call-by-value vuol dire che l’argomento di una funzione viene valutato (ovvero ridotto ad un valore) prima di essere passato ad una funzione. Si prenda come nozione di valore la seguente:

– i termini 0, 1 … sono i valori di tipo Nat ;

– i termini della forma fn x : T ⇒ M sono i valori del corrispondente tipo freccia.

2 Mini-ML con eccezioni

Estendere il linguaggio Mini-ML con i seguenti costrutti per la gestione delle eccezioni: siano ϵ_{0}, ϵ_{1}, … ϵ_{n} un insieme predefinito di nomi di eccezioni,

T ::= … | Exc
M ::= … | ϵ(M) | raise_{T} M | M handle ϵ(x) ⇒ N

Le ϵ_{i} sono costruttori di eccezioni. In ML le eccezioni possono “trasportare” un valore, chiamato argomento, di tipo specificato, che può essere utilizzato da un eventuale handler. Supponiamo dunque che a ciascun costruttore ϵ sia associato un tipo τ(ϵ), quello del suo argomento.

In ML esiste un tipo predefinito Exc delle eccezioni. Chiamiamo eccezione un qualunque termine di tipo Exc. Dato un termine M di tipo τ(ϵ), il termine ϵ(M) è una eccezione, ed M è il suo argomento.

Per ogni tipo T e per ogni eccezione M, il termine raise_{T} M è un termine di tipo T, e può dunque comparire in qualunque contesto legittimo per T. Ad esempio, 3 + raise_{Nat} M è un termine ben formato di tipo Nat. Informalmente, l’esecuzione di raise_{T} M valuta il termine M producendo un valore ϵ(v) e poi solleva (lancia) l’eccezione ϵ con argomento v. (Nota che la valutazione di M potrebbe a sua volta lanciare una eccezione.) Una volta sollevata l’eccezione ϵ, il flusso normale della computazione si interrompe, e il controllo passa al primo (nel senso di più “interno”) handle ϵ(x) che racchiude sintatticamente il termine che ha generato l’eccezione. Se un tale costrutto non esiste, l’eccezione è il risultato dell’intero programma.

Il termine M handle ϵ(x) ⇒ N lega tutte le occorrenze libere di x in N. Informalmente, la sua valutazione consiste innanzitutto nella valutazione di M. Se questa produce un valore v, allora v è il risultato dell’intero termine. Se M produce una eccezione ϵ(w), allora viene eseguito lo “handler” N in un ambiente in cui x vale w. Se M produce una eccezione ϵ′(w) con ϵ ≠ ϵ′, l’eccezione non viene catturata e l’intero termine produce l’eccezione ϵ′(w). Tutto questo è come in ML.

1. Definire un sistema dei tipi per Mini-ML con eccezioni.

2. Definire una semantica operazionale call-by-value che sia in accordo con la semantica di ML.

3. Sia τ(ϵ) = Nat. Derivare:

– ∅ ⊢ (3 + raise_{Nat} ϵ(5 − 1)) handle ϵ(x) ⇒ (x + 2) : Nat

– ∅ ⊢ ((3 + raise_{Nat} ϵ(5 − 1)) handle ϵ(x) ⇒ (x + 2)) ⇒ 6

4. Sia τ(ϵ) = Exc → T, e sia t il seguente termine:

fn x : Exc ⇒ ((raise_{T} x) handle ϵ(y) ⇒ y x)

– Determinare il tipo del termine t ϵ(t).

– Esiste un valore v tale che ∅ ⊢ t ϵ(t) ⇒ v?

Suggerimenti. Si estenda la nozione di valore includendo i termini della forma ϵ(v), dove v è un valore. Si definisca l’insieme dei risultati come l’unione dell’insieme dei valori con quello dei termini della forma: raise_{T} v, dove v è un valore. Le asserzioni della semantica operazionale siano della forma:

E ⊢ t ⇒ r

dove r è un risultato ed E è in ambiente che associa valori a variabili. Buon lavoro!