A.A. 2000-01

Linguaggi di Programmazione I: Paradigmi

secondo “esonero”

data di assegnazione: 5 dicembre 2000 data di consegna: 21 dicembre 2000

1 Mini-ML polimorfo con let

Considerare il seguente sottoinsieme del linguaggio ML. Usiamo le metavariabili M ed N per indicare termini generici:

M ::= 0 | 1 | … | true | false | x | fn x ⇒ M | M N | let x = M in N

Definire un sistema dei tipi per questo linguaggio che sia in accordo con quello di ML.

Suggerimenti. Si prendano come tipi base int e bool. Il sistema dei tipi è essenzialmente quello definito a lezione per il Mini-ML polimorfo senza costrutto let. Per quest’ultimo, ispirarsi a fn.

2 Algoritmo di inferenza dei tipi

1. Estendere l’algoritmo W di inferenza dei tipi visto a lezione con una clausola per gestire il costrutto let.

2. Applicare l’algoritmo (mostrando tutti i passaggi) al termine:

fn z ⇒ (let x = (fn y ⇒ z) in ((x z) ((x 5) true)))

3. Applicare l’algoritmo (mostrando tutti i passaggi) al termine:

fn z ⇒ (let x = (fn y ⇒ z) in ((x z) (x 5)))

Suggerimenti. Nel cercare il tipo di N in un termine della forma let x = M in N, attenzione ad assegnare un tipo sufficientemente “generale” alla variabile x. Controllate che, applicando l’algoritmo agli esempi dati, si ottengano risultati intuitivamente corretti! … o altrimenti dimostrate …

3 Correttezza dell’algoritmo

… che se W (Γ, t) = (S, τ), dove W è l’algoritmo sviluppato nell’esercizio precedente, allora è possibile derivare S Γ ⊢ t : τ nel sistema dei tipi. Molto facoltativo!

Buon lavoro!