**(1)**- ,
**(2)**- ,
**(3)**- ,
**(4)****(5)**- ,
**(6)**- .

- 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 to be a ring. Hence we need BOUNDED GENERICITY. - In rule
**(4)**we need to say that is an ideal of . 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 depends on a total ordering on . 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.

*
*

2008-01-07