Implementazione del -calcolo tipato definizione di nuovi tipi ricorsivi



Scaricare 0.6 Mb.
17.12.2017
Dimensione del file0.6 Mb.


    • implementazione del -calcolo tipato
    • definizione di nuovi tipi ricorsivi
    • i valori dei nuovi tipi sono termini, che possono essere visitati con un meccanismo di pattern matching (versione semplificata dell’unificazione)
    • scoping statico (a differenza di LISP)
    • semantica statica molto potente (inferenza e controllo dei tipi)
      • un programma “corretto” per la semantica statica quasi sempre va bene
    • gestione della memoria a heap con garbage collector



nucleo funzionale puro

  • nucleo funzionale puro

    • funzioni (ricorsive)
    • tipi e pattern matching
    • primitive utili: liste
  • componente imperativo

  • moduli e oggetti

  • meccanismi per la definizione di tipi e di tipi di dato astratto



Applicazione: macchina astratta

  • semantica operazionale: implementazione e strutture a tempo di esecuzuioone

  • riprenderemo l’interprete di un semplice linguaggio imperativo (frammento C) visto a Programmazione I

  • vedremo come utilizzare le caratteristiche del linguaggio ad oggetti (meccanismi di astrazione sui dati)



Seguendo il tutorial

  • sessione interattiva

  • l’utente scrive frasi CAML che iniziano con prompt #

  • a seguito del prompt, il sistema compila le frasi, le esegue e stampa il risultato della valutazione

  • per ogni frase il risultato e’ un valore ed il tipo (type inference)



Objective Caml version 2.00+3/Mac1.0a1

  • Objective Caml version 2.00+3/Mac1.0a1

  • # 25;;

  • - : int = 25

  • # true;;

  • - : bool = true

  • # 23 * 17;;

  • - : int = 391

  • # true & false;;

  • - : bool = false

  • # 23 * true;;

  • This expression has type bool but is here used with type int

  • # if 2 = 3 then 23 * 17 else 15;;

  • - : int = 15

  • # if 2 = 3 then 23 else true;;

  • This expression has type bool but is here used with type int



# function x -> x + 1;;

  • # function x -> x + 1;;

  • - : int -> int =

  • # (function x -> x + 1) 3;;

  • - : int = 4

  • # (function x -> x + 1) true;;

  • This expression has type bool but is here used with type int



# function x -> x;;

  • # function x -> x;;

  • - : 'a -> 'a =

  • # function x -> function y -> x y;;

  • - : ('a -> 'b) -> 'a -> 'b =

  • # (function x -> x) 2;;

  • - : int = 2

  • # (function x -> x) (function x -> x + 1);;

  • - : int -> int =

  • # function (x, y) -> x + y;;

  • - : int * int -> int =

  • # (function (x, y) -> x + y) (2, 33);;

  • - : int = 35





# let x = 3;;

  • # let x = 3;;

  • val x : int = 3

  • # x;;

  • - : int = 3

  • # let y = 5 in x + y;;

  • - : int = 8

  • # y;;

  • Unbound value y

  • (definizione globale/locale)



# let f = function x -> x + 1;;

  • # let f = function x -> x + 1;;

  • val f : int -> int =

  • # f 3;;

  • - : int = 4

  • # let f x = x + 1;;

  • val f : int -> int =

  • # f 3;;

  • - : int = 4

  • # let fact x = if x = 0 then 1 else x * fact(x - 1) ;;

  • Unbound value fact



# let rec fact x = if x = 0 then 1 else x * fact(x - 1) ;;

  • # let rec fact x = if x = 0 then 1 else x * fact(x - 1) ;;

  • val fact : int -> int =

  • # fact (x + 1);;

  • - : int = 24



Type



# type ratio={num:int; denum:int};;

  • # type ratio={num:int; denum:int};;

  • type ratio={num:int; denum:int}

  • # let x={num=1;denum=3);;

  • val x: ratio={num=1;denum=3;}

  • # x.num;;

  • - int =1

  • un record per memorizzare numeri razionali

  • creare e selezionare i campi



enumera tutti i casi che possono assumere i valori di quel tipo

  • enumera tutti i casi che possono assumere i valori di quel tipo

  • ogni caso e’ identificato da un nome (costruttore) che serve per costruire valori di quel tipo e per riconscerlo per pattern-matching

  • utile per definire tipi di dato ricorsivi





# type ide = string;;

  • # type ide = string;;

  • type ide = string

  • # type expr = | Den of ide | Val of ide | Fun of ide * expr

  • | Plus of expr * expr | Apply of expr * expr;;

  • type expr =

  • | Den of ide

  • | Val of ide

  • | Fun of ide * expr

  • | Plus of expr * expr

  • | Apply of expr * expr

  • E ::= I | val(I) | lambda(I, E1) | plus(E1, E2) | apply(E1, E2)

  • # Apply(Fun("x",Plus(Den "x", Den "x")), Val "y");;

  • - : expr = Apply (Fun ("x", Plus (Den "x", Den "x")), Val "y")



# type eval = Int of int | Bool of bool | Efun of expr

  • # type eval = Int of int | Bool of bool | Efun of expr

  • | Unbound;;

  • type eval = | Int of int | Bool of bool | Efun of expr | Unbound

  • # type env = ide -> eval;;

  • type env = ide -> eval

  • # let bind (rho, i, d) =

  • function x -> if x = i then d else rho x;;

  • val bind : (ide -> eval) * ide * eval -> (ide -> eval) =

  • env = IDE  eval

  • eval = [ int + bool + fun ]



# type com = Assign of ide * expr | Ifthenelse of expr *

  • # type com = Assign of ide * expr | Ifthenelse of expr *

  • com list * com list | While of expr * com list;;

  • type com =

  • | Assign of ide * expr

  • | Ifthenelse of expr * com list * com list

  • | While of expr * com list

  • C ::= ifthenelse(E, C1, C2) | while(E, C1) | assign(I, E) | cseq(C1, C2)

  • # While(Den "x", [Assign("y", Plus(Val "y", Val "x"))]);;

  • : com =

  • While (Den "x", [Assign ("y", Plus (Val "y", Val "x"))])





Un tipo primitivo utile: le liste

  • Si costruiscono enumerando esplicitamente gli elementi, racchiusi tra []

  • Oppure a partire dalla lista vuota [] tramite l’operatore di cons

  • Operazioni primitive standard



# let l1 = [1; 2; 1];;

  • # let l1 = [1; 2; 1];;

  • val l1 : int list = [1; 2; 1]

  • # let l2 = 3 :: l1;;

  • val l2 : int list = [3; 1; 2; 1]

  • # let l3 = l1 @ l2;;

  • val l3 : int list = [1; 2; 1; 3; 1; 2; 1]

  • # List.hd l3;;

  • - : int = 1

  • # List.tl l3;;

  • - : int list = [2; 1; 3; 1; 2; 1]

  • # List.length l3;;

  • - : int = 7



Caratteristiche Imperative

  • variabili e assegnamento

  • arrays (mutabili)

  • comandi iterativi, while, for



# let x = ref(3);;

  • # let x = ref(3);;

  • val x : int ref = {contents=3}

  • # !x;;

  • - : int = 3

  • # x := 25;;

  • - : unit = ()

  • # !x;;

  • - : int = 25

  • # x := !x + 2; !x;;

  • : int = 27

  • references sono mutable indirection cells, il cui valore puo’ essere modificato da un assegnamento



# let a = [| 1; 2; 3 |];;

  • # let a = [| 1; 2; 3 |];;

  • val a : int array = [|1; 2; 3|]

  • # let b = Array.make 12 1;;

  • val b : int array = [|1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1|]

  • # Array.length b;;

  • - : int = 12

  • # Array.get a 0;;

  • - : int = 1

  • # Array.get b 12;;

  • Uncaught exception: Invalid_argument("Array.get")

  • # Array.set b 3 131;;

  • - : unit = ()

  • # b;;

  • - : int array = [|1; 1; 1; 131; 1; 1; 1; 1; 1; 1; 1; 1|]



Il programma da eseguire deve essere memorizzato in un file .ml

  • Il programma da eseguire deve essere memorizzato in un file .ml

  • Compilare ed eseguire



Funziona per ordinare una lista polimorfa

  • Funziona per ordinare una lista polimorfa

  • Le liste sono un tipo di dato primitivo immutabile (in stile funzionale), a differenza degli array

  • La funzione sort ha tipo

  • 'a list -> 'a list

  • Gli operatori di confronto (=,<=,….) sono polimorfi, si applicano ad ogni tipo



Cosa vogliamo?

  • # let l1 = [6; 2; 5; 3];;

  • val l1 : int list = [6; 2; 5;3]

  • # sort l1 ;;

  • - : int list = [2; 3; 5;6]

  • # let l2 = [3.14; 2.17];;

  • val l1 : int list = [3.14; 2.17]

  • # sort l2 ;;

  • : float list = [2.17; 3.14]

  • La lista passata come input non e’ modificata, la funzione restituisce una nuova lista, che contiene gli elementi in ordine crescente



Insertion sort

  • Realizzare sort in modo ricorsivo

  • caso base: []

  • caso ricorsivo cons: head:: tail

  • Pattern matching

  • Insertion sort (funzione ausiliaria che inserisce un elemento in una lista ordinata)



Funzioni di ordine superiore

  • in puro stile funzionale le funzioni sono valori, possono essere passate come parametri ad altre funzioni

  • E’ utile per realizzare operazioni su strutture dati





Definire un tipo unione ‘a btree che specifica alberi binari polimorfi

  • Definire un tipo unione ‘a btree che specifica alberi binari polimorfi

  • Definizione ricorsiva:

  • caso base: vuoto

  • caso ricorsivo: un nodo che contiene un valore

  • di tipo ‘a, e due sottoalberi ‘a btree sx e dx





Funzioni

  • Scrivere una funzione che, dato un ‘a btree, calcola il numero di nodi

  • Ordered Binary Btree: ‘a btree polimorfi ma ordinati, il sottoalbero sx ha un valore strettamente minore, e quello dx un valore strettamente maggiore di quello del nodo

  • Scrivere due funzioni che, dato un ordered ‘a btree ed un valore x di tipo ‘a , fanno la ricerca o l’inserimento di x



Osservazione

  • Le funzioni member e insert come parametro un btree

  • Assumiamo che sia di tipo Ordered

  • Non possiamo definire un tipo di dato Ordered per costruzione

  • Che cosa serve? Un meccanismo per definire un tipo di dato astratto



Tipi di dato astratto

  • Dati + operazioni : insieme

  • In questo modo possiamo definire proprieta’ dei dati (tipo l’ordine per costruzione)

  • Meccanismi di astrazione, incapsulamento dell’informazione, in modo da garantire che le proprieta’ non siano violate dal codice che usa il tipo di dato





Condividi con i tuoi amici:


©astratto.info 2019
invia messaggio

    Pagina principale