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 (09:48)
From: Christophe TROESTLER <Christophe.Troestler+ocaml@u...>
Subject: Re: [Caml-list] Compiler feature - useful or not?
On Fri, 16 Nov 2007 09:23:28 +0100, Andrej Bauer wrote:
> This construction is natural in the technical sense that it is left
> adjoint to the forgetful functor(*) from rings to rigs.


> In what way is natural, or canonical, the construction of Z defined
> by sticking together two copies of N?

I do not think there is something natural about this construction in
the way you outlined it above.  It's just ad hoc for this case.

> The universal property of the resulting ring R is this: for any ring
> T, if f : M -> T is a function preserving 0, + and * then there is a
> unique function g : R -> T preserving 0, +, * and - such that g
> (include x) = f x, where include is as above. This needs to be
> accounted for, and it's not just a logical specification.

Would this fit your bill?

module type To_Ring = functor (M: RIG) -> sig
  include RING
  val embed : M.t -> t 
  module F : functor (T:RING) -> sig
    val lift : (M.t -> T.t) -> (t -> T.t)