04/22/23 1

Haskell: Tipi algebriciHaskell: Tipi algebrici

Tipi algebrici: proprietà, sintassi, semanticaTipi algebrici: proprietà, sintassi, semantica Tipi algebrici: esempi e applicazioniTipi algebrici: esempi e applicazioni Esempi: Tipi algebrici polimorfiEsempi: Tipi algebrici polimorfi Equivalenza strutturale e refenziale: vantaggiEquivalenza strutturale e refenziale: vantaggi Morfismi tra tipi: Deriving e esplicitoMorfismi tra tipi: Deriving e esplicito Tipi ricorsivi e mutuamente ricorsiviTipi ricorsivi e mutuamente ricorsivi Tipo unione (disgiunta): Either e MaybeTipo unione (disgiunta): Either e Maybe Induzione strutturaleInduzione strutturale EserciziEsercizi

04/22/23 2

Proprietà: sintassi e semanticaProprietà: sintassi e semantica Due forme per introdurre tipiDue forme per introdurre tipi espliciti espliciti::

– SinonimiSinonimi » type People = (Name, Age)type People = (Name, Age)

type Name = Stringtype Name = Stringtype Age = Inttype Age = Int

– AlgebriciAlgebrici» data People = Person Name Agedata People = Person Name Age

data Name = LastFisrt Stringdata Name = LastFisrt Stringdata Age = Year Intdata Age = Year Int

Struttura SintatticaStruttura Sintattica

» data Name Name == Constr Constrn1,1n1,1 e eT1,1T1,1 … e … eTn1,1 Tn1,1 | … | Constr| … | Constrnk,knk,k e eTk,1Tk,1 … e … eTnk,k Tnk,k

SignificatoSignificato

» data N N == C Cn1,1n1,1 e eT1,1T1,1…e…eTn1,1 Tn1,1 | … | C| … | Cnk,knk,k e eTk,1Tk,1…e…eTnk,kTnk,k definisce iniezioni da domini definisce iniezioni da domini somme di prodottosomme di prodotto

Tnk,1

x … xTnk,k

TnTn1,11,1

TT1,11,1

xx … … xx

NN

CCn1,1n1,1

CCnk,knk,k

++

++

04/22/23 3

Struttura: Esempi e applicazioniStruttura: Esempi e applicazioni

Tipi enumeratiTipi enumerati»data Tepore Tepore = = Caldo | FreddoCaldo | Freddo

» data Stagioni Stagioni = = Autunno | Inverno | Primavera | EstateAutunno | Inverno | Primavera | Estate» unioneunione di tipi il cui dominio di valori contiene un solo valore di tipi il cui dominio di valori contiene un solo valore» ogni valore è un costruttoreogni valore è un costruttore

Tipi prodottoTipi prodotto» data Persona Persona = = Person PNome PEtaPerson PNome PEta» data PNome PNome = = Coppia Cognome NomeCoppia Cognome Nome» data PEta PEta = = Anni IntAnni Int

» prodottoprodotto di tipi di tipi» ogni valore è una iniezione di un prodotto di valoriogni valore è una iniezione di un prodotto di valori

Tipi unioneTipi unione»data IntErr IntErr = = Val Int | Err StringVal Int | Err String

04/22/23 4

Esempi: Tipi algebrici polimorfiEsempi: Tipi algebrici polimorfi

data SExpr = A Atom | Cons SExpr SExprdata SExpr = A Atom | Cons SExpr SExprderiving(Show, Eq)deriving(Show, Eq)

data Atom = LAMBDA | VAL Int | VAR Stringdata Atom = LAMBDA | VAL Int | VAR Stringderiving(Show, Eq)deriving(Show, Eq)

fun = Cons (A LAMBDA) (Cons (Cons (A(VAR "X")) (A(VAR "y"))) (A(VAR "y")))fun = Cons (A LAMBDA) (Cons (Cons (A(VAR "X")) (A(VAR "y"))) (A(VAR "y")))

data Tree a = Nil | Node a (Tree a) (Tree a)data Tree a = Nil | Node a (Tree a) (Tree a)deriving(Show,Eq,Ord)deriving(Show,Eq,Ord)

t1 = Node “uno” (Node “due” (Node “tre” Nil Nil) Nil) Nilt1 = Node “uno” (Node “due” (Node “tre” Nil Nil) Nil) Nilt2 = Node “uno” Nil (Node “due” (Node “tre” Nil Nil) Nil) t2 = Node “uno” Nil (Node “due” (Node “tre” Nil Nil) Nil) t1 > t2t1 > t2

Lisp: S-espessioni

Alberi polimorfi

04/22/23 5

Equivalenza strutturale e nominaleEquivalenza strutturale e nominale

Due forme per introdurre tipiDue forme per introdurre tipi espliciti espliciti::– SinonimiSinonimi

» type People = (Name, Age)type People = (Name, Age)type Name = Stringtype Name = Stringtype Age = Inttype Age = Int

– AlgebriciAlgebrici» data People = Person Name Agedata People = Person Name Age

data Age = Year Intdata Age = Year Int Due forme di equivalenza di tipoDue forme di equivalenza di tipo

– Sinonimo: Sinonimo: equivalenza strutturaleequivalenza strutturale» x:: People; y:: (String,Int) --- x e y hanno stesso tipox:: People; y:: (String,Int) --- x e y hanno stesso tipo

– Algebrico:Algebrico: equivalenza nominale (referenziale)equivalenza nominale (referenziale)» Ogni tipo algebrico è unicoOgni tipo algebrico è unico

Vantaggi:Vantaggi:SinonimiSinonimi» Defnizione compatta: Defnizione compatta: dovuta all’uso di strutture built-in quali le tupledovuta all’uso di strutture built-in quali le tuple» Riusabilità: Riusabilità: dovuta alla equivalenza strutturaledovuta alla equivalenza strutturaleAlgebrici:Algebrici:» Morfismi: Morfismi: possibilità di morfismi tra tipi (possibilità di morfismi tra tipi (deriving istanze di classe)deriving istanze di classe)» Tipi ricorsivi: Tipi ricorsivi: sono ilsono il meccanismo per introdurre tipi ricorsivimeccanismo per introdurre tipi ricorsivi» Uso di nomi: Uso di nomi: (significativi) per i selettori dei componenti -- esempio: CognomeNome String String(significativi) per i selettori dei componenti -- esempio: CognomeNome String String» Riduzione di errori: Riduzione di errori: dovuta all’equivalenza nominale che previene l’uso improprio di tipi diversidovuta all’equivalenza nominale che previene l’uso improprio di tipi diversi» Documentazione: Documentazione: dovuta ad un buon uso di nomi -- esempio: Year Intdovuta ad un buon uso di nomi -- esempio: Year Int

04/22/23 6

Morfismi tra tipi: derivingMorfismi tra tipi: deriving

Morfismi tra tipi basati sui costruttoriMorfismi tra tipi basati sui costruttoriop: A --> Bop: A --> Bdata Tdata TAA = C = CAA A Adata Tdata TBB = C = CBB B B(A-->B)->(Ta-->Tb)(A-->B)->(Ta-->Tb)(op u) = op (C(op u) = op (CAA v) = C v) = CBB(op v) (op v)

Quando op preserva i morfismiQuando op preserva i morfismi -- -- class AB a where op:: A-->Bclass AB a where op:: A-->B

In Haskell: il costrutto deriving (solo per built-in)In Haskell: il costrutto deriving (solo per built-in)

» data Stagioni Stagioni = = Autunno | Inverno | Primavera | EstateAutunno | Inverno | Primavera | EstateDeriving (Eq, Ord, Enum, Show)Deriving (Eq, Ord, Enum, Show)

Equivale a:Equivale a:instance Eq Stagioni where instance Eq Stagioni where Autunno == Autunno = TrueAutunno == Autunno = True …; …;instance Ord Stagioni where instance Ord Stagioni where Autunno > Inverno = TrueAutunno > Inverno = True … ; … ;instance …instance …

04/22/23 7

Morfismi tra tipi: esplicitoMorfismi tra tipi: esplicito

Scenario iniziale: due classi e due tipiScenario iniziale: due classi e due tipiclass Movable a where class Movable a where reflectX:: a -> a --- ed altre operazioni che omettiamoreflectX:: a -> a --- ed altre operazioni che omettiamodata AName = Pair A Stringdata AName = Pair A String

Come esprimere un morfismo Come esprimere un morfismo Movable AMovable A --> --> Movable Pair A StringMovable Pair A String – passo1: passo1: liftinglifting di funzioni A->A su (AName)->(AName) di funzioni A->A su (AName)->(AName)

mapName f (Pair a s) = Pair (f a) smapName f (Pair a s) = Pair (f a) sesempio: esempio: reflectX:: a --> areflectX:: a --> amapAName reflectX:: AName --> AName mapAName reflectX:: AName --> AName

– passo2(ultimo): passo2(ultimo): AName AName è un movable quando è un movable quando AA è movable è movableinstance Movable A => Movable AName where reflectX = mapAName reflectXinstance Movable A => Movable AName where reflectX = mapAName reflectX

esempio:esempio:instance Movable A where reflectX u = ….instance Movable A where reflectX u = ….ora possiamo esprimere e calcolare:ora possiamo esprimere e calcolare:

reflectX (P v s)reflectX (P v s)con v espressione di tipo A ed s espressione di tipo Stringcon v espressione di tipo A ed s espressione di tipo String

04/22/23 8

Morfismi tra tipi polimorfi: esplicitoMorfismi tra tipi polimorfi: esplicito

Scenario iniziale: due classi e due tipiScenario iniziale: due classi e due tipiclass Movable a where class Movable a where reflectX:: a -> a --- ed altre operazioni che omettiamoreflectX:: a -> a --- ed altre operazioni che omettiamodata Name a = Pair a Stringdata Name a = Pair a String

Come esprimere un morfismo Come esprimere un morfismo Movable aMovable a --> --> Movable Pair a StringMovable Pair a String – passo1: passo1: liftinglifting di funzioni a->a su (Name a)->(Name a) di funzioni a->a su (Name a)->(Name a)

mapName f (Pair a s) = Pair (f a) smapName f (Pair a s) = Pair (f a) sesempio: esempio: reflectX:: a --> areflectX:: a --> amapName reflectX:: (Name a) --> (Name a)mapName reflectX:: (Name a) --> (Name a)

– passo2(ultimo): passo2(ultimo): Name a Name a è un movable quando è un movable quando aa è movable è movableinstance Movable a => Movable (Name a) where reflectX = mapName reflectXinstance Movable a => Movable (Name a) where reflectX = mapName reflectX

esempio:esempio:instance Movable A where reflectX u = ….instance Movable A where reflectX u = ….ora possiamo esprimere e calcolare:ora possiamo esprimere e calcolare:

reflectX (P v s)reflectX (P v s)con v espressione di tipo A ed s espressione di tipo Stringcon v espressione di tipo A ed s espressione di tipo String

04/22/23 9

Esempi: Tipi algebrici polimorfiEsempi: Tipi algebrici polimorfi

data SExpr = A Atom | Cons SExpr SExprdata SExpr = A Atom | Cons SExpr SExprderiving(Show, Eq)deriving(Show, Eq)

data Atom = LAMBDA | VAL Int | VAR Stringdata Atom = LAMBDA | VAL Int | VAR Stringderiving(Show, Eq)deriving(Show, Eq)

fun = Cons (A LAMBDA) (Cons (Cons (A(VAR "X")) (A(VAR "y"))) (A(VAR "y")))fun = Cons (A LAMBDA) (Cons (Cons (A(VAR "X")) (A(VAR "y"))) (A(VAR "y")))

data Tree a = Nil | Node a (Tree a) (Tree a)data Tree a = Nil | Node a (Tree a) (Tree a)deriving(Show,Eq,Ord)deriving(Show,Eq,Ord)

t1 = Node “uno” (Node “due” (Node “tre” Nil Nil) Nil) Nilt1 = Node “uno” (Node “due” (Node “tre” Nil Nil) Nil) Nilt2 = Node “uno” Nil (Node “due” (Node “tre” Nil Nil) Nil) t2 = Node “uno” Nil (Node “due” (Node “tre” Nil Nil) Nil) t1 > t2t1 > t2

Lisp: S-espessioni

Alberi polimorfi

04/22/23 10

Tipi ricorsivi e mutuamente ricorsiviTipi ricorsivi e mutuamente ricorsivi

data IntList = data IntList = Val Int |Val Int | Cons Int IntListCons Int IntList

data Expr = data Expr = Lit Int |Lit Int | Expr :+: Expr |Expr :+: Expr | Expr :-: ExprExpr :-: Expr

data SForest = data SForest = P TLabel [Stree]P TLabel [Stree]data STree = data STree = Leaf NLabel |Leaf NLabel | Root SforestRoot Sforest data TLabel = data TLabel = T StringT String data NLabel = data NLabel = N LabelN Label

Anche polimorfe:Anche polimorfe:RISCRIVIAMOLERISCRIVIAMOLE

04/22/23 11

Tipo unione: Either e MaybeTipo unione: Either e Maybe

data Either a b = Left a | Right bdata Either a b = Left a | Right bderiving(Show, Ord, Eq)deriving(Show, Ord, Eq)

compareMese::Either Int String -> Either Int String -> BooleancompareMese::Either Int String -> Either Int String -> Boolean

data Maybe a = Nothing | Just adata Maybe a = Nothing | Just aderiving(Show,Eq,Ord)deriving(Show,Eq,Ord)

factorial nfactorial n|(n < 0) |(n < 0) = Nothing= Nothing|(n==0)|(n==0) = Just 1= Just 1|otherwise= let Just m = factorial (n-1)|otherwise= let Just m = factorial (n-1)

in Just (n* m)in Just (n* m)

Either

Maybe

04/22/23 12

Induzione strutturaleInduzione strutturaledata TyName a = C1 a | … | Ck adata TyName a = C1 a | … | Ck a

esempio: esempio: data Tree a = Nil | Node a (Tree a) (Tree a)data Tree a = Nil | Node a (Tree a) (Tree a)

v::TyName, P(v)v::TyName, P(v)

esempio: esempio: AA || v::Tree a, v::Tree a, C(v)C(v) dove, A: flipT Nil = Nildove, A: flipT Nil = Nil

flipT(Node u t1 t2) = Node u (flipT t2) (flipT t1)flipT(Node u t1 t2) = Node u (flipT t2) (flipT t1) C(v): flipT(flipT v) = vC(v): flipT(flipT v) = v

Un tipo algebrico (polimorfo su a)

Una proprietà su TyName

BaseBase: Nil --- (componenti non ricorsivi) : Nil --- (componenti non ricorsivi) v=Nil => flipT(flipT Nil) = flipT Nil = Nilv=Nil => flipT(flipT Nil) = flipT Nil = NilGeneraleGenerale: vero per t1,t2, --- (termini dei componenti ricorsivi): vero per t1,t2, --- (termini dei componenti ricorsivi)

i.e. i.e. AA || flipT(flipT t1))=t1 & flipT(flipT t2))=t2 --- (ind. Hyp.)flipT(flipT t1))=t1 & flipT(flipT t2))=t2 --- (ind. Hyp.) v = Node u t1 t2 => flipT(flipT(Node u t1 t2)) v = Node u t1 t2 => flipT(flipT(Node u t1 t2))

= flipT(Node u (flipT t2) (flipT t1)) --- (by 2)= flipT(Node u (flipT t2) (flipT t1)) --- (by 2) = Node u (flipT(flipT t1)) (flipT(flipT t2)) --- (by 2)= Node u (flipT(flipT t1)) (flipT(flipT t2)) --- (by 2) = Node u t1 t2 --- (by ind. Hyp.)= Node u t1 t2 --- (by ind. Hyp.)

Dimostrazione: Induzione sulla strutturaInduzione sulla struttura

(1)

(2)

04/22/23 13

Esercizi:Esercizi:

PolimorfiPolimorfi: : Si ridefinisca il tipo Expr in un polimorfo che generalizzi Int. Si ridefisnisca il tipo Sforest (ed tipi Si ridefinisca il tipo Expr in un polimorfo che generalizzi Int. Si ridefisnisca il tipo Sforest (ed tipi correlati) in un polimorfo che astragga rispetto ad una variabile correlati) in un polimorfo che astragga rispetto ad una variabile aa per il tipo delle etichette dei nodi interni e una per il tipo delle etichette dei nodi interni e una bb per i nodi foglia. Si definisca, quindi una funzione per i nodi foglia. Si definisca, quindi una funzione sizeIn sizeIn che calcoli il numero di nodiche calcoli il numero di nodiinterni di una SForest interni di una SForest

Show: Show: Per il polimorfo Sforest precedente si provveda a definire l’operazione show, ricorrendo:Per il polimorfo Sforest precedente si provveda a definire l’operazione show, ricorrendo:– 1) ora al morfismo implicito, 1) ora al morfismo implicito, – 2) ora a quello esplicito. In quest’ultimo caso, la stringa di presentazione deve essere una sequenza racchiusa tra parentesi 2) ora a quello esplicito. In quest’ultimo caso, la stringa di presentazione deve essere una sequenza racchiusa tra parentesi

tonde e contenente le presentazione degli alberi, a loro volte sequenze, senza separatori.tonde e contenente le presentazione degli alberi, a loro volte sequenze, senza separatori.

Tipi: Tipi: Si definisca un tipo di dato per memorie rappresentate come funzioni da Location -> Val, dove Val sia un Si definisca un tipo di dato per memorie rappresentate come funzioni da Location -> Val, dove Val sia un tipo adatto per esprimere 3 possibili differenti tipi di valore e Location sia un tipo per locazioni raprresenta- bili tipo adatto per esprimere 3 possibili differenti tipi di valore e Location sia un tipo per locazioni raprresenta- bili con arbitari interi. Si definisca l’operazione con arbitari interi. Si definisca l’operazione alloc alloc che data una Location e un tipo dei tre possibili allochi in che data una Location e un tipo dei tre possibili allochi in memoria tale locazioni con valore il valore di default previsto per tale tipo. memoria tale locazioni con valore il valore di default previsto per tale tipo.

Tipi: Tipi: Si definisca un tipo di dato per insiemi polimorfi e lo si equipaggi con le operazioni di unione, Si definisca un tipo di dato per insiemi polimorfi e lo si equipaggi con le operazioni di unione, appartenenza, e confronto, > e ==.appartenenza, e confronto, > e ==.

Tipi: Tipi: Si definisca un tipo di dato per relazioni binarie polimorfe rispetto ad un tipo Si definisca un tipo di dato per relazioni binarie polimorfe rispetto ad un tipo aa di classe Ord. Si fornisca di classe Ord. Si fornisca la definizione di un predicato la definizione di un predicato transitivetransitive che calcola true se e solo se la relazione è transitiva, e la definizione che calcola true se e solo se la relazione è transitiva, e la definizione della funzione della funzione minmin che, data una relazione e un valore u, calcola il minimo valore che è in relazione con u. che, data una relazione e un valore u, calcola il minimo valore che è in relazione con u.

04/22/23 14

Briciole:Briciole: Tipi ricorsivi e domini riflessiviTipi ricorsivi e domini riflessivi

data Rec a = R ((Rec a) -> (Rec a))data Rec a = R ((Rec a) -> (Rec a))

unfoldRec (R f) = funfoldRec (R f) = f

foldRec (R f) x = f xfoldRec (R f) x = f x

-- typing \x -> (x x)-- typing \x -> (x x)

funXX:: Rec a -> Rec afunXX:: Rec a -> Rec afunXX = \x -> foldRec x xfunXX = \x -> foldRec x x

-- typing Y=\f -> (\x -> f x x) (\x -> f x x), s.t. Y F = f(Y F)-- typing Y=\f -> (\x -> f x x) (\x -> f x x), s.t. Y F = f(Y F)