coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Colm Bhandal <bhandalc AT tcd.ie>
- To: Pierre Courtieu <pierre.courtieu AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Module Inheritance in Coq?
- Date: Thu, 24 Jan 2013 12:12:48 +0000
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?
- [Coq-Club] Module Inheritance in Coq?, bhandalc, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Pierre Courtieu, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Colm Bhandal, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Pierre Courtieu, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Colm Bhandal, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Pierre Courtieu, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Colm Bhandal, 01/24/2013
- Re: [Coq-Club] Module Inheritance in Coq?, Pierre Courtieu, 01/24/2013
Archive powered by MHonArc 2.6.18.