The Coq mailing list

[<bhandalc AT tcd.ie>]

Hi,

I notice that Coq does not allow Module Sub-Typing, which would facilitate
some really nice inheritance i.e.

Module Type A

...

Module Type B : A

Right now, all that can be done is:

Module Type A

...

Module B : A

If I am incorrect please stop me here? If not, read on.

The above allows B to inherit all the results of A as long as B redefines the
Parameters of A. Redefining the parameters is much like function override in
OO programming and inheritance. Except in Coq it's enforced. It would be nice
if the parameters didn't HAVE to be redefined. But the real problem is that
after one step, you can't go any further i.e. it is impossible to then write:

Module C : B

Because B is not a Module Type, it is just an instance of A. What we would
like is to define another Module TYPE B which is a subtype of A, just as in OO
programming one can define subclasses of a superclass.

To summarise, I have two suggestions:

1. Allow Module Sub-Typing i.e. inheritance.
2. Remove the enforcement of redefining all Parameters, and if they are not
redefined, just carry them over as they are. (This is less crucial).

Thoughts anyone?