Compiler feature  useful or not?
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Christophe TROESTLER <Christophe.Troestler+ocaml@u...> 
Subject:  Re: [Camllist] Compiler feature  useful or not? 
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 nitpicking (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 Requivalent 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 subtyping 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