From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 8F5C6BC69 for ; Fri, 16 Nov 2007 09:23:02 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAALrhPEfAXQInh2dsb2JhbACPCgEBAQgKKYEP X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="19371375" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 16 Nov 2007 09:23:02 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id lAG8Mu3S020546 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 16 Nov 2007 09:23:02 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAG/iPEfBAkMt/2dsb2JhbACQVw X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="4316653" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 16 Nov 2007 09:22:59 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id F02C91E3C71; Fri, 16 Nov 2007 09:22:57 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id aC4B1wi239Gi; Fri, 16 Nov 2007 09:22:54 +0100 (CET) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 78E7A1E314C; Fri, 16 Nov 2007 09:22:54 +0100 (CET) Message-ID: <473D5380.2010508@fmf.uni-lj.si> Date: Fri, 16 Nov 2007 09:23:28 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 2.0.0.6 (X11/20071022) MIME-Version: 1.0 To: Christophe TROESTLER , Caml Subject: Re: [Caml-list] Compiler feature - useful or not? References: <20071114184352.GB28796@yquem.inria.fr> <473BE750.9060301@frisch.fr> <20071115132649.GB15754@yquem.inria.fr> <20071116.014620.919650100.Christophe.Troestler+ocaml@umh.ac.be> In-Reply-To: <20071116.014620.919650100.Christophe.Troestler+ocaml@umh.ac.be> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 473D5360.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 compiler:01 christophe:01 troestler:01 variants:01 subtraction:01 axioms:01 a-b:01 functor:01 functor:01 ocaml:01 ocaml:01 sig:01 val:01 Christophe TROESTLER wrote: > I believe Z is generally defined as a quotient of the disjoint union > (borrowed as variants in programming languages) of N and N > (identifying the two 0). Of course you can also define it as a > quotient of N×N by the smaller equivalent relation "~" s.t. (n,m) ~ > (n+1,m+1) and it is quite nice as addition is "inherited" from the one > on N×N but I am not sure it is the way it is usually done. As another mathematician, also prone to nitpicking, I beg to differ. It is more natural to define Z as a quotient of N x N, because this is just a special case of a general construction of a (commutative) ring out of a (commutative) rig. A rig is a structure with 0, + and * but no subtraction. A ring is a structure with 0, +, - and *. (Of course you need to imagine suitable axioms for 0, +, * such as commutativity, associativity and distributivity, but I am not writing them down here.) From every rig M we can construct a ring R as a quotient (M x M)/~ of M x M where we define (a,b) ~ (c,d) iff a+d = b+c Think of (a,b) as the "non-existent" difference a-b. This construction is natural in the technical sense that it is left adjoint to the forgetful functor(*) from rings to rigs. (In non-mathematician language: if we already have + and *, there is a _best_ way of getting - as well.) Caveat: (*) the use of "functor" here was as in mathematics, not as in ocaml. In what way is natural, or canonical, the construction of Z defined by sticking together two copies of N? To add some value to this post, other than mathematical willy waving, let me pose a puzzle. Implement the above in Ocaml, i.e., start with: module type RIG = sig type t val zero : t val add : t -> t -> t val mul : t -> t -> t end module type RING = sig include RIG val sub : t -> t -> t end 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? Andrej