Tip ca mulțime de valori
	finită
	infinită
	enumerabilă (care este următoarea valoare)
	
	
	
Lumea datelor					Lumea tipurilor
================================================

Expersii de date				Expresii de tip


Constructori de date			Constructori de tip
	încep cu literă mare			încep cu literă mare

Asociativitate stânga			Asociativitate dreapta

Variabile de date				Variabile de tip
									încep cu literă mică



f 	::		 a -> b -> b

expr			expr
de date			de tip




TDA
	Constructori de bază
	Operatori
	Axiome
	
	
(->) Natural ((->) Natural Natural) -- expresie de tip, construiește un tip, tipul funcției add

([] Natural) -- construiește tipul listă de Natural

Natural -> Natural -> Natural





data expr-1 = constr-1 | constr-2 | constr-3

expr-1
	expresie de tip
	începe cu constructorul de tip pentru tipul nou (numele tipului)
	poate avea argumente (variabile de tip)
constr-i = numele-constructorului-de-date tipuri parametri (expresii de tip)

type constr-de-tip = expresie de tip





f g = (g 3) + 1

f = \g -> (g 3) + 1   (E)
          -----
		    F
		  ----------
		      G

E: TLambda
g :: a				OK
(g 3) + 1 :: b		OK
f :: a -> b			OK

F: TApp
g :: c -> d			OK
3 :: c				OK
(g 3) :: d			OK

G: T+
(g 3) :: Int		OK
1 :: Int			OK
(g 3) + 1 :: Int	OK

TInt
3 :: Int			OK
1 :: Int			OK

a = c -> d
c = Int
d = Int
b = Int

f :: (Int -> Int) -> Int






fix f = f (fix f)

fix = \f -> (f (fix f))    (E)
			   -------
				 G
			-----------
				H
				
E: TLambda
f :: a				OK
(f (fix f)) :: b
fix :: a -> b		OK

G: TApp
fix :: c -> d		OK
f :: c				OK
(fix f) :: d

H: TApp
f :: e -> g			OK
(fix f) :: e
(f (fix f)) :: g

a = c = e -> g			(f)
a -> b = c -> d			(fix)
a = c
b = d
b = e					(fix f)
b = g					(f (fix f))

E: TLambda
f :: b -> b			OK
(f (fix f)) :: b	OK
fix :: a -> b		OK

G: TApp
fix :: a -> b		OK
f :: a				OK
(fix f) :: b		OK

H: TApp
f :: b -> b			OK
(fix f) :: b		OK
(f (fix f)) :: b	OK


fix :: (b -> b) -> b




f x = (x x)

f = \x -> (x x)    (E)
		  -----
		    G
E: TLambda
x :: a
(x x) :: b
f :: a -> b

G: TApp
x :: c -> d
x :: c
(x x) :: d

a = c = c -> d