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₁, R₂)  $\longmapsto$   R₁×R₂.

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.