Paradigme de programare -...

33
Paradigme de programare 2010-2011, semestrul 2 Curs 8

Transcript of Paradigme de programare -...

Page 1: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Paradigme de programare2010-2011, semestrul 2

Curs 8

Page 2: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Cuprins – Programare functionala

cu tipare statica

Sistem de tipuri

Inferenta de tip

Unificare de tip

Echivalenta/compatibilitate de tip

Siguranta de tip

Haskell

Page 3: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Sistem de tipuri

= set de mecanisme si reguli valabile intr-un

limbaj de programare, privind

◦ organizarea

◦ construirea

◦ manevrarea

tipurilor de date acceptate in limbaj

Page 4: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Atributiile unui sistem de tipuri

Definirea de noi tipuri

Asocierea de tipuri constructelor

existente in limbaj

Decizia asupra echivalentei tipurilor

Decizia asupra compatibilitatii tipurilor

Inferenta de tip

Page 5: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Avantajele unui sistem de tipuri

Detectare timpurie a erorilor (+ mai mare

acuratete in identificarea sursei)

Sustine abstractizarea

Declaratii de tip = forma de documentare (care

nu devine inconsistenta cu modificarile efectuate

ulterior)

Siguranta limbajului

Eficienta

Page 6: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Dezavantaj al tiparii statice

Sistemul de tipuri garanteaza absenta unor

comportamente nedorite, insa nu poate dovedi

prezenta lor

Se rejecteaza uneori cod care nu ar produce

probleme

In plus, tiparea statica necesita declaratii sau

inferenta de tip

Page 7: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Sisteme de tipuri si limbaje de

programare

Designul limbajului trebuie gandit in

paralel cu designul sistemului de tipuri

Limbajele cu tipare dinamica sau slaba tind

sa ofere facilitati care fac verificarea de tip

foarte dificila (sau imposibila)

Trebuie ales de la inceput intre adnotari

sau inferenta de tip

Page 8: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Inferenta de tip

Automata (tipurile nu trebuie declarate explicit)

Tipul unei expresii este sintetizat pe baza

◦ tipurilor componentelor expresiei

◦ contextului lexical al expresiei

Reprezentarea tipului = o expresie de

◦ constante de tip (= tipurile primitive: Int, Bool etc)

◦ variabile de tip

◦ constructori de tip (->, [ ] etc)

Sinteza de tip = combinarea constantelor,

variabilelor si constructorilor de tip dupa reguli

bine stabilite (= reguli de inferenta de tip)

Page 9: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Exemple de scheme de tip

la calculator

Page 10: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Relatia de tipare

t : T

Se citeste: expresia t are tipul T

Un termen t este bine tipat daca exista un

tip T a.i. t : T

Page 11: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Reguli de inferenta de tip

Sintaxa:

P1, P2, … Pn

___________ id_regula

C

Pi = premise

C = concluzie

Page 12: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Reguli de inferenta de tip

___________ t_true

true:Bool

___________ t_false

false:Bool

t1:Bool t2:T t3:T

____________________ t_if

if t1 then t2 else t3 : T

Page 13: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Reguli de inferenta de tip

___________ t_zero

0:Int

t : Int

___________ t_succ

succ t : Int

t : Int

______________ t_isZero

isZero t : Bool

Page 14: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Sintetizarea tipului expresiei

if isZero 0 then 0 else succ 0

___________ t_zero _____ t_zero

0:Int 0:Int

_______________ isZero _____ t_zero _______ t_succ

isZero 0 : Bool 0:Int succ 0:Int

___________________________________________________ t_if

if isZero 0 then 0 else succ 0 : Int

Page 15: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Observatii

Tipul unei expresii este unic

Relatiile de tipare se pot citi si invers:

◦ daca false : R, atunci R = Bool

◦ daca if t1 then t2 else t3 : R, atunci t1 :

Bool, t2 : R, t3 : R

Page 16: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Calcul Lambda tipat

Page 17: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Unificare de tip

Unificarea a 2 scheme de tip = gasirea

celei mai generale substitutii

S={a1/t1, a2/t2, … an/tn}

pentru variabilele de tip ti din cele 2

scheme de tip a.i., in urma substitutiei,

cele 2 scheme de tip devin una si aceeasi

Page 18: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Exemple de unificare

a

Int -> Bool

substitutia S={Int -> Bool/a}

Schema unificata devine Int->Bool, adica

functie de la un Int la un Bool

Page 19: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Exemple de unificare

a -> [b]

Int -> c

substitutia S={Int/a, [b]/c}

Schema unificata devine Int->[b], adica

functie de la un Int la o lista de un tip

generic b

Page 20: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Exemple de unificare

Int

Float

Nu unifica!

Page 21: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Exemple de unificare

a

a -> b

Nu unifica, unificarea ar da un tip infinit!

Page 22: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Exemple de unificare

Γ├ x:t1 Γ├ y:t2 Γ├ {t1,t2} unifica la Int sub o substitutie S

__________________________________________+Γ,S├ x+y:Int

Page 23: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Reguli generale de unificare

Orice variabila de tip unifica cu orice expresie de tip (se substituie variabila cu acea expresie) (in general se testeaza aparitiavariabilei in expresie, pentru a nu rezulta unificari infinite)

2 constante de tip unifica doar daca stau pentru acelasi tip

2 constructii de tip unifica doar daca sunt aplicatii ale aceluiasi constructor de tip asupra unor argumente care unifica recursiv

Page 24: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Echivalenta de tip

Structurala: cele 2 tipuri sunt construite la

fel (cu aceiasi constructori) din tipuri

echivalente (definitie recursiva pana se

ajunge la tipuri primitive)

Pe nume: cele 2 tipuri au un alias comun

Page 25: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Compatibilitate de tip

Decide daca o valoare poate fi procesata

corect intr-un anumit context

Page 26: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Siguranta de tip

“Termenii bine tipati nu o pot lua pe cai

gresite”

Siguranta = progres+conservare

Progres = un termen bine tipat nu se

blocheaza (ori este o valoare, ori poate

evolua conform unei reguli de evaluare)

Conservare = dupa un pas de evaluare

efectuat asupra unui termen bine tipat,

rezultatul este de asemenea bine tipat

Page 27: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Haskell

Limbaj pur functional

Tipare statica

Elementul de baza: functia unara

Functii curry (default) sau uncurry

Parantezele sunt folosite pentru controlul prioritatii

Legare pe lant static a variabilelor (inclusiv cele de top-level: regiunea lor = intreg modulul in care au fost definite)

Evaluare lenesa

Pattern match (permite definirea functiilor prin puncte)

Page 28: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Pattern match => f mare asemanare cu

specificatia formala

Exemplu: Formal, pt tipul List:

Constructori de baza:

[ ]

:

Axiome pt append:

append [] b = b

append (x:xs) b = x:(append xs b)

In Haskell: absolut identic!

Page 29: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Tipuri de date utilizator

Haskell da utilizatorului posibilitatea

definirii unui TDA cu implementare

completa direct din axiome

data IdTip = NCons1 | NCons2 … |

| Cons1 t1 | Cons2 t2 | … Consn tn

Ex: tipul Natural

Page 30: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Expresii de control al regiunii

variabilelor

let

where

Page 31: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Constructori de tip

data (cel mai puternic)

, : MTn->MT

◦ (t1,t2,…,tn) = produs cartezian

[ ] : MT->MT

◦ [ t ] = lista cu elemente de tip t

-> : MT->MT

◦ t1->t2 = functie de un element de tip t1 care

calculeaza valori de tip t2

Page 32: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

Liste = fluxuri (eventual infinite)

Exemple la calculator

Exemplu: seria aproximarilor numarului e

Exemplu: ciurul lui Eratostene

Page 33: Paradigme de programare - andrei.clubcisco.roandrei.clubcisco.ro/cursuri/f/f-sym/2pp/cb/curs8.pdf · Sistem de tipuri = set de mecanisme si reguli valabile intr-un limbaj de programare,

List comprehensions

Exemple la calculator