The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello, notice that "Include A" allows to include all definitions of
module (type) A in the current module (type).

This not subtyping but often helps to develop modules layer by layer.

see: http://coq.inria.fr/coq/refman/Reference-Manual004.html#@command52

Hope this helps,
Pierre

2013/1/24  
<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?