Re: [Caml-list] Compiler feature - useful or not?

["Jean-Christophe Filliâtre" <Jean-Christophe.Filliatre@lri.fr>]

Andrej Bauer a écrit :
> The puzzle is this: write down the module type for the construction
> taking a rig and returning the free ring over it. It is _not_ just
> 
> module type ConstructRing = functor (M : RIG) -> RING
> 
> because that would allow _any_ ring whatsoever as the result. It has to
> be the ring that comes from M via above construction, so there has to be
> extra stuff, such as an embedding of M into the resulting R. But what else?

Despite the embedding you're mentioning, which could be added as follows

  module type ConstructRing =
    functor (M : RIG) -> sig include RING val embed : M.t -> t end

I don't see what else you could add to the signature (unless you want to
expose that the type t of the RING is a pair of type M.t * M.t; and even
with that you couldn't expose the definitions of the operations in the
signature).

All the properties you're expecting for the resulting ring are part of
(logical) specifications, which cannot be expressed via ocaml types.
You could do that in a richer type system (e.g. Coq).

But may be I misunderstood your question...

--
Jean-Christophe