A sample revised prelude for numeric classes

I've started writing up a more concrete proposal for what I'd like the Prelude to look like in terms of numeric classes. Please find it attached below. It's still a draft and rather incomplete, but please let me know any comments, questions, or suggestions. Best, Dylan Thurston

Sun, 11 Feb 2001 17:42:15 -0500, Dylan Thurston
I've started writing up a more concrete proposal for what I'd like the Prelude to look like in terms of numeric classes. Please find it attached below. It's still a draft and rather incomplete, but please let me know any comments, questions, or suggestions.
I must say I like it. It has a good balance between generality and usefulness / convenience. Modulo a few details, see below.
class (Num a, Additive b) => Powerful a b where (^) :: a -> b -> a instance (Num a) => Powerful a (Positive Integer) where a ^ 0 = one a ^ n = reduceRepeated (*) a n instance (Fractional a) => Powerful a Integer where a ^ n | n < 0 = recip (a ^ (negate n)) a ^ n = a ^ (positive n)
I don't like the fact that there is no Powerful Integer Integer. Since the definition on negative exponents really depends on the first type but can be polymorphic wrt. any Integral exponent, I would make other instances instead: instance RealIntegral b => Powerful Int b instance RealIntegral b => Powerful Integer b instance (Num a, RealIntegral b) => Powerful (Ratio a) b instance Powerful Float Int instance Powerful Float Integer instance Powerful Float Float instance Powerful Double Int instance Powerful Double Integer instance Powerful Double Double This requires more instances for other types, but I don't see how to make it better with (^), (^^) and (**) unified. It's a bit irregular: Int can be raised to custom integral types without extra instances, but Double not. It's simpler to unify only (^) and (^^), leaving (**) :: Floating a => a -> a -> a with the default definition of \a b -> exp (b * log a). I guess that we always know which one we mean, although in math the notation is the same. Then the second argument of (^) is always arbitrary RealIntegral, so we can have a single-parameter class with a default definition: class (Num a) => Powerful a where (^) :: RealIntegral b => a -> b -> a a ^ 0 = one a ^ n = reduceRepeated (*) a n instance Powerful Int instance Powerful Integer instance (Num a) => Powerful (Ratio a) where -- Here unfortunately we must write the definition explicitly, -- including the positive exponent case: we don't have access to -- whatever the default definition would give if it was not -- replaced here. We should probably provide the default definition -- for such cases as a global function: -- fracPower :: (Fractional a, RealIntegral b) => a -> b -> a -- (under a better name). instance Powerful Float -- Ditto here. instance Powerful Double -- And here.
class (Real a, Floating a) => RealFrac a where -- lifted directly from Haskell 98 Prelude properFraction :: (Integral b) => a -> (b,a) truncate, round :: (Integral b) => a -> b ceiling, floor :: (Integral b) => a -> b
Should be RealIntegral instead of Integral. Perhaps RealIntegral should be called Integral, and your Integral should be called somewhat differently.
class (Real a, Integral a) => RealIntegral a where quot, rem :: a -> a -> a quotRem :: a -> a -> (a,a)
-- Minimal definition: toInteger
You forgot toInteger.
class (Lattice a, Num a) => NumLattice a where abs :: a -> a -> a abs x = meet x (negate x)
Should be: abs :: a -> a -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

On Sun, Feb 11, 2001 at 05:42:15PM -0500, Dylan Thurston wrote:
I've started writing up a more concrete proposal for what I'd like the Prelude to look like in terms of numeric classes. Please find it attached below. It's still a draft and rather incomplete, but please let me know any comments, questions, or suggestions.
This is great, it gets something concrete out there to comment on, which is probably quite a bit of what needs to happen. For brevity's sake, I'll have to chop up your message a bit.
(1) The current Prelude defines no semantics for the fundamental operations. For instance, presumably addition should be associative (or come as close as feasible), but this is not mentioned anywhere.
This is something serious, as I sort of took for granted the various properties of operations etc. I'm glad you pointed it out.
(2) There are some superfluous superclasses. For instance, Eq and Show are superclasses of Num. Consider the data type
data IntegerFunction a = IF (a -> Integer)
One can reasonably define all the methods of Num for IntegerFunction a (satisfying good semantics), but it is impossible to define non-bottom instances of Eq and Show.
In general, superclass relationship should indicate some semantic connection between the two classes.
It's possible to define non-bottom instances, for instance: instance Eq (a->b) where _ == _ = False instance Show (a->b) where show = const "<<function>>" I suspect you're aware of this and had in mind the constraint that they should also respect the invariants and laws of the classes.
class (Additive a) => Num a where (*) :: a -> a -> a one :: a fromInteger :: Integer -> a
Num encapsulates the mathematical structure of a (not necessarily commutative) ring, with the laws
a * (b * c) === (a * b) * c one * a === a a * one === a a * (b + c) === a * b + a * c
Typical examples include integers, matrices, and quaternions.
There is an additional property of zero being neglected here, namely that it is an annihilator. That is, zero * x === zero x * zero === zero Again, it's probably a reasonable compromise not to accommodate nonassociative algebras, though an important application of them lies within graphics, namely 3-vectors with the cross product.
"reduceRepeat op a n" is an auxiliary function that, for an associative operation "op", computes the same value as
reduceRepeat op a n = foldr1 op (repeat n a)
but applies "op" O(log n) times. A sample implementation is below.
This is a terrific idea, and I'm glad someone has at last proposed using it.
class (Num a) => Integral a where div, mod :: a -> a -> a divMod :: a -> a -> (a,a) gcd, lcm :: a -> a -> a extendedGCD :: a -> a -> (a,a,a)
While I'm wholeheartedly in favor of the Euclidean algorithm idea, I suspect that more structure (i.e. separating it out to another class) could be useful, for instance, formal power series' over Z are integral domains, but are not a Euclidean domain because their residue classes aren't computable by a finite process. Various esoteric rings like Z[sqrt(k)] for various positive and negative integer k can also make this dependence explode, though they're probably too rare to matter.
TODO: quot, rem partially defined. Explain. The default definition of extendedGCD above should not be taken as canonical (unlike most default definitions); for some Integral instances, the algorithm could diverge, might not satisfy the laws above, etc. TODO: (/) is only partially defined. How to specify? Add a member isInvertible :: a -> Bool? Typical examples include rationals, the real numbers, and rational functions (ratios of polynomials).
It's too easy to make it a partial function to really consider this, but if you wanted to go over the top (and you don't) you want the multiplicative group of units to be the type of the argument (and hence result) of recip.
class (Num a, Additive b) => Powerful a b where ... I don't know interesting examples of this structure besides the instances above defined above and the Floating class below. "Positive" is a type constructor that asserts that its argument is >= 0; "positive" makes this assertion. I am not sure how this will interact with defaulting arguments so that one can write
x ^ 5
without constraining x to be of Fractional type.
What you're really trying to capture here is the (right?) Z-module-like structure of the multiplicative monoid in a commutative ring. There are some weird things going on here I'm not sure about, namely: (1) in an arbitary commutative ring (or multiplicative semigroup), the function can (at best) be defined as (^) :: ring -> NaturalNumbers -> ring That is, only the natural numbers can act on ring to produce an exponentiation-like operation. (2) if you have at least a division ring (or multiplicative group), you can extend it to (^) :: ring -> Integer -> ring so that all of Z acts on ring to produce an exponentiation operation. (3) Under some condition I don't seem to be able to formulate offhand, one can do (^) :: ring -> ring -> ring Now the ring (or perhaps more generally some related ring) acts on ring to produce an expontiation operation like what is typically thought of for real numbers. Anyone with good ideas as to what the appropriate conditions are here, please speak up. (Be careful, w ^ z = exp (z * log w) behaves badly for w < 0 on the reals.)
-- Note: I think "Analytic" would be a better name than "Floating". class (Fractional a, Powerful a a) => Floating a where ... The semantics of these operations are rather ill-defined because of branch cuts, etc.
A useful semantics can be recovered by assuming that the library-defined functions are all the Cauchy principal values. Even now: Complex> (0 :+ 1)**(0 :+ 1) 0.20788 :+ 0.0
class (Num a, Ord a) => Real a where abs :: x -> x signum :: x -> x
I'm not convinced that Real is a great name for this, or that this is really the right type for all this stuff. I'd still like to see abs and signum generalized to vector spaces.
module Lattice where class Lattice a where meet, join :: a -> a -> a
Mathematically, a lattice (more properly, a semilattice) is a space with operations "meet" and "join" which are idempotent, commutative, associative, and (usually) distribute over each other. Examples include real-valued function with (pointwise) max and min and sets with union and intersection. It would be reasonable to make Ord a subclass of this, but it would probably complicate the class heirarchy too much for the gain. The advantage of Lattice over Ord is that it is better defined. Thus we can define a class
class (Lattice a, Num a) => NumLattice a where abs :: a -> a -> a abs x = meet x (negate x)
and real-valued functions and computable reals can both be declared as instances of this class.
I'd be careful here, a meet (join) semilattices are partial orders in which finite meets (joins) exist, and they only distribute over each other in distributive lattices. Boolean lattices also have complementation (e.g. not on type Bool) and Heyting lattices have implications (x <= y ==> z iff x `meet` y <= z). My suggestion (for simplicity) is: class Ord a => MeetSemiLattice a where meet :: a -> a -> a class MeetSemiLattice a => CompleteMeetSemiLattice a where bottom :: a class Ord a => JoinSemiLattice a where join :: a -> a -> a class JoinSemiLattice a => CompleteJoinSemiLattice a where top :: a and Ord defines a partial order (and hence induces Eq) on a type. (e.g. instance Ord a => Eq a where x == y = x <= y && y <= x ) I don't really think bottoms and tops really get bundled in with the strict mathematical definition, e.g. natural numbers have all finite joins but no top, Integer has no bottom or top but all finite joins and meets, etc. Again, your design seems to incorporate the kind of simplicity that language implementors might want for a Standard Prelude, so your judgment on how much generality is appropriate here would probably be good. Cheers, Bill

Dylan Thurston wrote:
I've started writing up a more concrete proposal for what I'd like the Prelude to look like in terms of numeric classes.
I like this proposal a lot. The organization is closer to traditional mathematical structures than the current Prelude, but not as intimidating as Mechveliani's Basic Algebra Proposal. A very nice balance, IMO. A couple of requests:
module Lattice where class Lattice a where meet, join :: a -> a -> a
Could this be split into class SemiLattice a where join :: a -> a -> a and class (SemiLattice a) => Lattice a where meet :: a -> a -> a I run across a lot of structures which could usefully be modeled as semilattices, but lack a 'meet' operation.
It would be reasonable to make Ord a subclass of this, but it would probably complicate the class heirarchy too much for the gain.
In a similar vein, I'd really like to see the Ord class split up: class PartialOrder a where (<), (>) :: a -> a -> Bool class (Eq a, PartialOrder a) => Ord a where compare :: a -> a -> Ordering (<=), (>=) :: a -> a -> Bool max, min :: a -> a -> a Perhaps it would make sense for PartialOrder to be a superclass of Lattice? --Joe English jenglish@flightlab.com

Thanks for the comments! On Mon, Feb 12, 2001 at 12:26:35AM +0000, Marcin 'Qrczak' Kowalczyk wrote:
I don't like the fact that there is no Powerful Integer Integer.
Reading this, it occurred to me that you could explictly declare an instance of Powerful Integer Integer and have everything else work.
Then the second argument of (^) is always arbitrary RealIntegral,
Nit: the second argument should be an Integer, not an arbitrary RealIntegral.
class (Real a, Floating a) => RealFrac a where -- lifted directly from Haskell 98 Prelude properFraction :: (Integral b) => a -> (b,a) truncate, round :: (Integral b) => a -> b ceiling, floor :: (Integral b) => a -> b
Should be RealIntegral instead of Integral.
Yes. I'd actually like to make it Integer, and let the user compose with fromInteger herself.
Perhaps RealIntegral should be called Integral, and your Integral should be called somewhat differently.
Perhaps. Do you have suggestions for names? RealIntegral is what naive users probably want, but Integral is what mathematicians would use (and call something like an integral domain).
class (Real a, Integral a) => RealIntegral a where quot, rem :: a -> a -> a quotRem :: a -> a -> (a,a)
-- Minimal definition: toInteger
You forgot toInteger.
Oh, right. I actually had it and then deleted it. On the one hand, it feels very implementation-specific to me, comparable to the decodeFloat routines (which are useful, but not generally applicable). On the other hand, I couldn't think of many examples where I really wouldn't want that operation (other than monadic numbers, that, say, count the number of operations), and I couldn't think of a better place to put it. You'll notice that toRational was similarly missing. My preferred solution might still be the Convertible class I mentioned earlier. Recall it was class Convertible a b where convert :: a -> b maybe with another class like class (Convertible a Integer) => ConvertibleToInteger a where toInteger :: a -> Integer toInteger = convert if the restrictions on instance contexts remain. Convertible a b should indicate that a can safely be converted to b without losing any information and maintaining relevant structure; from this point of view, its use would be strictly limited. (But what's relevant?) I'm still undecided here. Best, Dylan Thurston

On 11-Feb-2001, Dylan Thurston
class (Num a) => Integral a where div, mod :: a -> a -> a divMod :: a -> a -> (a,a) gcd, lcm :: a -> a -> a extendedGCD :: a -> a -> (a,a,a)
-- Minimal definition: divMod or (div and mod) -- and extendedGCD, if the provided definition does not work div a b | (d,_) <- divMod a b = d mod a b | (_,m) <- divMod a b = m divMod a b = (div a b, mod a b) gcd a b | (_,_,g) <- extendedGCD a b = g extendedGCD a b = ... -- insert Euclid's algorithm here lcm a b = (a `div` gcd a b) * b
Integral has the mathematical structure of a unique factorization domain, satisfying the laws
a * b === b * a (div a b) * b + (mod a b) === a mod (a+k*b) b === mod a b a `div` gcd a b === zero gcd a b === gcd b a gcd (a + k*b) b === gcd a b a*c + b*d === g where (c, d, g) = extendedGCD a b
TODO: quot, rem partially defined. Explain. The default definition of extendedGCD above should not be taken as canonical (unlike most default definitions); for some Integral instances, the algorithm could diverge, might not satisfy the laws above, etc.
In that case, I think it might be better to not provide it as a default, and instead to provide a function called say `euclid_extendedGCD'; someone defining an instance can then extendedGCD = euclid_extendedGCD if that is appropriate. It's so much easier to find bugs in code that you did write rather than bugs which are caused by what you *didn't* write. Of course this is not so effective if we keep the awful Haskell 98 rule that instance methods always default to bottom if not defined; but even if that rule is not changed, compilers can at least warn about that case.
class (Num a, Additive b) => Powerful a b where (^) :: a -> b -> a
I don't like the name. Plain `Pow' would be better, IMHO.
Apart from those two points, I quite like this proposal,
at least at first glance.
--
Fergus Henderson

On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
There is an additional property of zero being neglected here, namely that it is an annihilator. That is,
zero * x === zero x * zero === zero
It follows: zero * x === (one - one) * x === one * x - one * x === x - x === zero
Again, it's probably a reasonable compromise not to accommodate nonassociative algebras, though an important application of them lies within graphics, namely 3-vectors with the cross product.
Agreed that non-associative algebras are useful, but I feel that they should have a different symbol.
class (Num a) => Integral a where div, mod :: a -> a -> a divMod :: a -> a -> (a,a) gcd, lcm :: a -> a -> a extendedGCD :: a -> a -> (a,a,a)
While I'm wholeheartedly in favor of the Euclidean algorithm idea, I suspect that more structure (i.e. separating it out to another class) could be useful, for instance, formal power series' over Z are integral domains, but are not a Euclidean domain because their residue classes aren't computable by a finite process. Various esoteric rings like Z[sqrt(k)] for various positive and negative integer k can also make this dependence explode, though they're probably too rare to matter.
<technical math> I tried to write the definitions in a way that could be defined for any unique factorization domain, not necessarily Euclidean: just take the two numbers, write them as a unit times prime factors in canonical form, and take the product of the common factors and call that the GCD. On reflection, extendedGCD probably isn't easy to write in general. What operations would you propose to encapsulate an integral domain (rather than a UFD)? Formal power series over Z are an interesting example; I'll think about it. On first blush, it seems like if you represented them as lazy lists you might be able to compute the remainder term by term.
TODO: quot, rem partially defined. Explain. The default definition of extendedGCD above should not be taken as canonical (unlike most default definitions); for some Integral instances, the algorithm could diverge, might not satisfy the laws above, etc. TODO: (/) is only partially defined. How to specify? Add a member isInvertible :: a -> Bool? Typical examples include rationals, the real numbers, and rational functions (ratios of polynomials).
It's too easy to make it a partial function to really consider this, but if you wanted to go over the top (and you don't) you want the multiplicative group of units to be the type of the argument (and hence result) of recip.
Yes. I considered and rejected that. But it would be nice to let callers check whether the division will blow up, and that's not possible for classes that aren't members of Eq. But I suppose that's the whole point. For computable reals, the way I would compute 1/(very small number) would be to look at (very small number) more and more closely to figure out on which side of 0 it lay; if it actually were zero, the program would loop. I think programs that want to avoid this have to take type-specific steps (in this case, cutting off the evaluation at a certain point.)
What you're really trying to capture here is the (right?) Z-module-like structure of the multiplicative monoid in a commutative ring. There are some weird things going on here I'm not sure about, namely:
Right.
(3) Under some condition I don't seem to be able to formulate offhand, one can do (^) :: ring -> ring -> ring Now the ring (or perhaps more generally some related ring) acts on ring to produce an expontiation operation like what is typically thought of for real numbers. Anyone with good ideas as to what the appropriate conditions are here, please speak up. (Be careful, w ^ z = exp (z * log w) behaves badly for w < 0 on the reals.)
For complex numbers as well, this operation has problems because of branch cuts. It does satisfy that identity I mentioned, but is not continuous in the first argument. It is more common to see functions like exp be well defined (for more general additive groups) than to see the full (^) be defined.
class (Num a, Ord a) => Real a where abs :: x -> x signum :: x -> x
I'm not convinced that Real is a great name for this, or that this is really the right type for all this stuff. I'd still like to see abs and signum generalized to vector spaces.
After thinking about this, I decided that I would be happy calling the comparable operation on vector spaces "norm": a) it's compatible with mathematical usage b) it keeps the Prelude itself simple. It's unfortunate that the operation for complex numbers can't be called "abs", but I think it's reasonable.
<good stuff on lattices deleted> ...and Ord defines a partial order (and hence induces Eq) on a type.
I think that "Ord" should define a total ordering; it's certainly what naive users would expect. I would define another class "Poset" with a partial ordering.
(e.g. instance Ord a => Eq a where x == y = x <= y && y <= x )
But to define <= in terms of meet and join you already need Eq! x <= y === meet x y == y Best, Dylan Thurston

Dylan Thurston wrote:
I've started writing up a more concrete proposal for what I'd like the Prelude to look like in terms of numeric classes. Please find it attached below. It's still a draft and rather incomplete, but please let me know any comments, questions, or suggestions.
This is a good basis for discussion, and it helps to see something concrete. Here are a few comments:
Thus these laws should be interpreted as guidelines rather than absolute rules. In particular, the compiler is not allowed to use them. Unless stated otherwise, default definitions should also be taken as laws.
Including laws was discussed very early in the development of the language, but was rejected. IIRC Miranda had them. The argument against laws was that their presence might mislead users into the assumption that they did hold, yet if they were not enforcable then they might not hold and that could have serious consequences. Also, some laws do not hold in domains with bottom, e.g. a + (negate a) === 0 is only true if a is not bottom.
class (Additive a) => Num a where (*) :: a -> a -> a one :: a fromInteger :: Integer -> a
-- Minimal definition: (*), one fromInteger 0 = zero fromInteger n | n < 0 = negate (fromInteger (-n)) fromInteger n | n > 0 = reduceRepeat (+) one n
This definition requires both Eq and Ord!!! As does this one:
class (Num a, Additive b) => Powerful a b where (^) :: a -> b -> a instance (Num a) => Powerful a (Positive Integer) where a ^ 0 = one a ^ n = reduceRepeated (*) a n instance (Fractional a) => Powerful a Integer where a ^ n | n < 0 = recip (a ^ (negate n)) a ^ n = a ^ (positive n)
and several others further down.
(4) In some cases, the hierarchy is not finely-grained enough: operations that are often defined independently are lumped together. For instance, in a financial application one might want a type "Dollar", or in a graphics application one might want a type "Vector". It is reasonable to add two Vectors or Dollars, but not, in general, reasonable to multiply them. But the programmer is currently forced to define a method for (*) when she defines a method for (+).
Why do you stop at allowing addition on Dollars and not include multiplication by a scalar? Division is also readily defined on Dollar values, with a scalar result, but this, too, is not available in the proposal. Having Units as types, with the idea of preventing adding Apples to Oranges, or Dollars to Roubles, is a venerable idea, but is not in widespread use in actual programming languages. Why not? Vectors, too, can be multiplied, producing both scalar- and vector-products. It seems that you are content with going as far as the proposal permits, though you cannot define, even within the revised Class system, all the common and useful operations on these types. This is the same situation as with Haskell as it stands. The question is whether the (IMHO) marginal increase in flexibility is worth the cost. This is not an argument for not separating Additive from Num, but it does weaken the argument for doing it. --brian

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
It follows: zero * x === (one - one) * x === one * x - one * x === x - x === zero
Heh, you've caught me sleeping. =) On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
I tried to write the definitions in a way that could be defined for any unique factorization domain, not necessarily Euclidean: just take the two numbers, write them as a unit times prime factors in canonical form, and take the product of the common factors and call that the GCD. On reflection, extendedGCD probably isn't easy to write in general.
Well, factorizing things in various UFD's doesn't sound easy to me, but at this point I'm already having to do some reaching for counterexamples of practical programs where this matters. It could end up being a useless class method in some instances, so I'm wary of it. On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
What operations would you propose to encapsulate an integral domain (rather than a UFD)?
I'm not necessarily proposing a different set of operations to encapsulate them, but rather that gcd and cousins be split off into another subclass. Your design decisions in general appear to be striking a good chord, so I'll just bring up the idea and let you decide whether it should be done that way and so on. On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
Formal power series over Z are an interesting example; I'll think about it. On first blush, it seems like if you represented them as lazy lists you might be able to compute the remainder term by term.
Consider taking of the residue of a truly infinite member of Z[[x]] mod an ideal generated by a polynomial, e.g. 1/(1-x) mod (1+x^2). You can take the residue of each term of 1/(1-x), so x^(2n) -> (-1)^n and x^(2n+1) -> (-1)^n x, but you end up with an infinite number of (nonzero!) residues to add up and hence encounter the troubles with processes not being finite that I mentioned. On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
(3) Under some condition I don't seem to be able to formulate offhand, one can do (^) :: ring -> ring -> ring Now the ring (or perhaps more generally some related ring) acts on ring to produce an expontiation operation like what is typically thought of for real numbers. Anyone with good ideas as to what the appropriate conditions are here, please speak up. (Be careful, w ^ z = exp (z * log w) behaves badly for w < 0 on the reals.)
On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
For complex numbers as well, this operation has problems because of branch cuts. It does satisfy that identity I mentioned, but is not continuous in the first argument. It is more common to see functions like exp be well defined (for more general additive groups) than to see the full (^) be defined.
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 Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
I'm not convinced that Real is a great name for this, or that this is really the right type for all this stuff. I'd still like to see abs and signum generalized to vector spaces.
On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
After thinking about this, I decided that I would be happy calling the comparable operation on vector spaces "norm": a) it's compatible with mathematical usage b) it keeps the Prelude itself simple. It's unfortunate that the operation for complex numbers can't be called "abs", but I think it's reasonable.
I'm not entirely sure, but I think part of the reason this hasn't been done already is because it's perhaps painful to statically type dimensionality in vector spaces. On the other hand, assuming that the user has perhaps contrived a representation satisfactory to him or her, defining a class on the necessary type constructor shouldn't be tough at all. In a side note, it seems conventional to use abs and signum on complex numbers (and functions), and also perhaps the same symbol as abs for the norm on vectors and vector functions. It seems the distinction drawn is that abs is definitely pointwise and the norm more often does some sort of shenanigan like L^p norms etc. How much of this convention should be preserved seems like a design decision, but perhaps one that should be made explicit. On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
<good stuff on lattices deleted> ...and Ord defines a partial order (and hence induces Eq) on a type.
On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
I think that "Ord" should define a total ordering; it's certainly what naive users would expect. I would define another class "Poset" with a partial ordering.
I neglected here to add in the assumption that (<=) was a total relation, I had in mind antisymmetry of (<=) in posets so that element isomorphism implies equality. Introducing a Poset class where elements may be incomparable appears to butt against some of the bits where Bool is hardwired into the language, at least where one might attempt to use a trinary logical type in place of Bool to denote the result of an attempted comparison. On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
(e.g. instance Ord a => Eq a where x == y = x <= y && y <= x )
On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
But to define <= in terms of meet and join you already need Eq!
x <= y === meet x y == y
I don't usually see this definition of (<=), and it doesn't seem like the natural way to go about defining it on most machines. The notion of the partial (possibly total) ordering (<=) seems to be logically prior to that of the meet to me. The containment usually goes: reflexive + transitive partial relation (preorder) => antisymmetric (partial order) [lattices possible here with additional structure, also equality decidable in terms of <= independently of the notion of lattices, for arbitrary partial orders] => total relation (well ordering) Whether this matters for library design is fairly unclear. Good work! Cheers, Bill

Brian Boutel writes: : | Having Units as types, with the idea of preventing adding Apples to | Oranges, or Dollars to Roubles, is a venerable idea, but is not in | widespread use in actual programming languages. Why not? There was a pointer to some good papers on this in a previous discussion of units and dimensions: http://www.mail-archive.com/haskell@haskell.org/msg04490.html The main complication is that the type system needs to deal with integer exponents of dimensions, if it's to do the job well. For example, it should be OK to divide an acceleration (length * time^-2) by a density (mass * length^-3). Such things may well occur as subexpressions of something more intuitive, and it's undesirable to spell out all the anticipated dimension types in a program (a Haskell 98 program, for example) because: - Only an arbitrary finite number would be covered, and - The declarations would contain enough un-abstracted clichés to bring a tear to the eye. instance Mul Double (Dim_L Double) (Dim_L Double) instance Mul (Dim_L Double) (Dim_per_T Double) (Dim_L_per_T Double) etc. Regards, Tom

On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
Including laws was discussed very early in the development of the language, but was rejected. IIRC Miranda had them. The argument against laws was that their presence might mislead users into the assumption that they did hold, yet if they were not enforcable then they might not hold and that could have serious consequences. Also, some laws do not hold in domains with bottom, e.g. a + (negate a) === 0 is only true if a is not bottom.
I actually think it would be useful to have them and optionally dynamically enforce them, or at least whichever ones are computable, as a compile-time option. This would be _extremely_ useful for debugging purposes, and I, at the very least, would use it. I think Eiffel does something like this, can anyone else comment? This, of course, is a language extension, and so probably belongs in a different discussion from the rest of all this. Dylan Thurston wrote:
class (Additive a) => Num a where (*) :: a -> a -> a one :: a fromInteger :: Integer -> a -- Minimal definition: (*), one fromInteger 0 = zero fromInteger n | n < 0 = negate (fromInteger (-n)) fromInteger n | n > 0 = reduceRepeat (+) one n
On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
This definition requires both Eq and Ord!!!
Only on Integer, not on a. On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
As does this one:
Dylan Thurston wrote:
class (Num a, Additive b) => Powerful a b where (^) :: a -> b -> a instance (Num a) => Powerful a (Positive Integer) where a ^ 0 = one a ^ n = reduceRepeated (*) a n instance (Fractional a) => Powerful a Integer where a ^ n | n < 0 = recip (a ^ (negate n)) a ^ n = a ^ (positive n)
I should note that both of these definitions which require Eq and Ord only require it on Integer. On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
and several others further down.
I'm not sure which ones you hit on, though I'm sure we'd all be more than happy to counter-comment on them or repair the inadequacies. Dylan Thurston wrote:
(4) In some cases, the hierarchy is not finely-grained enough: operations that are often defined independently are lumped together. For instance, in a financial application one might want a type "Dollar", or in a graphics application one might want a type "Vector". It is reasonable to add two Vectors or Dollars, but not, in general, reasonable to multiply them. But the programmer is currently forced to define a method for (*) when she defines a method for (+).
On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
Why do you stop at allowing addition on Dollars and not include multiplication by a scalar? Division is also readily defined on Dollar values, with a scalar result, but this, too, is not available in the proposal.
I can comment a little on this, though I can't speak for someone else's design decisions. In general, the results of division and multiplication for units have a different result type than those of the arguments. This makes defining them by type class overloading either require existential wrappers or makes them otherwise difficult or impossible to define. On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
Having Units as types, with the idea of preventing adding Apples to Oranges, or Dollars to Roubles, is a venerable idea, but is not in widespread use in actual programming languages. Why not?
I'm probably even less qualified to comment on this, but I'll conjecture that the typing disciplines of most languages make it impractical. I suspect it could be possible in Haskell. On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
Vectors, too, can be multiplied, producing both scalar- and vector-products.
Exterior and inner products both encounter much the same troubles as defining arithmetic on types with units attached, with the additional complication that statically typing dimensionality is nontrivial. On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
It seems that you are content with going as far as the proposal permits, though you cannot define, even within the revised Class system, all the common and useful operations on these types. This is the same situation as with Haskell as it stands. The question is whether the (IMHO) marginal increase in flexibility is worth the cost. This is not an argument for not separating Additive from Num, but it does weaken the argument for doing it.
I'm not convinced of this, though I _am_ convinced that a general framework for units would probably be useful to have in either a standard or add-on library distributed with Haskell, or perhaps to attempt to address units even within the standard Prelude if it's simple enough. Are you up to perhaps taking a stab at this? Perhaps if you tried it within the framework Thurston has laid out, some of the inadequacies could be revealed. Cheers, Bill

Mon, 12 Feb 2001 17:24:37 +1300, Brian Boutel
class (Additive a) => Num a where (*) :: a -> a -> a one :: a fromInteger :: Integer -> a
-- Minimal definition: (*), one fromInteger 0 = zero fromInteger n | n < 0 = negate (fromInteger (-n)) fromInteger n | n > 0 = reduceRepeat (+) one n
This definition requires both Eq and Ord!!!
Only Eq Integer and Ord Integer, which are always there.
Why do you stop at allowing addition on Dollars and not include multiplication by a scalar?
Perhaps because there is no good universal type for (*). Sorry, it would have to have a different symbol.
Having Units as types, with the idea of preventing adding Apples to Oranges, or Dollars to Roubles, is a venerable idea, but is not in widespread use in actual programming languages. Why not?
It does not scale to more general cases. (m/s) / (s) = (m/s^2), so (/) would have to have the type (...) => a -> b -> c, which is not generally usable because of ambiguities. Haskell's classes are not powerful enough to define full algebra of units.
It seems that you are content with going as far as the proposal permits, though you cannot define, even within the revised Class system, all the common and useful operations on these types. This is the same situation as with Haskell as it stands. The question is whether the (IMHO) marginal increase in flexibility is worth the cost.
The Prelude class system requires a compromise. There is no single design which accommodates all needs because Haskell's classes are not powerful enough to unify all levels of generality in a single class operation. And even if it was possible, it would be awkward to use in simpler cases. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

Sun, 11 Feb 2001 18:48:42 -0800, William Lee Irwin III
class Ord a => MeetSemiLattice a where meet :: a -> a -> a
class MeetSemiLattice a => CompleteMeetSemiLattice a where bottom :: a
class Ord a => JoinSemiLattice a where join :: a -> a -> a
class JoinSemiLattice a => CompleteJoinSemiLattice a where top :: a
Please: ok, but not for Prelude! -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

Sun, 11 Feb 2001 22:27:53 -0500, Dylan Thurston
Reading this, it occurred to me that you could explictly declare an instance of Powerful Integer Integer and have everything else work.
No, because it overlaps with Powerful a Integer (the constraint on a doesn't matter for determining if it overlaps).
Then the second argument of (^) is always arbitrary RealIntegral,
Nit: the second argument should be an Integer, not an arbitrary RealIntegral.
Of course not. (2 :: Integer) ^ (i :: Int) makes perfect sense.
You forgot toInteger.
Oh, right. I actually had it and then deleted it. On the one hand, it feels very implementation-specific to me, comparable to the decodeFloat routines
It is needed for conversions (fromIntegral in particular).
class Convertible a b where convert :: a -> b maybe with another class like class (Convertible a Integer) => ConvertibleToInteger a where toInteger :: a -> Integer toInteger = convert
This requires to write a Convertible instance in addition to ConvertibleToInteger, where currently mere toInteger in Integral suffices. Since Convertible must be defined separately for each pair of types (otherwise instances would easily overlap), it's not very useful for numeric conversions. Remember that there are a lot of numeric types in the FFI: Int8, Word16, CLong, CSize. It does not provide anything in this area so should not be required to define instances there. After a proposal is developed, please check how many instances one has to define to make a type the same powerful as Int, and is it required to define methods irrelevant to non-mathematical needs. basAlgPropos fails badly in this criterion.
Convertible a b should indicate that a can safely be converted to b without losing any information and maintaining relevant structure;
So fromInteger does not require Convertible, which is inconsistent with toInteger. Sorry, I am against Convertible in Prelude - tries to be too general, which makes it inappropriate. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

Tom Pledger:
Brian Boutel writes: : | Having Units as types, with the idea of preventing adding Apples to | Oranges, or Dollars to Roubles, is a venerable idea, but is not in | widespread use in actual programming languages. Why not?
There was a pointer to some good papers on this in a previous discussion of units and dimensions:
http://www.mail-archive.com/haskell@haskell.org/msg04490.html
The main complication is that the type system needs to deal with integer exponents of dimensions, if it's to do the job well.
Andrew Kennedy has basically solved this for higher order languages with HM type inference. He made an extension of the ML type system with dimensional analysis a couple of years back. Sorry I don't have the references at hand but he had a paper in ESOP I think. I think the real place for dimension and unit inference is in modelling languages, where you can specify physical systems through differential equations and simulate them numerically. Such languages are being increasingly used in the "real world" now. It would be quite interesting to have a version of Haskell that would allow the specification of differential equations, so one could make use of all the good features of Haskell for this. This would allow the unified specification of systems that consist both of physical and computational components. This niche is now being filled by a mix of special-purpose modeling languages like Modelica and Matlab/Simulink for the physical part, and SDL and UML for control parts. The result is likely to be a mess, in particular when these specifications are to be combined into full system descriptions. Björn Lisper

On Mon, Feb 12, 2001 at 05:24:37PM +1300, Brian Boutel wrote:
Thus these laws should be interpreted as guidelines rather than absolute rules. In particular, the compiler is not allowed to use them. Unless stated otherwise, default definitions should also be taken as laws.
Including laws was discussed very early in the development of the language, but was rejected. IIRC Miranda had them. The argument against laws was that their presence might mislead users into the assumption that they did hold, yet if they were not enforcable then they might not hold and that could have serious consequences. Also, some laws do not hold in domains with bottom, e.g. a + (negate a) === 0 is only true if a is not bottom.
These are good points, but I still feel that laws can be helpful as guidelines, as long as they are not interpreted as anything more. For instance, the Haskell Report does give laws for Monads and quotRem, although they, too, are not satisfied in the presence of bottom, etc. (Is that right?) Writing out the laws lets me say, for instance, whether users of Num and Fractional should expect multiplication to be commutative. (No and yes, respectively. I require Fractional to be commutative mainly because common usage does not use either '/' or 'reciprocal' to indicate inverse in a non-commutative ring.)
class (Additive a) => Num a where (*) :: a -> a -> a one :: a fromInteger :: Integer -> a
-- Minimal definition: (*), one fromInteger 0 = zero fromInteger n | n < 0 = negate (fromInteger (-n)) fromInteger n | n > 0 = reduceRepeat (+) one n
This definition requires both Eq and Ord!!!
Ah, but only Eq and Ord for Integer, which (as a built-in type) has Eq and Ord instances. The type signature for reduceRepeated is reduceRepeated :: (a -> a -> a) -> a -> Integer -> a
As does this one:
class (Num a, Additive b) => Powerful a b where (^) :: a -> b -> a instance (Num a) => Powerful a (Positive Integer) where a ^ 0 = one a ^ n = reduceRepeated (*) a n instance (Fractional a) => Powerful a Integer where a ^ n | n < 0 = recip (a ^ (negate n)) a ^ n = a ^ (positive n)
Likewise here.
and several others further down.
I tried to be careful not to use Eq and Ord for generic types when not necessary, but I may have missed some. Please let me know. (Oh, I just realised that Euclid's algorithm requires Eq. Oops. That's what I get for not writing it out explicitly. I'll have to revisit the Integral part of the hierarchy.)
(4) In some cases, the hierarchy is not finely-grained enough: operations that are often defined independently are lumped together. For instance, in a financial application one might want a type "Dollar", or in a graphics application one might want a type "Vector". It is reasonable to add two Vectors or Dollars, but not, in general, reasonable to multiply them. But the programmer is currently forced to define a method for (*) when she defines a method for (+).
Why do you stop at allowing addition on Dollars and not include multiplication by a scalar? Division is also readily defined on Dollar values, with a scalar result, but this, too, is not available in the proposal.
I will allow multiplication by a scalar; it's just not in the classes I've written down so far. (And may not be in the Prelude.) Thanks for reminding me about division. I had forgotten about that. It bears some thought.
Having Units as types, with the idea of preventing adding Apples to Oranges, or Dollars to Roubles, is a venerable idea, but is not in widespread use in actual programming languages. Why not?
That's a good question. I don't know. One cheeky answer would be for lack of a powerful enough type system (allowing you to, e.g., work on generic units when you want to), but I don't know if that is actually true. Don't modern HP calculators use units consistently?
Vectors, too, can be multiplied, producing both scalar- and vector-products.
Yes, but these are really different operations and should be represented with different symbols. Neither one is associative, for instance.
It seems that you are content with going as far as the proposal permits, though you cannot define, even within the revised Class system, all the common and useful operations on these types. This is the same situation as with Haskell as it stands. The question is whether the (IMHO) marginal increase in flexibility is worth the cost.
I believe that with this structure as base, the other common and useful operations can easily be added on top. But I should go ahead and do it. Best, Dylan Thurston

On Mon, Feb 12, 2001 at 07:24:31AM +0000, Marcin 'Qrczak' Kowalczyk wrote:
Sun, 11 Feb 2001 22:27:53 -0500, Dylan Thurston
pisze: Reading this, it occurred to me that you could explictly declare an instance of Powerful Integer Integer and have everything else work. No, because it overlaps with Powerful a Integer (the constraint on a doesn't matter for determining if it overlaps).
Point. Thanks. Slightly annoying.
Then the second argument of (^) is always arbitrary RealIntegral,
Nit: the second argument should be an Integer, not an arbitrary RealIntegral.
Of course not. (2 :: Integer) ^ (i :: Int) makes perfect sense.
But for arbitrary RealIntegrals it need not make sense. Please do not assume that toInteger :: RealIntegral a => a -> Integer toInteger n | n < 0 = toInteger negate n toInteger 0 = 0 toInteger n | n > 0 = 1 + toInteger (n-1) (or the more efficient version using 'even') terminates (in principle) for all RealIntegrals, at least with the definition as it stands in my proposal. Possibly toInteger should be added; then (^) could have the type you suggest. For usability issues, I suppose it should. (E.g., users will want to use Int ^ Int.) OK, I'm convinced of the necessity of toInteger (or an equivalent). I'll fit it in. Best, Dylan Thurston

On Sun, Feb 11, 2001 at 09:17:53PM -0800, William Lee Irwin III wrote:
Consider taking of the residue of a truly infinite member of Z[[x]] mod an ideal generated by a polynomial, e.g. 1/(1-x) mod (1+x^2). You can take the residue of each term of 1/(1-x), so x^(2n) -> (-1)^n and x^(2n+1) -> (-1)^n x, but you end up with an infinite number of (nonzero!) residues to add up and hence encounter the troubles with processes not being finite that I mentioned.
Sorry, isn't (1+x^2) invertible in Z[[x]]?
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.)
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? For the Complex class, that should be the choice.
I neglected here to add in the assumption that (<=) was a total relation, I had in mind antisymmetry of (<=) in posets so that element isomorphism implies equality. Introducing a Poset class where elements may be incomparable appears to butt against some of the bits where Bool is hardwired into the language, at least where one might attempt to use a trinary logical type in place of Bool to denote the result of an attempted comparison.
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.
On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
But to define <= in terms of meet and join you already need Eq!
x <= y === meet x y == y
I don't usually see this definition of (<=), and it doesn't seem like the natural way to go about defining it on most machines. The notion of the partial (possibly total) ordering (<=) seems to be logically prior to that of the meet to me. The containment usually goes:
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. (In a completely fine-grained ordering heirarchy, I would have the equation I gave above as a default definition for <=, with the expectation that most users would want to override it. Compare my fromInteger default definition.) Best, Dylan Thurston

On Mon, Feb 12, 2001 at 10:08:02AM +0100, Bjorn Lisper wrote:
The main complication is that the type system needs to deal with integer exponents of dimensions, if it's to do the job well. Andrew Kennedy has basically solved this for higher order languages with HM type inference. He made an extension of the ML type system with dimensional analysis a couple of years back. Sorry I don't have the references at hand but he had a paper in ESOP I think.
The papers I could find (e.g., http://citeseer.nj.nec.com/kennedy94dimension.html, "Dimension Types") mention extensions to ML. I wonder if it is possible to work within the Haskell type system, which is richer than ML's type system. The main problem I see is that the dimensions should commute: Length * Time = Time * Length. I can't think of how to represent Length, Time, and * as types, type constructors, or whatnot so that that would be true. You could put in functions to explicitly do the conversion, but that obviously gets impractical. Any such system would probably not be able to type (^), since the output type depends on the exponent. I think that is acceptable. I think you would also need a finer-grained heirarchy in the Prelude (including than in my proposal) to get this to work.
It would be quite interesting to have a version of Haskell that would allow the specification of differential equations, so one could make use of all the good features of Haskell for this. This would allow the unified specification of systems that consist both of physical and computational components. This niche is now being filled by a mix of special-purpose modeling languages like Modelica and Matlab/Simulink for the physical part, and SDL and UML for control parts. The result is likely to be a mess, in particular when these specifications are to be combined into full system descriptions.
My hope is that you wouldn't need a special version of Haskell. Best, Dylan Thurston

Dylan Thurston writes: | Any such system would probably not be able to type (^), since the | output type depends on the exponent. I think that is acceptable. In other words, the first argument to (^) would have to be dimensionless? I agree. So would the arguments to trig functions, etc. Ashley Yakeley writes: | Very occasionally non-integer or 'fractal' exponents of dimensions | are useful. For instance, geographic coastlines can be measured in | km ^ n, where 1 <= n < 2. This doesn't stop the CIA world factbook | listing all coastline lengths in straight kilometres, however. David Barton writes: | Even without fractals, there are cases where weird dimensions come | up (I ran across this in my old MHDL (microwave) days). Square | root volts is the example that was constantly thrown in my face. In both of those cases, the apparent non-integer dimension is accompanied by a particular unit (km, V). So, could they equally well be handled by stripping away the units and exponentiating a dimensionless number? For example: (x / 1V) ^ y Regards, Tom

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

Tom Pledger writes: In both of those cases, the apparent non-integer dimension is accompanied by a particular unit (km, V). So, could they equally well be handled by stripping away the units and exponentiating a dimensionless number? For example: (x / 1V) ^ y I think not. The "Dimension Types" paper really is excellent, and makes the distinction between the necessity of exponents on the dimensions and the exponents on the numbers very clear; I commend it to everyone in this discussion. The two things (a number of "square root volts" and a "number of volts to an exponent" are different things, unless you are simply trying to represent a ground number as an expression! Dave Barton <*> dlb@averstar.com )0( http://www.averstar.com/~dlb

On Mon, Feb 12, 2001 at 12:26:35AM +0000, Marcin 'Qrczak' Kowalczyk wrote:
I must say I like it. It has a good balance between generality and usefulness / convenience.
Modulo a few details, see below.
class (Num a, Additive b) => Powerful a b where (^) :: a -> b -> a instance (Num a) => Powerful a (Positive Integer) where a ^ 0 = one a ^ n = reduceRepeated (*) a n instance (Fractional a) => Powerful a Integer where a ^ n | n < 0 = recip (a ^ (negate n)) a ^ n = a ^ (positive n)
I don't like the fact that there is no Powerful Integer Integer. Since the definition on negative exponents really depends on the first type but can be polymorphic wrt. any Integral exponent, I would make other instances instead:
instance RealIntegral b => Powerful Int b instance RealIntegral b => Powerful Integer b instance (Num a, RealIntegral b) => Powerful (Ratio a) b instance Powerful Float Int instance Powerful Float Integer instance Powerful Float Float instance Powerful Double Int instance Powerful Double Integer instance Powerful Double Double
OK, I'm slow. I finally understand your point here. I might leave off a few cases, and simplify this to instance Powerful Int Int instance Powerful Integer Integer instance (Num a, SmallIntegral b) => Powerful (Ratio a) b instance Powerful Float Float instance Powerful Double Double instance Powerful Complex Complex (where "SmallIntegral" is a class that contains toInteger; "small" in the sense that it fits inside an Integer.) All of these call one of 3 functions: postivePow :: (Num a, SmallIntegral b) => a -> b -> a integerPow :: (Fractional a, SmallIntegral b) => a -> b -> a analyticPow :: (Floating a) => a -> a -> a (These 3 functions might be in a separate module from the Prelude.) Consequences: you cannot, e.g., raise a Double to an Integer power without an explicit conversion or calling a different function (or declaring your own instance). Is this acceptable? I think it might be: after all, you can't multiply a Double by an Integer either... You then have one instance declaration per type, just as for the other classes. Opinions? I'm still not very happy. Best, Dylan Thurston

Tue, 13 Feb 2001 14:01:25 -0500, Dylan Thurston
Consequences: you cannot, e.g., raise a Double to an Integer power without an explicit conversion or calling a different function (or declaring your own instance). Is this acceptable?
I don't like it: (-3::Double)^2 should be 9, and generally x^(2::Integer) should be x*x for all types of x where it makes sense. Same for Int. (**) does not work for negative base. Neither of (^) and (**) is a generalization of the other: the knowledge that an exponent is restricted to integers widens the domain of the base. x^2 = x*x cannot actually work for any x in Num, or whatever the class of (*) is called, if (^) is not defined inside the same class. This is because (^) is unified with (^^): the unified (^) should use recip if available, but be partially defined without it if it's not available. So I propose to put (^) together with (*). With a default definition of course. It means "apply (*) the specified number of times", and for fractional types has a meaning extended to negative exponents. (^) is related to (*) as discussed times or scale is related to (+). (**):: a -> a -> a, together with other analytic functions. Sorry, the fact that they are written the same in conventional math is not enough to force their unification against technical reasons. It's not bad: we succeeded in unification of (^) and (^^). -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

Hi, I don't know if this is useful, but in response to a link to that article that I posted on Lambda, someone posted a link arguing that such an approach (at least in Ada) was impractical. To be honest, I don't find it very convincing, but I haven't been following this discussion in detail. It might raise some problems you have not considered. Anyway, if you are interested, it's all at http://lambda.weblogs.com/discuss/msgReader$818 Apologies if it's irrelevant or you've already seen it, Andrew On Mon, Feb 12, 2001 at 01:51:54PM -0500, Dylan Thurston wrote: [...]
The papers I could find (e.g., http://citeseer.nj.nec.com/kennedy94dimension.html, "Dimension Types") mention extensions to ML. I wonder if it is possible to work within the Haskell type system, which is richer than ML's type system. [...]
participants (10)
-
andrew@andrewcooke.free-online.co.uk
-
Bjorn Lisper
-
Brian Boutel
-
David Barton
-
Dylan Thurston
-
Fergus Henderson
-
Joe English
-
qrczak@knm.org.pl
-
Tom Pledger
-
William Lee Irwin III