Produit Cartésien I
Produit cartésien d'ensembles:
A × B = { (x,y) : x Î A, yÎ B }
Projections:
A × B ® A, A × B ® B
(A × B) × C ¹ A × (B × C) mais isomorphisme
Produit cartésien de deux types:
|
|
| Env |- e1 : t1 Env |- e2 : t2 |
|
|
|
|
#fst;;
- : 'a * 'b -> 'a = <fun>
#snd ;;
- : 'a * 'b -> 'b = <fun>
Produit cartésien de n types:
t_1 * t_2 * ..* t_n
Attention:
t1 * t2 * t3 ¹ (t1 * t2) * t3
¹ t1 * (t2 * t3)
Projections à définir par l'utilisateur