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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id ACB5FBC69 for ; Fri, 16 Nov 2007 01:46:26 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAKV2PEfUNQVbkmdsb2JhbACPBQIBAQcCBhMWgRE X-IronPort-AV: E=Sophos;i="4.21,422,1188770400"; d="scan'208";a="4309307" Received: from postbode01.versateladsl.be ([212.53.5.91]) by mail2-smtp-roc.national.inria.fr with ESMTP; 16 Nov 2007 01:46:26 +0100 Received: (qmail 5061 invoked by uid 0); 16 Nov 2007 00:46:19 -0000 Received: from unknown (HELO poincare.swapping.umh.ac.be) ([83.182.219.185]) (envelope-sender ) by smtp.versateladsl.be (qmail-ldap-1.03) with SMTP for < >; 16 Nov 2007 00:46:19 -0000 Received: from [127.0.0.1] (helo=localhost ident=trch) by poincare.swapping.umh.ac.be with esmtp (Exim 4.67) (envelope-from ) id 1IspLg-0003Co-7H; Fri, 16 Nov 2007 01:46:20 +0100 Date: Fri, 16 Nov 2007 01:46:20 +0100 (CET) Message-Id: <20071116.014620.919650100.Christophe.Troestler+ocaml@umh.ac.be> To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Compiler feature - useful or not? From: Christophe TROESTLER In-Reply-To: <20071115132649.GB15754@yquem.inria.fr> References: <20071114184352.GB28796@yquem.inria.fr> <473BE750.9060301@frisch.fr> <20071115132649.GB15754@yquem.inria.fr> X-Face: #2fb%mPx>rRL@4ff~TVgZ"<[:,oL"`TUEGK/[8/qb58~C>jR(x4A+v/n)7BgpEtIph_neoLKJBq0JBY9:}8v|j Organization: University of Mons-Hainaut X-Mailer: Mew version 5.2.51 on Emacs 22.1 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; compiler:01 christophe:01 troestler:01 christophe:01 troestler:01 ocaml:01 0100,:01 weis:01 variants:01 isomorphism:01 subset:01 forall:01 subset:01 subtyping:01 abbreviation:01 Hi, On Thu, 15 Nov 2007 14:26:49 +0100, Pierre Weis wrote: > > we define Z (the set of relative integer numbers) as a quotient of NxN), 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. > In the previous definition of quotient structures, there is a > careful distinction between the base set S and the quotient set > S/R. In fact, there always exists a canonical injection from S to S/R, Sorry for the nit-picking (I'm a mathematician, you know how we are :) ), but unless R is diagonal, the function S -> S/R is not injective (since we identify R-equivalent elements) but it is surjective. > We understand why the mathematicians always write after having designed a > quotient structure: ``thanks to this isomorphism, and if no confusion may > arise, we always assimilate S to its canonical injection in S/R''. By the above remark, S can be identified to a subset of S'/R for some S' but definitely not (of) S/R. > (...) > - the canonical projection from S/R to S is automatic. > (...) > More exactly, the canonical injection from S to S/R maps each element of S to > its equivalent class in S/R; if we assimilate each equivalence class to its > canonical representant (an element of S), the canonical injection maps each > element of S to the canonical representant of its equivalence class. Hence > the canonical injection has type S -> S. This is rather the projection (and generally not an injection) as, mathematically, p : S -> S is a projection means p(p x) = p x, forall x. Moreover, in the abstract, there is no canonical representative of an equivalent class -- that depends on the situation at hand. Given your example (deleted), I suppose what you mean is that the projection S -> S (representing S -> S/R) has to be written (since one has to actually choose a representative) while the injection S/R -> S comes for free or up to a coerecion (since we identified S/R to a subset of S). > What about private abbreviations ? (...) > If not implicit, the injection function should granted to be the > identity function (something that we would get for free, if we allow > projection via sub-typing coercion). I second the use of a subtyping coercion for that (after all, it would be really annoying to have to use a private type abbreviation from a module "forgetting" to provide a way out :) ). > The moca compiler (see http://moca.inria.fr/) helps you to write the > canonical injection by generating one for you, provided you can express the > injection at hand via a set of predefined algebraic relations (and/or rewrite May you tell a bit more ? That looks quite interesting ! Since there is nothing canonical about the injection S/R -> S, what does moca do if several representatives are possible (e.g. pick one by preferring left associativity to the right one?). (I saw there is some paper on the page but I have no time to dig through it right now.) Best regards, ChriS