The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Ok, I have read it. So it was real that you have to manually redeclare
the instantiation for your set/ map /... so on
in OCaml if they are inside modules abstracting over the element kind.
That makes me wondering why
camel support polymorphic function in the first place, if modules arent. :-P
(ok ok, just forgot, I do not want to place a flame bomb here, even
more since I'm convinced that a (succint) manual redeclaration is a
good thing)
Anyway it does not help me if i want to use sets in OCamel, instead It
looks like a design guide on how to re implement myself sets :)
The same, for the little I have understanded,
http://coq.inria.fr/stdlib/Coq.FSets.FMapInterface.html looks like a
good start if someone want to reimplement maps.
I absolutely understand the parallel with camel, that is,

-In camel having an interface ( aka module type) and a (possible set
of) implementation allows to change the implementation saving the
code,
providing an amazing useful hook for optimization, debugging (mocks
for example), code reuse, and so on so forth.
The same advantages also provided from java interfaces.

-In coq using an interface and an implementation allows to make proofs
that relay only on the interface specification,
and providing an implementation it is only needed to make the theorem
assistant accepting that such implementation there exists, similarly
somehow to showing that a theorem holds showing an instance (for what
I understand of the underlying bases).
This also means that to understand the meaning of a statement that is
using such interface i do not need to know nothing about the
implementation.
Anyway it also means that i have no hope to see my map pretty printed
as [1->"hello";2->"hello"] when I will use concrete
maps for testing


Now, can I know what to do to instantiate my map and set? Moreover,
since setoid is required, Does setoid use extra axioms or not? Is
there a standard way to know if a library I'm using does use extra
axioms?

Marco.