**(1)**-
*R*= , **(2)**-
*n*/*n*, **(3)**-
*R**R*[*X*], **(4)**-
(
*R*,)*R*/ **(5)**-
*R*(*R*), **(6)**-
(
*R*_{1},*R*_{2})*R*_{1}×*R*_{2}.

- To define functions which return a type (as in rule
**(2)**). - To define functions that can be parametrized by a type (as in rule
**(3)**). Hence we need__GENERICITY__. - To handle
__INTERFACE__(or type of types). Indeed in**(3)**we need*R*to be a ring. Hence we need__BOUNDED____GENERICITY__. - In rule
**(4)**we need to say that is an ideal of*R*. Hence we need__BOUNDED____GENERICITY____WITH____DEPENDENT____TYPES__. - We should be able to have functions as parameters of other functions.
For instance an ordered abelian free monoid genetated by
a set
*S*depends on a total ordering on*S*. Hence functions must have types too. Finally, both functions and types must have types and must be possible parameters for functions. Hence functions and types must be__TREATED____AS____VALUES__.

2003-06-06