Bounded genericity with dependent types

Recall that the RINGS $R$ in Computer Algebra are obtained by applying rules like

(1)

$R = {\mbox{${\mathbb{Z}}$}}$ ,

(2)

$n \ \longmapsto \ {\mbox{${\mathbb{Z}}$}}/n{\mbox{${\mathbb{Z}}$}}$ ,

(3)

$R \ \longmapsto \ {R}[X]$ ,

(4)

$(R, {\cal I}) \ \longmapsto \ R/{\cal I}$

(5)

$R \ \longmapsto \ {\bf Fr}({R})$ ,

(6)

$(R_1, R_2) \ \longmapsto \ \ R_1 \times R_2$ .

To implement the above rules we would like to do the following constructions in our programming language.

• 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 ${\cal I}$ 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.