1\chapter{Introduzione a ML} 2\label{ML} 3 4Questo capitolo � una breve introduzione al meta-linguaggio \ML. 5L'obiettivo � solo quello di dare una sensazione di come sia interagire con 6il linguaggio. Si pu� trovare un'introduzione pi� dettagliata 7in numerosi libri di testo e pagine web; si veda per esempio l'elenco delle risorse 8sulla home page 9di MoscowML\footnote{\url{http://www.dina.kvl.dk/~sestoft/mosml.html}}, 10o le FAQ 11\texttt{comp.lang.ml}\footnote{\url{http://www.faqs.org/faqs/meta-lang-faq/}}. 12 13\section{Come interagire con ML} 14 15\ML{} � un linguaggio di programmazione interattivo come il Lisp. Al livello 16dell'interprete si possono valutare espressioni ed eseguire dichiarazioni. Le prime 17risultano nella stampa a schermo del valore dell'espressione e del suo tipo, le seconde 18nel binding di un valore a un nome. 19 20Un modo standard di interagire con \ML{} � quello di configurare lo schermo 21della workstation in modo tale che ci siano due finestre: 22\begin{myenumerate} 23\item Una finestra di modifica in cui i comandi \ML{} sono inizialmente battuti 24 e registrati. 25\item Una finestra shell (o l'equivalente non-Unix) che � usata per 26 valutare i comandi. 27\end{myenumerate} 28 29\noindent 30Un modo comune per ottenere questo � lavorare all'interno di \ml{Emacs} con una 31finestra di testo e una finestra shell. 32 33Dopo ave battuto un comando sulla finestra di modifica (testo) esso pu� essere 34trasferito alla shell e valutato in \HOL{} con un `copia e incolla'. In 35\ml{Emacs} questo si ottiene copiando il testo in un buffer e poi facendo il 36suo `yanking' nella shell. Il vantaggio di lavorare con un editor � 37che se il comando ha un errore, allora il testo pu� essere modificato semplicemente 38e usato di nuovo; inoltre esso salva i comandi in un file che pu� poi 39essere usato di nuovo pi� avanti (attraverso un caricamento batch). In \ml{Emacs}, la finestra 40di shell registra anche la sessione, inclusi sia l'input dell'utente 41sia la risposta del sistema. Le sessioni in questo tutorial sono state prodotte 42in questo modo. Queste sessioni sono divise in segmenti mostrati in riquadri 43con un numero sul loro angolo superiore destro (per indicare la loro 44posizione nella sessione completa). 45 46Le interazioni in questi riquadri dovrebbero essere intese operare in 47sequenza. Per esempio, si assume che i binding delle variabili fatte in box precedenti 48persistano nei successivi. Per entrare nel sistema \HOL{} si 49digita {\small\verb|hol|} o {\small\verb|hol.noquote|} in Unix, 50eventualmente preceduti dall'informazione del percorso se la directory bin del sistema 51\HOL{} non � nel proprio percorso. Il sistema \HOL{} quindi 52stampa un messaggio di sign-on e ci colloca all'interno di \ML. Il prompt \ML{} � 53{\small\verb|-|}, perci� le righe cominciano con {\small\verb|-|} sono quelle digitate 54dall'utente e le altre righe sono le risposte del sistema. 55 56 Qui, come nelle altre parti del \TUTORIAL{}, assumeremo che si stia usando 57 {\small\verb|hol|}. 58 59\setcounter{sessioncount}{0} 60\begin{session}\begin{alltt} 61\$ bin/hol 62 63----------------------------------------------------------------- 64 HOL-4 [\holnsversion (built Fri Apr 12 15:34:35 2002)] 65 66 For introductory HOL help, type: help "hol"; 67----------------------------------------------------------------- 68 69[loading theories and proof tools ************* ] 70[closing file "/local/scratch/mn200/Work/hol98/tools/end-init-boss.sml"] 71- 1 :: [2,3,4,5]; 72> val it = [1, 2, 3, 4, 5] : int list 73\end{alltt} 74\end{session} 75 76L'espressione \ML{} {\small\verb|1 :: [2,3,4,5]|} ha la forma $e_1\ 77op\ e_2$ dove $e_1$ � l'espressione {\small\verb|1|} (il cui valore 78� l'intero $1$), $e_2$ � l'espressione {\small\verb|[2,3,4,5]|} 79(il cui valore � una lista di quattro interi) e $op$ � l'operatore 80infisso `{\small\verb|::|}' che � come la funzione del Lisp {\it cons}. 81Altre funzioni di elaborazione di liste includono {\small\verb|hd|} ($car$ in 82Lisp), {\small\verb|tl|} ($cdr$ in Lisp) e {\small\verb|null|} 83($null$ in Lisp). Il punto e virgola `{\small\verb|;|}' termina una 84frase complessiva. La risposta del sistema � mostrata sulla linea che comincia 85con il prompt {\small\verb|>|}. Essa consiste del valore 86dell'espressione seguito, dopo un segno di due punti, dal suo tipo. Il type checker di \ML{} 87deduce il tipo delle espressioni usando metodi inventati da Robin Milner 88\cite{Milner-types}. Il tipo {\small\verb|int list|} � il tipo delle 89`liste di interi'; {\small\verb|list|} � un operatore di tipo unario. 90Il sistema di tipi di \ML{} � molto simile al sistema di tipi della 91logica \HOL{} che � spiegata nel Capitolo~\ref{HOLlogic}. 92 93Il valore dell'ultima espressione valutata dal top level \ML{} � sempre 94memorizzata in una variabile chiamata {\small\verb|it|}. 95 96\begin{session} 97\begin{verbatim} 98- val l = it; 99> val l = [1, 2, 3, 4, 5] : int list 100 101- tl l; 102> val it = [2, 3, 4, 5] : int list 103 104- hd it; 105> val it = 2 : int 106 107- tl(tl(tl(tl(tl l)))); 108> val it = [] : int list 109\end{verbatim} 110\end{session} 111 112Seguendo gli standard del $\lambda$-calcolo, l'applicazione di una 113funzione $f$ a un argomento $x$ pu� essere scritta senza parentesi come $f\ 114x$ (bench� � permesso anche 115il pi� convenzionale $f${\small\verb|(|}$x${\small\verb|)|}). L'espressione 116$f\ x_1\ x_2\ \cdots\ x_n$ abbrevia l'espressione 117meno intelligibile {\small\verb|(|}$\cdots${\small\verb|((|}$f\ x_1$% 118{\small\verb|)|}$x_2${\small\verb|)|}$\cdots${\small\verb|)|}$x_n$ 119(l'applicazione di funzione � associativa a sinistra). 120 121Le dichiarazioni hanno la forma {\small\verb|val |}$x_1${\small\verb|=|}$e_1${\small\verb| and |}$\cdots 122${\small\verb| and |}$x_n${\small\verb|=|}$e_n$ e hanno l'effetto che il valore di 123ogni espressione $e_i$ venga legato al nome $x_i$. 124 125\begin{session} 126\begin{verbatim} 127- val l1 = [1,2,3] and l2 = ["a","b","c"]; 128> val l1 = [1, 2, 3] : int list 129 val l2 = ["a", "b", "c"] : string list 130\end{verbatim} 131\end{session} 132 133Espressioni \ML{} come {\small\verb|"a"|}, {\small\verb|"b"|}, 134{\small\verb|"foo"|} \etc\ sono {\it stringhe\/} e hanno il tipo 135{\small\verb|string|}. Qualsiasi sequenza di caratteri {\small ASCII} pu� 136essere scritta tra virgolette\footnote{I caratteri di nuova riga devono essere scritti come 137 \ml{$\backslash$n}, e le virgolette come \ml{$\backslash$"}.}. La funzione 138{\small\verb|explode|} divide una stringa in una lista di caratteri 139singoli, che sono scritti come stringhe di un singolo carattere, con 140anteposto un carattere {\small\verb|#|}. 141 142\begin{session} 143\begin{verbatim} 144- explode "a b c"; 145> val it = [#"a", #" ", #"b", #" ", #"c"] : char list 146\end{verbatim} 147\end{session} 148 149Un'espressione della forma 150{\small\verb|(|}$e_1${\small\verb|,|}$e_2${\small\verb|)|} viene valutata 151a una coppia dei valori di $e_1$ e $e_2$. Se $e_1$ ha il tipo 152$\sigma_1$ e $e_2$ ha il tipo $\sigma_2$ allora 153{\small\verb|(|}$e_1${\small\verb|,|}$e_2${\small\verb|)|} ha il tipo 154$\sigma_1${\small\verb|*|}$\sigma_2$. Il primo e il secondo componente 155di una coppia possono essere estratti con le funzioni \ML{} {\small\verb|#1|} 156e {\small\verb|#2|} rispettivamente. Se una tupla ha pi� di due componenti, 157il suo $n$-esimo componente pu� essere estratto con una funzione 158{\small\verb|#|$n$}. 159 160I valori {\small\verb|(1,2,3)|}, {\small\verb|(1,(2,3))|} e 161{\small\verb|((1,2), 3)|} sono tutti distinti e hanno i tipi 162\linebreak{} {\small\verb|int * int * int|}, {\small\verb|int * (int * int)|} and 163{\small\verb|(int * int) * int|} rispettivamente. 164 165\begin{session} 166\begin{verbatim} 167- val triple1 = (1,true,"abc"); 168> val triple1 = (1, true, "abc") : int * bool * string 169- #2 triple1; 170> val it = true : bool 171 172- val triple2 = (1, (true, "abc")); 173> val triple2 = (1, (true, "abc")) : int * (bool * string) 174- #2 triple2;; 175> val it = (true, "abc") : bool * string 176\end{verbatim} 177\end{session} 178 179\noindent L'espressioni \ML{} {\small\verb|true|} e {\small\verb|false|} 180denotano i due valori di verit� di tipo {\small\verb|bool|}. 181 182I tipi \ML{} possono contenere {\it variabili di tipo\/} {\small\verb|'a|}, 183{\small\verb|'b|}, {\small\verb|'c|}, \etc\ Tali tipi sono chiamati {\it 184polimorfici\/}. Una funzione con un tipo polimorfico dovrebbe essere pensata come 185se possedesse tutti i tipi che si possono ottenere sostituendo le variabili di tipo con dei tipi. 186Questo � illustrato di sotto con la funzione {\small\verb|zip|}. 187 188Le funzioni sono definite con dichiarazioni della forma {\small\verb|fun|}$\ f\ 189v_1\ \ldots\ v_n$ \ml{=} $e$ dove ciascuna $v_i$ � o una variabile o un pattern 190composto di variabili. 191 192La funzione {\small\verb|zip|}, di sotto, converte una coppia di liste 193{\small\verb|([|}$x_1${\small\verb|,|}$\ldots${\small\verb|,|}$x_n$% 194{\small\verb|], [|}$y_1${\small\verb|,|}$\ldots${\small\verb|,|}$y_n$% 195{\small\verb|])|} in una lista di coppie 196{\small\verb|[(|}$x_1${\small\verb|,|}$y_1${\small\verb|),|}$\ldots$% 197{\small\verb|,(|}$x_n${\small\verb|,|}$y_n${\small\verb|)]|}. 198 199\begin{session} 200\begin{verbatim} 201- fun zip(l1,l2) = 202 if null l1 orelse null l2 then [] 203 else (hd l1,hd l2) :: zip(tl l1,tl l2); 204> val zip = fn : 'a list * 'b list -> ('a * 'b) list 205 206- zip([1,2,3],["a","b","c"]); 207> val it = [(1, "a"), (2, "b"), (3, "c")] : (int * string) list 208\end{verbatim} 209\end{session} 210 211Le funzioni possono essere {\it curried\/}, \ie\ prendono i lori argomenti `uno alla volta' 212al posto che come una tupla. Questo � illustrato con la funzione 213{\small\verb|curried_zip|} di sotto: 214 215\begin{session} 216\begin{verbatim} 217- fun curried_zip l1 l2 = zip(l1,l2); 218> val curried_zip = fn : 'a list -> 'b list -> ('a * 'b) list 219 220- fun zip_num l2 = curried_zip [0,1,2] l2; 221> val zip_num = fn : 'a list -> (int * 'a) list 222 223- zip_num ["a","b","c"]; 224> val it = [(0, "a"), (1, "b"), (2, "c")] : (int * string) list 225\end{verbatim} 226\end{session} 227 228La valutazione di un'espressione o {\it ha successo\/} o {\it 229 fallisce\/}. Nel primo caso, la valutazione restituisce un valore; nel 230secondo caso la valutazione � interrotta ed � sollevata 231un'\emph{eccezione}. Questa eccezione � passata a qualunque cosa abbia invocato la valutazione. 232Questo contesto pu� o propagare il fallimento (questo � il default) o 233pu� {\it gestirlo\/}. Queste due possibilit� sono illustrate di sotto. 234La gestione di un'eccezione � un'espressione della forma 235$e_1${\small\verb| handle _ => |}$e_2$. Un'espressione di questa forma � 236valutata valutando per prima cosa $e_1$. Se la valutazione ha successo (\ie\ 237non fallisce) allora il valore dell'intera espressione � il valore di 238$e_1$. Se la valutazione di $e_1$ ha sollevato un'eccezione, allora il valore 239dell'intera espressione � ottenuto valutando $e_2$.\footnote{Questa 240 descrizione della gestione dell'eccezioni � di fatto una semplificazione grossolana 241 del modo in cui le eccezioni possono essere gestite in \ML{}; si consulti un testo appropriato 242 per una spiegazione migliore.}. 243 244\begin{session} 245\begin{verbatim} 246- 3 div 0; 247! Uncaught exception: 248! Div 249 250- 3 div 0 handle _ => 0; 251> val it = 0 : int 252\end{verbatim} 253\end{session} 254 255Le sessioni di sopra sono sufficienti per dare un idea dell'\ML. Nel prossimo 256capitolo, sar� introdotta la logica supportata dal sistema \HOL{} (la logica di 257ordine superiore), insieme con gli strumenti all'interno di \ML{} per 258manipolarla. 259 260%%% Local Variables: 261%%% mode: latex 262%%% TeX-master: "tutorial" 263%%% End: 264