The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

On Wed, 19 May 2004, Adam Koprowski wrote:

> (1) Below is a structure of my modules simplified and without a content. My
> problem is to make Coq unify between modules H.T and Comp.T (which are
> clearly the same) in module HorpoWF. Basically I won't to get rid of an
> error message that appears when trying to enter definition for HorpoWF.x.
> Note that in case Term is just a definition (not an inductive one)
> everything works fine.

i suspect that it is related to a problem that sebastien hinderer and myself
had in a formalization of rewriting and polynomial interpretations in coq, a
contribution that we should release by the end of june, or in july.

when you define such a functor:

>  > Module Terms (S: Signature).
>  >   Inductive Term: Set :=
>  >   | blah: Term.
>  > End Terms.

with an inductive type definition, two instances of it with the same signature
will be considered as distinct. until it changes in coq, the solution is to
use a module -- type -- TERMS identical to Terms wherever you need to use
terms. then, at the end, you can fill in your functors with Terms.

> (2) Let's say we have a hierarchy of modules one being refinement of 
> another.
> For instance modules describing order with more and more assumptions about 
> it.
> Below I'll restrict to two modules but in principle there can be much more.
>    I can see two methods (at least) of such definition.
>
>  > Module Type Relation.
>  >   Parameter A: Set.
>  >   Parameter R: A -> A -> Prop.
>  > End Relation.
>  >
>  > Module Type Order.
>  >   Parameter A: Set.
>  >   Declare Module R: Relation with Definition A := A.
>  >   Parameter R_irr: forall (a: A), ~R.R a a.
>  > End Order.
>
>    or
>
>  > Module Type Order'.
>  >   Declare Module R: Relation.
>  >   Parameter R_irr: forall (a: R.A), ~R.R a a.
>  > End Order'.
>
>    Both approaches have disadvantages. It is possible to avoid them?

i also remarked this problem and asked Jacek Chrzaszcz whether it would be
possible to have syntatic sugar to extend modules or module types like the
inheritance mechanism in object-oriented languages.

Module Type Order inherits/extends Relation.
  Parameter R_irr: forall (a: A), ~R.R a a.
End Order.

perhaps we could go further in this direction: when we want to implement a
module type containing some definitions, it is not useful to write
them again! in oo languages, only abstract methods need to be defined.

Module Terms implements TERMS.
  (* here, we only define/prove the things not already defined/proved
        in TERMS *)
End Terms.