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:  Andrej Bauer <Andrej.Bauer@f...> 
Subject:  Re: [Camllist] Compiler feature  useful or not? 
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 "nonexistent" difference ab. This construction is natural in the technical sense that it is left adjoint to the forgetful functor(*) from rings to rigs. (In nonmathematician 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