I guess nontermination is a problem (e.g. if one or both functions fail to terminate for some values, equality will be undecidable). /Jonas On 14 April 2010 08:42, Ashley Yakeley wrote:

On Wed, 2010-04-14 at 16:11 +1000, Ivan Miljenovic wrote:

...

but the only way you can "prove" it in Haskell is by comparing the values for the entire domain  (which gets computationally expensive)...

It's not expensive if the domain is, for instance, Bool.

-- Ashley Yakeley

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ivan Lazar Miljenovic wrote:

Ashley Yakeley writes:

...

On Wed, 2010-04-14 at 16:11 +1000, Ivan Miljenovic wrote:

...

but the only way you can "prove" it in Haskell is by comparing the values for the entire domain (which gets computationally expensive)... It's not expensive if the domain is, for instance, Bool.

You didn't make such a restriction; you wanted it for _all_ function types.

That's OK. There are lots of ways of writing computationally expensive things in Haskell. If you really want to compare two functions over Word32, using my (==) is no more computationally expensive than any other way. -- Ashley Yakeley

Joe Fredette wrote:

this is bounded, enumerable, but infinite.

The question is whether there are types like this. If so, we would need a new class: class Finite a where allValues :: [a] instance (Finite a,Eq b) => Eq (a -> b) where p == q = fmap p allValues == fmap q allValues instance (Finite a,Eq a) => Traversable (a -> b) where sequenceA afb = fmap lookup (sequenceA (fmap (\a -> fmap (b -> (a,b)) (afb a)) allValues)) where lookup :: [(a,b)] -> a -> b lookup (a,b):_ a' | a == a' = b lookup _:r a' = lookup r a' lookup [] _ = undefined instance Finite () where allValues = [()] data Nothing instance Finite Nothing where allValues = [] -- Ashley Yakeley

On Wed, 2010-04-14 at 08:13 +0100, Thomas Davie wrote:

Your instances of Finite are not quite right:

bottom :: a bottom = doSomethingToLoopInfinitely.

instance Finite () where allValues = [(), bottom]

Bottom is not a value, it's failure to evaluate to a value. But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error "ABC") vs. (error "PQR"). Obviously this is not finite. -- Ashley Yakeley

On 14 Apr 2010, at 09:01, Jonas Almström Duregård wrote:

...

But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error "ABC") vs. (error "PQR"). Obviously this is not finite.

Nor is it computable, since it must distinguish terminating programs from nonterminating ones (i.e. the halting problem).

On a side note, since "instance (Finite a, Finite b) => Finite (a -> b)" should be possible, one can even compare some higher order functions with this approach ;).

f,g :: Bool -> Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. Bob

On 14 Apr 2010, at 09:08, Jonas Almström Duregård wrote:

...

f,g :: Bool -> Int f x = 6 g x = 6

We can in Haskell compute that these two functions are equal, without solving the halting problem.

Of course, this is the nature of generally undecidable problems. They are decidable in some cases, but not in general.

Well yes, but we already knew that this was true of function equality – we can't tell in general. Bob

On 14 Apr 2010, at 09:12, Jonas Almström Duregård wrote:

...

f,g :: Bool -> Int f x = 6 g x = 6

We can in Haskell compute that these two functions are equal, without solving the halting problem.

what about these? f,g :: Bool -> Int f x = 6 g x = x `seq` 6

As pointed out on #haskell by roconnor, we apparently don't care, this is a shame... We only care that x == y => f x == g y, and x == y can't tell if _|_ == _|_. It's a shame that we can't use this to tell if two functions are equally lazy (something I would consider part of the semantics of the function). Bob

On 14 Apr 2010, at 09:35, Jonas Almström Duregård wrote:

...

...

what about these? f,g :: Bool -> Int f x = 6 g x = x `seq` 6

As pointed out on #haskell by roconnor, we apparently don't care, this is a shame... We only care that x == y => f x == g y, and x == y can't tell if _|_ == _|_.

So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem?

Yeh :( Shame, isn't it. Bob

On Wed, Apr 14, 2010 at 02:07:52AM -0700, Ashley Yakeley wrote:

...

So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem?

This is not a problem. f and g represent the same moral function, they are just implemented differently. f is smart enough to know that its argument doesn't matter, so it doesn't need to evaluate it. g waits forever trying to evaluate its function, not knowing it doesn't need it.

Hence they are distinct functions, and should not be determined to be equal by an equality instance. A compiler will not transform g into f because said distinction is important and part of the definition of a function. Not considering 'bottom' a normal value leads to all sorts of issues when trying to prove properties of a program. Just because they don't occur at run time, you can't pretend they don't exist when reasoning about the meaning of a program, any more than you can reasonably reason about haskell without taking types into account simply because types don't occur in the run-time representation. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/

On Apr 14, 2010, at 12:16 PM, Ashley Yakeley wrote:

They are distinct Haskell functions, but they represent the same moral function.

If you're willing to accept that distinct functions can represent the same "moral function", you should be willing to accept that different "bottoms" represent the same "moral value". You're quantifying over equivalence classes either way. And one of them is much simpler conceptually.

On Apr 14, 2010, at 1:24 PM, Ashley Yakeley wrote:

Bottoms should not be considered values. They are failures to calculate values, because your calculation would never terminate (or similar condition).

And yet you are trying to recover the semantics of comparing bottoms.

On Wed, 14 Apr 2010, Ashley Yakeley wrote:

On 2010-04-14 13:03, Alexander Solla wrote:

...

If you're willing to accept that distinct functions can represent the same "moral function", you should be willing to accept that different "bottoms" represent the same "moral value".

Bottoms should not be considered values. They are failures to calculate values, because your calculation would never terminate (or similar condition).

Let's not get muddled too much in semantics here. There is some notion of value, let's call it proper value, such that bottom is not one. In other words bottom is not a proper value. Define a proper value to be a value x such that x == x. So neither undefined nor (0.0/0.0) are proper values In fact proper values are not just subsets of values but are also quotients. thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

On 2010-04-14 14:58, Ashley Yakeley wrote:

On 2010-04-14 13:59, roconnor@theorem.ca wrote:

...

There is some notion of value, let's call it proper value, such that bottom is not one.

In other words bottom is not a proper value.

Define a proper value to be a value x such that x == x.

So neither undefined nor (0.0/0.0) are proper values

In fact proper values are not just subsets of values but are also quotients.

thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values.

The trouble is, there are functions that can distinguish -0.0 and 0.0. Do we call them bad functions, or are the Eq instances for Float and Double broken?

Worse, this rules out values of types that are not Eq. -- Ashley Yakeley

On Wed, 14 Apr 2010, Ashley Yakeley wrote:

On 2010-04-14 14:58, Ashley Yakeley wrote:

...

On 2010-04-14 13:59, roconnor@theorem.ca wrote:

...

There is some notion of value, let's call it proper value, such that bottom is not one.

In other words bottom is not a proper value.

Define a proper value to be a value x such that x == x.

So neither undefined nor (0.0/0.0) are proper values

In fact proper values are not just subsets of values but are also quotients.

thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values.

The trouble is, there are functions that can distinguish -0.0 and 0.0. Do we call them bad functions, or are the Eq instances for Float and Double broken?

I'd call them disrespectful functions, or maybe nowadays I might call them improper functions. The "good" functions are respectful functions or proper functions. Proper functions are functions that are proper values i.e. f == f which is defined to mean that (x == y) ==> f x == f y (even if this isn't a decidable relation).

Worse, this rules out values of types that are not Eq.

Hmm, I guess I'm carrying all this over from the world of dependently typed programming where we have setoids and the like that admit equality relations that are not necessarily decidable. In Haskell only the decidable instances of equality manage to have a Eq instance. The other data types one has an (partial) equivalence relation in mind but it goes unwritten. But in my dependently typed world we don't have partial values so there are no bottoms to worry about; maybe these ideas don't carry over perfectly. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

On 03:53 Thu 15 Apr , roconnor@theorem.ca wrote:

On Wed, 14 Apr 2010, Ashley Yakeley wrote:

...

On 2010-04-14 14:58, Ashley Yakeley wrote:

...

On 2010-04-14 13:59, roconnor@theorem.ca wrote:

...

There is some notion of value, let's call it proper value, such that bottom is not one.

In other words bottom is not a proper value.

Define a proper value to be a value x such that x == x.

So neither undefined nor (0.0/0.0) are proper values

In fact proper values are not just subsets of values but are also quotients.

thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values.

The trouble is, there are functions that can distinguish -0.0 and 0.0. Do we call them bad functions, or are the Eq instances for Float and Double broken?

I'd call them disrespectful functions, or maybe nowadays I might call them improper functions. The "good" functions are respectful functions or proper functions.

<snip from other post>

Try using the (x == y) ==> (f x = g y) test yourself.

Your definitions seem very strange, because according to this, the functions f :: Double -> Double f x = 1/x and g :: Double -> Double g x = 1/x are not equal, since (-0.0 == 0.0) yet f (-0.0) /= g (0.0). -- Nick Bowler, Elliptic Technologies (http://www.elliptictech.com/)

Ashley Yakeley writes:

There's an impedance mismatch between the IEEE notion of equality (under which -0.0 == 0.0), and the Haskell notion of equality (where we'd want x == y to imply f x == f y).

Do we also want to modify equality for lazy bytestrings, where equality is currently independent of chunk segmentation? (I.e. toChunks s1 == toChunks s2 ==> s1 == s2 but not vice versa.) My preference would be to keep Eq as it is, a rough approximation of an intuitive notion of equality. -k -- If I haven't seen further, it is by standing in the footprints of giants

Because it is the most utilitarian way to get a bunch of strict ByteStrings out of a lazy one. Yes it exposes an implementation detail, but the alternatives involve an unnatural amount of copying. -Edward Kmett On Sat, Apr 17, 2010 at 6:37 PM, Ashley Yakeley wrote:

Ketil Malde wrote:

...

Do we also want to modify equality for lazy bytestrings, where equality is currently independent of chunk segmentation? (I.e.

toChunks s1 == toChunks s2 ==> s1 == s2 but not vice versa.)

Why is toChunks exposed?

-- Ashley Yakeley

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I don't mind the 0.0 == -0.0 case, its the NaN /= NaN one that gets me. ;) The former just says that the equivalence relation you are using isn't structural. The latter breaks the notion that you have an equivalence relation by breaking reflexivity. Eq doesn't state anywhere that the instances should be structural, though in general where possible it is a good idea, since you don't have to worry about whether or not functions respect your choice of setoid. Ultimately, I find myself having to play a bit unsafe with lazy bytestrings more often than I'd like to admit. Use of toChunks should always be careful to be safe to work regardless of the size of the chunks exposed, and can also rely on the extra-logical fact enforced by the bytestring internals that each such chunk is non-empty. It greatly facilitates 'lifting' algorithms that work over strict bytestrings to work over their lazy kin, and its omission would deal a terrible blow to the practical usability and efficiency of the bytestring library. I frankly would be forced to reimplement them from scratch in several packages were it gone. Ultimately, almost any libraries relies on a contract that extends beyond the level of the type system to ensure they are used them correctly. A malformed 'Ord' instance can wreak havoc with Set, a non-associative 'Monoid' can leak structural information out of a FingerTree. Similarly, the pleasant fiction that x == y ==> f x == f y -- only holds if the Eq instance is structural, and toChunks can only 'safely' be used in a manner that is oblivious to the structural partitioning of the lazy bytestring. -Edward Kmett On Mon, Apr 19, 2010 at 6:02 PM, Ashley Yakeley wrote:

Why is a function that gets a bunch of strict ByteStrings out of a lazy one exposed?

In any case, it sounds like a similar situation to (==) on Float and Double. There's a mismatch between the "Haskellish" desire for a law on (==), and the "convenient" desire for -0.0 == 0.0, or for exposing toChunks. Which one you prefer depends on your attitude. My point is not so much to advocate for the Haskellish viewpoint than to recognise the tension in the design. Float and Double are pretty ugly anyway from a Haskell point of view, since they break a bunch of other desirable properties for (+), (-) and so on.

The theoretical reason for using floating point rather than fixed point is when one needs relative precision over a range of scales: for other needs one should use fixed point or rationals. I added a Fixed type to base, but it doesn't implement the functions in the Floating class and I doubt it's as fast as Double for common arithmetic functions.

It would be possible to represent the IEEE types in a Haskellish way, properly revealing all their ugliness. This would be gratifying for us purists, but would annoy those just trying to get some numeric calculations done.

-- Ashley Yakeley

On Mon, 2010-04-19 at 15:32 -0400, Edward Kmett wrote:

Because it is the most utilitarian way to get a bunch of strict ByteStrings out of a lazy one.

Yes it exposes an implementation detail, but the alternatives involve an unnatural amount of copying.

-Edward Kmett

On Sat, Apr 17, 2010 at 6:37 PM, Ashley Yakeley wrote:

Ketil Malde wrote:

Do we also want to modify equality for lazy bytestrings, where equality is currently independent of chunk segmentation? (I.e.

toChunks s1 == toChunks s2 ==> s1 == s2 but not vice versa.)

Why is toChunks exposed?

-- Ashley Yakeley

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing listHaskell-Cafe@haskell.orghttp://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Apr 21, 2010 at 5:25 AM, Max Rabkin wrote:

On Wed, Apr 21, 2010 at 1:44 AM, Edward Kmett wrote:

...

Eq doesn't state anywhere that the instances should be structural, though in general where possible it is a good idea, since you don't have to worry about whether or not functions respect your choice of setoid.

Wikipedia's definition of structural equality is an object-oriented one, but if by structural equality you mean the natural equality on algebraic datatypes (as derived automatically), I don't believe this is quite the case. If the type is abstract, surely the Eq instance need only be a quotient w.r.t. the operations defined on it. Thus, for example, two Sets can be considered equal if they contain the same elements, rather than having identical tree shapes (except that Data.Set exports unsafe functions, like mapMonotonic which has an unchecked precondition).

Yes. My point about why falling back on structural equality is a good idea when possible, is that then you don't have to work so hard to make sure that x == y => f x == f y holds. When your equality instance isn't structural you need to effectively prove a theorem every time you work with the structure to avoid violating preconceptions. My post was acknowledging the expedience of such methods. I think we are using a lot of words to agree with one another. ;) -Edward Kmett

--Max

On Wed, 2010-04-14 at 12:16 -0700, Ashley Yakeley wrote:

...

On Wed, Apr 14, 2010 at 02:07:52AM -0700, Ashley Yakeley wrote:

...

...

So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem?

This is not a problem. f and g represent the same moral function,

On 2010-04-14 11:12, John Meacham wrote: they

...

...

are just implemented differently. f is smart enough to know that its argument doesn't matter, so it doesn't need to evaluate it. g waits forever trying to evaluate its function, not knowing it doesn't need it.

Hence they are distinct functions,

They are distinct Haskell functions, but they represent the same moral function.

Are f 0 = 1 f n = f (n - 1) + f (n - 2) and g 0 = 1 g n | n > 0 = g (n - 1) + g (n - 2) | n < 0 = g (n + 2) - g (n + 1) The same (morally) function? Are: f x = 2*x and f x = undefined The same function

On 14 Apr 2010, at 08:29, Ashley Yakeley wrote:

On Wed, 2010-04-14 at 08:13 +0100, Thomas Davie wrote:

...

Your instances of Finite are not quite right:

bottom :: a bottom = doSomethingToLoopInfinitely.

instance Finite () where allValues = [(), bottom]

Bottom is not a value, it's failure to evaluate to a value.

But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error "ABC") vs. (error "PQR"). Obviously this is not finite.

Certainly bottom is a value, and it's a value in *all* Haskell types. Of note, bottom is very important to this question – two functions are not equal unless their behaviour when handed bottom is equal. We also don't need to distinguish different bottoms, there is only one bottom value, the runtime has different side effects when it occurs at different times though. Bob

On 14 Apr 2010, at 09:17, Ashley Yakeley wrote:

Thomas Davie wrote:

...

Certainly bottom is a value, and it's a value in *all* Haskell types.

This is a matter of interpretation. If you consider bottom to be a value, then all the laws fail. For instance, (==) is supposed to be reflexive, but "undefined == undefined" is not True for almost any type.

For this reason I recommend "fast and loose reasoning": http://www.cs.nott.ac.uk/~nad/publications/danielsson-et-al-popl2006.html

It might be nice to have a definition of whether we consider bottom to be a value in Haskell then, because the definition of second and fmap on tuples are different because of this consideration: fmap f (x,y) = (x,f y) second f ~(x,y) = (x,f y) Because we consider that the Functor laws must hold for all values in the type (including bottom). Bob

On 14 Apr 2010, at 09:25, Ashley Yakeley wrote:

Thomas Davie wrote:

...

Because we consider that the Functor laws must hold for all values in the type (including bottom).

This is not so for IO, which is an instance of Functor. "fmap id undefined" is not bottom.

It isn't? fPrelude> fmap id (undefined :: IO ()) *** Exception: Prelude.undefined Bob

On 14 Apr 2010, at 09:31, Ashley Yakeley wrote:

On Wed, 2010-04-14 at 09:29 +0100, Thomas Davie wrote:

...

It isn't?

fPrelude> fmap id (undefined :: IO ()) *** Exception: Prelude.undefined

ghci is helpfully running the IO action for you. Try this:

seq (fmap id (undefined :: IO ())) "not bottom"

Ah, rubbish... I guess this further reinforces my point though – we have a mixture of places where we consider _|_ when considering laws, and places where we don't consider _|_. This surely needs better defined somewhere. For reference, the fmap on tuples which ignores the bottom case for the sake of the laws is useful :(. Bob

On 14 Apr 2010, at 09:39, Ashley Yakeley wrote:

Thomas Davie wrote:

...

I guess this further reinforces my point though – we have a mixture of places where we consider _|_ when considering laws, and places where we don't consider _|_. This surely needs better defined somewhere.

It's easy: don't consider bottom as a value, and the laws work fine.

If it were this easy, then why is our instance of Functor on tuples gimped? Bob

On Wed, 14 Apr 2010, Ashley Yakeley wrote:

Joe Fredette wrote:

...

this is bounded, enumerable, but infinite.

The question is whether there are types like this. If so, we would need a new class:

class Finite a where allValues :: [a]

instance (Finite a,Eq b) => Eq (a -> b) where p == q = fmap p allValues == fmap q allValues

As ski noted on #haskell we probably want to extend this to work on Compact types and not just Finite types instance (Compact a, Eq b) => Eq (a -> b) where ... For example (Int -> Bool) is a perfectly fine Compact set that isn't finite and (Int -> Bool) -> Int has a decidable equality in Haskell (which Oleg claims that everyone knows ;). I don't know off the top of my head what the class member for Compact should be. I'd guess it should have a member search :: (a -> Bool) -> a with the specificaiton that p (search p) = True iff p is True from some a. But I'm not sure if this is correct or not. Maybe someone know knows more than I do can claify what the member of the Compact class should be. http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer wrote:

On Wed, Apr 14, 2010 at 4:41 AM,   wrote:

...

As ski noted on #haskell we probably want to extend this to work on Compact types and not just Finite types

instance (Compact a, Eq b) => Eq (a -> b) where ...

For example (Int -> Bool) is a perfectly fine Compact set that isn't finite and (Int -> Bool) -> Int has a decidable equality in Haskell (which Oleg claims that everyone knows ;).

I don't know off the top of my head what the class member for Compact should be.  I'd guess it should have a member search :: (a -> Bool) -> a with the specificaiton that p (search p) = True iff p is True from some a. But I'm not sure if this is correct or not.  Maybe someone know knows more than I do can claify what the member of the Compact class should be.

http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/

Here is a summary of my prelude for topology-extras, which never got cool enough to publish.

-- The sierpinski space.  Two values: T and _|_ (top and bottom); aka. halting and not-halting. -- With a reliable unamb we could implement this as data Sigma = Sigma. -- Note that negation is not a computable function, so we for example split up equality and -- inequality below. data Sigma

(\/) :: Sigma -> Sigma -> Sigma   -- unamb (/\) :: Sigma -> Sigma -> Sigma   -- seq

class Discrete a where  -- equality is observable    (===) :: a -> a -> Sigma

class Hausdorff a where  -- inequality is observable    (=/=) :: a -> a -> Sigma

class Compact a where  -- universal quantifiers are computable    forevery :: (a -> Sigma) -> Sigma

class Overt a where   -- existential quantifiers are computable    forsome :: (a -> Sigma) -> Sigma

instance (Compact a, Discrete b) => Discrete (a -> b) where    f === g = forevery $ \x -> f x === g x

instance (Overt a, Hausdorff b) => Hausdorff (a -> b) where    f =/= g = forsome $ \x -> f x =/= g x

Elaborating a little, for Eq we need Discrete and Hausdorff, together with some new primitive: -- Takes x and y such that x \/ y = T and x /\ y = _|_, and returns False if x = T and True if y = T. decide :: Sigma -> Sigma -> Bool Escardo's searchable monad[1][2] from an Abstract Stone Duality perspective actually encodes compact *and* overt. (a -> Bool) -> a seems a good basis, even though it has a weird spec (it gives you an a for which the predicate returns true, but it's allowed to lie if there is no such a). (a -> Bool) -> Maybe a seems more appropriate, but it does not compose well. I am not sure how I feel about adding an instance of Eq (a -> b). All this topology stuff gets a lot more interesting and enlightening when you talk about Sigma instead of Bool, so I think any sort of Compact constraint on Eq would be a bit ad-hoc. The issues with bottom are subtle and wishywashy enough that, if I were writing the prelude, I would be wary of providing any general mechanism for comparing functions, leaving those decisions to be tailored to the specific problem at hand. On the other hand, with a good unamb (pleeeeeeeeeez?) and Sigma, I think all these definitions make perfect sense. I think the reason I feel that way is that in Sigma's very essence lies the concept of bottom, whereas with Bool sometimes we like to pretend there is no bottom and sometimes we don't. [1] On hackage: http://hackage.haskell.org/package/infinite-search [2] Article: http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-fin...

By Tychonoff's theorem we should have:

instance (Compact b) => Compact (a -> b) where    forevert p = ???

But I am not sure whether this is computable, whether (->) counts as a product topology, how it generalizes to ASD-land [1] (in which I am still a noob -- not that I am not a topology noob), etc.

Luke

[1] Abstract Stone Duality -- a formalization of computable topology. http://www.paultaylor.eu/ASD/

On Wed, 14 Apr 2010, Ashley Yakeley wrote:

On 2010-04-14 03:41, roconnor@theorem.ca wrote:

...

For example (Int -> Bool) is a perfectly fine Compact set that isn't finite

Did you mean "Integer -> Bool"? "Int -> Bool" is finite, but large.

Yes, I meant Integer -> Bool. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

I wrote:

class Compact a where

After reading Luke Palmer's message I'm thinking this might not be the best name. -- Ashley Yakeley

Ketil Malde wrote:

Another practical consideration is that checking a function taking a simple Int parameter for equality would mean 2^65 function evaluations. I think function equality would be too much of a black hole to be worth it.

Oh FFS, _don't do that_. -- Ashley Yakeley

Ketil Malde wrote:

(If you'd made clear from the start that when you say "Enum a, Bounded a" you really mean "Bool", you might have avoided these replies that you apparently find offensive.)

I don't mean Bool. There are lots of small finite types, for instance, (), Word8, Maybe Bool, and so on. They're very useful. -- Ashley Yakeley

Maciej Piechotka wrote:

I guess that the fact that: - It is costly.

No, it's not. Evaluating equality for "Bool -> Int" does not take significantly longer than for its isomorph "(Int,Int)". The latter has an Eq instance, so why doesn't the former? -- Ashley Yakeley

On Wed, Apr 14, 2010 at 2:22 PM, Stefan Monnier wrote:

While we're here, I'd be more interested in a dirty&fast comparison operation which could look like:

   eq :: a -> a -> IO Bool

where the semantics is "if (eq x y) returns True, then x and y are the same object, else they may be different".  Placing it in IO is not great since its behavior really depends on the compiler rather than on the external world, but at least it would be available.

What about something like System.Mem.StableName? Various pointer types from the FFI have Eq instances as well and could potentially be (mis)used to that end. - C.