English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Compiler feature - useful or not?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-11-16 (08:58)
From: Jean-Christophe_Filliâtre <Jean-Christophe.Filliatre@l...>
Subject: Re: [Caml-list] Compiler feature - useful or not?
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

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...