A sample revised prelude for numeric classes

[William Lee Irwin III]

On Sun, Feb 11, 2001 at 09:17:53PM -0800, William Lee Irwin III wrote:
>> mod an ideal generated by a polynomial, e.g. 1/(1-x) mod (1+x^2).

On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
> Sorry, isn't (1+x^2) invertible in Z[[x]]?

You've caught me asleep at the wheel again. Try 1/(1-x) mod 2+x^2. Then
	x^(2n)   -> (-2)^n
	x^(2n+1) -> (-2)^n x
so our process isn't finite again, and as 2 is not a unit in Z,
2+x^2 is not a unit in Z[[x]].

On Sun, Feb 11, 2001 at 09:17:53PM -0800, William Lee Irwin III wrote:
>> I think it's nice to have the Cauchy principal value versions of things
>> floating around.  I know at least that I've had call for using the CPV
>> of exponentiation (and it's not hard to contrive an implementation),
>> but I'm almost definitely an atypical user. (Note, (**) does this today.)

On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
> Does Cauchy Principal Value have a specific definition I should know?
> The Haskell report refers to the APL language report; do you mean that
> definition?

The Cauchy principal value of an integral seems fairly common in complex
analysis, and so what I mean by the CPV of exponentiation is using the
principal value of the logarithm in the definition w^z = exp (z * log w).

Essentially, given an integral from one point to another in the complex
plane (where the points can be e^(i*\gamma)*\infty) the Cauchy principal
value specifies precisely which contour to use, for if the function has
a singularity, connecting the endpoints by a countour that loops about
those singularities a number of times will affect the value of the
integral. This is fairly standard complex analysis, are you sure you
can't dig it up somewhere? It basically says to connect the endpoints
of integration by a straight line unless singularities occur along that
line, and in that case, to shrink a semicircle about the singularities,
and the limit is the Cauchy principal value. More precise definitions
are lengthier.

On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
> I'm still agnostic on the Poset issue, but as an aside, let me mention
> that "Maybe Bool" works very well as a trinary logical type.  "liftM2
> &&" does the correct trinary and, for instance.

I can only argue against this on aesthetic grounds. (<=) and cousins
are not usually typed so as to return Maybe Bool.

On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
> It may be logically prior, but computationally it's not...  Note that
> the axioms for lattices can be stated either in terms of the partial
> ordering, or in terms of meet and join.

I was under the impression the distinction between lattices and partial
orders was the existence of the meet and join operations.

Actually, I think my argument centers about the use of the antisymmetry
of the relation (<=) being used to define computational equality in
some instances. Can I think of any good examples? Well, a contrived one
would be that on types, if there is a substitution S such that S t = t'
(structurally), where we might say that t' <= t, and also a
substitution S' so such that S' t' = t (again, structurally) where we
might say that t <= t', so we have then t == t' (semantically). Yes,
I realize this is not a great way to go about this.

Another (perhaps contrived) example would be ordering expression trees
by the flat CPO bottom <= _ on constants of a signature, and the
natural business where if the trees differ in structure, they're
incomparable, except where bottom would be compared with something
non-bottom, in which case (<=) holds. In this case, we might want
equality to be that two expression trees t, t' are equal iff there are
sequences of reductions r, r' such that r t = r' t' (again, structurally).

You might argue that the notion of structural equality underlying these
is some sort of grounds for the dependency, and I think that hits on
the gray area where design decisions come in. What I'm hoping the
examples demonstrate is the mathematical equality and ordering (in some
metalanguage) underlie both of the computational notions, and that the
computational notions may very reverse or break the dependency

	class Eq t => Ord t where ...

especially when the structure of the data does not reflect the
equivalence relation we'd like (==) to denote.

Cheers,
Bill