The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi everyone,

Is it possible for the definitions in a module to not be in scope, but
for its computational behavior to still be evaluated?  If a module is
pulled in with "Require" (but not "Import"), then its computational
behavior is evaluated, but its definitions are still there and can be
accessed with "Module.definition", they just haven't been aliased into
the unqualified namespace.  On the other hand, if a module implements
an abstract module type, then its definitions are only visible insofar
as they have the types specified by the module type, but its
computational behavior is also hidden.  (These are my understandings,
but please correct if I am wrong, or if I am using the wrong words.)

This question came up here:
http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant
where the ability to do something of this sort in Agda is convenient,
but we were unable to replicate it in Coq.  A suggestion was made that
this is an intentional part of the design of Coq, so that "the types
of a client of an abstract module don’t depend on the implementation
of that module".  Is that correct?  Is there a way to replicate this
trick in Coq, or are there good reasons that something of this sort
should never be allowed?

Thanks!
Mike