The Coq mailing list

[Colm Bhandal <bhandalc AT tcd.ie>]

Hi Pierre,

This is useful, but they key feature is lacks, and the one I am most interested in, is the ability to override Parameters with new definitions. I probably should have made that more clear. Consider the following.

Module Type A.

Parameter X : Type.

End A.

Module B.

Include A.

Inductive Y : Type :=.

Definition X := Y. ********************FAILS HERE. ERROR: X ALREADY EXISTS.

End B.

This fails because X is rigid. It cannot be overridden.

I also noticed another little problem while doing this example: You can't override a Type Parameter with an Inductive Type. Though it looks like the Coq people are working on this? The following minimal example demonstrates what I'm talking about:

Module Type A.

Parameter X : Type.

End A.

Module B : A.

Inductive X : Type :=.

End B. ********************FAILS HERE. ERROR: The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name.

The problem with the proposed fix "you can rename the inductive type and give a definition to map the old name to the new name." is that the definitional equality inside a Module is for some reason not recognised outside it, and thus cbv reduction fails outside the Module. So it would be nice to get this sorted too:

1. Allow instantiation of a parameter by an inductive type.
2. Recognise definitional equality outside the Module where the definition occurred. Perhaps there is a workaround for this that I am not aware of, but it would be nice if it could be seamlessly built into the "simpl" tactic.

All the best,

Colm

On 24 January 2013 11:58, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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?