The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi, I would do the following. This is a bit cumbersome but this is the
price of putting definitions in a module type in the current state of
coq modules. If one could import things from a module type into a
module, we could factorize things. I think Elie Soubiran did his phd
on this subject, the idea was that there is no real difference between
a module type and a module in a dependently typed language.

I don't know if there are better solution.

Module Type Sig.
  Definition T : Type := nat.
  Parameter  f : T -> T.
  Definition g (t : T) : T := f (f t).
End Sig.

Module Impl <: Sig.
  Definition T : Type := nat.
  Definition f (t : T) : T := t * 2.
  Definition g (t : T) : T := f (f t).
End Impl.

You could make a functor building a sig from {T ; f } but you also end
up duplicating definitions between module and module type:

Module Type F.
  Definition T: Type := nat.
  Parameter  f : T -> T.
End F.

Module IMPLF<:F.
  Definition T: Type := nat.
  Definition f (t : T) : T := t * 2.
End IMPLF.

Module Type Sig(A:F).
  Import A.
  Definition g (t : T) : T := f (f t).
End Sig.


Module IMPLSig <: Sig(IMPLF).
  Import IMPLF.
  Definition g (t : T) : T := f (f t).
End IMPLSig.

Best regards,
Pierre

2014-02-11 22:26 GMT+01:00 Kirill Taran 
<kirill.t256 AT gmail.com>:
> Module Type Sig.
>   Definition T : Type := nat.
>   Parameter  f : T -> T.
>   Definition g (t : T) : T := f (f t).
> End Sig.
>
> Module Impl <: Sig.
>   Definition f (t : T) : T := t * 2.
> End Impl.