Bounded genericity with dependent types

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

(1)

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

(2)

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

(3)

R  $\longmapsto$  R[X] mathend000#,

(4)

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

(5)

R  $\longmapsto$  $\bf Fr$(R) mathend000#,

(6)

(R₁, R₂)  $\longmapsto$   R₁ x R₂ mathend000#.

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 mathend000# to be a ring. Hence we need BOUNDED GENERICITY.
• In rule (4) we need to say that $\cal {I}$ mathend000# is an ideal of R mathend000#. 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 mathend000# depends on a total ordering on S mathend000#. 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.