Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Edward Kmett]

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 list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

I wrote:


  class Compact a where


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


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

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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] Re: instance Eq (a -> b)

[Ashley Yakeley]

rocon...@theorem.ca 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.


 


Here's a first attempt, which works when I tried comparing values of 
type ((Integer -> Bool) -> Bool). It needs some generalisation, however. 
I want to be able to write these:


  instance (Countable a,Countable b) => Countable (a,b)
  instance (Countable c,Compact b) => Compact (c -> b)

...


{-# LANGUAGE FlexibleInstances #-}
module Compact where

  import Data.List
  import Data.Maybe
  import Prelude

  class Countable a where
countPrevious :: a -> Maybe a

  countDown :: (Countable a) => a -> [a]
  countDown a = case countPrevious a of
Just a' -> a':(countDown a')
Nothing -> []

  instance Countable () where
countPrevious () = Nothing

  instance Countable Bool where
countPrevious True = Just False
countPrevious False = Nothing

  instance Countable Integer where
countPrevious 0 = Nothing
countPrevious a | a < 0 = Just (- a - 1)
countPrevious a = Just (- a)

  instance (Countable a) => Countable (Maybe a) where
countPrevious = fmap countPrevious

  class Compact a where
search :: (a -> Bool) -> Maybe a
forsome :: (a -> Bool) -> Bool
forsome = isJust . search

  forevery :: (Compact a) => (a -> Bool) -> Bool
  forevery p = not (forsome (not . p))

  instance (Compact a) => Compact (Maybe a) where
search mab = if mab Nothing
 then Just Nothing
 else fmap Just (search (mab . Just))

  prepend :: (Countable c) => b -> (c -> b) -> c -> b
  prepend b cb c = case countPrevious c of
Just c' -> cb c'
Nothing -> b

  find_i :: (Countable c) => ((c -> Bool) -> Bool) -> c -> Bool
  find_i cbb = let
b = forsome(cbb . (prepend True)) in
prepend b (find_i (cbb . (prepend b)))

  instance (Countable c) => Compact (c -> Bool) where
forsome cbb = cbb (find_i cbb)
search cbb = if forsome cbb then Just(find_i cbb) else Nothing

  instance (Compact a,Eq b) => Eq (a -> b) where
p == q = forevery (\a -> p a == q a)

  class (Compact a,Countable a) => Finite a where
allValues :: [a]

  finiteSearch :: (Finite a) => (a -> Bool) -> Maybe a
  finiteSearch p = find p allValues

  instance Compact () where
search = finiteSearch

  instance Finite () where
allValues = [()]

  instance Compact Bool where
search = finiteSearch

  instance Finite Bool where
allValues = [False,True]

  instance (Finite a) => Finite (Maybe a) where
allValues = Nothing:(fmap Just allValues)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Ketil Malde]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

On 2010-04-15 06:18, Nick Bowler wrote:


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).


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).


A Haskellish solution would be to implement Eq so that it compares the 
bits of the representations of Float and Double, thus -0.0 /= 0.0, NaN 
== NaN (if it's the same NaN). But this might surprise people expecting 
IEEE equality, which is probably almost everyone using Float or Double.


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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Alexander Solla]

On Apr 15, 2010, at 12:53 AM, rocon...@theorem.ca wrote:

I'd call them disrespectful functions, or maybe nowadays I might  
call them

improper functions.  The "good" functions are respectful functions or
proper functions.


There's no need to put these into a different class.  The IEEE defined  
this behavior in 1985, in order to help with rounding error.  Floats  
and doubles are NOT a field, let alone an ordered field.  0.0 =/= -0.0  
by design, for floats and doubles.  0.0 == -0.0 for integers, exact  
computable reals, etc.  The problem isn't the functions, or the Eq  
instance.  It's the semantics of the underlying data type -- or  
equivalently, expecting that floats and doubles form an ordered field.

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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Nick Bowler]

On 03:53 Thu 15 Apr , rocon...@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, rocon...@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.


> 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/)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

On Thu, 2010-04-15 at 03:53 -0400, rocon...@theorem.ca wrote:
> 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.

It's an interesting approach, though, since decided equality seems to
capture the idea of "full value" fairly well.

I'm currently thinking along the lines of a set V of "Platonic" values,
while Haskell names are bound to expressions that attempt to calculate
these values. At any given time during the calculation, an expression
can be modelled as a subset of V. Initially, it's V, as calculation
progresses it may become progressively smaller subsets of V.

Saying a calculation is bottom is to make a prediction that cannot in
general be decided. It's to say that the calculation will always be V.
If it ever becomes not V, it's a "partial value". If it ever becomes a
singleton, it's a "complete value".

On the other hand, this approach may not help with strict vs. non-strict
functions.

-- 
Ashley Yakeley

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

[Haskell-cafe] Re: instance Eq (a -> b)

[roconnor]

On Wed, 14 Apr 2010, Ashley Yakeley wrote:


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

On 2010-04-14 13:59, rocon...@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  
``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.''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[roconnor]

On Thu, 15 Apr 2010, Maciej Piechotka wrote:


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


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

--
Russell O'Connor  
``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.''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Maciej Piechotka]

On Wed, 2010-04-14 at 12:16 -0700, Ashley Yakeley wrote:
> On 2010-04-14 11:12, John Meacham 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,
> 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


signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Alexander Solla]

On Apr 14, 2010, at 5:10 PM, Ashley Yakeley wrote:


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


In principle, every type is an instance of Eq, because every type  
satisfies the identity function.  Unfortunately, you can't DERIVE  
instances in general.  As you are finding out...  On the other hand,  
if you're not comparing things by equality, it hardly matters that you  
haven't defined the function (==) :: (Eq a) => a -> a -> Bool for  
whatever your a is.


Put it another way:  the existence of the identity function defines --  
conceptually, not in code -- instances for Eq.  In particular, note  
that the extension of the identify function is a set of the form  
(value, value) for EVERY value in the type.  A proof that (id x) is x  
is a proof that x = x.

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

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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

On 2010-04-14 13:59, rocon...@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

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

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

On 2010-04-14 13:59, rocon...@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?


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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[roconnor]

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  
``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.''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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

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


No, I don't think so.

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

[Haskell-cafe] Re: instance Eq (a -> b)

[Alexander Solla]

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. 
 
___

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

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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).


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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Alexander Solla]

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.

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

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

On 2010-04-14 11:12, John Meacham 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, 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.



and should not be determined to be equal by an equality instance.


I don't see why not. It doesn't break the expected Eq laws of 
reflexivity, symmetry, transitivity. Also, it supports this law:


  if f == g = True, then f x == g x = True

... in exactly the same way that it supports reflexivity, that is, "fast 
and loose" ignoring bottom.



A compiler will not transform g into f
because said distinction is important and part of the definition of a
function.


I'm not seeing this implication as part of the semantics of (==).

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

[Haskell-cafe] Re: instance Eq (a -> b)

[roconnor]

On Wed, 14 Apr 2010, Ashley Yakeley wrote:


On 2010-04-14 03:41, rocon...@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  
``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.''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Casey McCann]

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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ertugrul Soeylemez]

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's "the same object"?  Functions and values have no identity in
Haskell.  The best you can do is to ask, whether the arguments refer to
the same thunk in memory (sharing), but as you say the answer isn't
portable.  It's also not much useful IMO.


Greets,
Ertugrul


-- 
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://blog.ertes.de/


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

[Haskell-cafe] Re: instance Eq (a -> b)

[Stefan Monnier]

> Why isn't there an instance Eq (a -> b) ?

I guess it's because even for those cases where it can be written, it
will rarely be what you want to do, so it's better to require the
programmer to explicitly request a function-comparison than to risk
silently using such a costly operation when the programmer intended no
such thing.

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.


Stefan

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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[John Meacham]

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/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

On 2010-04-14 03:41, rocon...@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.

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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Luke Palmer]

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.
>>
>> 
>
> 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
(pleez?) 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-finite-time/

> 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/
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Luke Palmer]

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.
>
> 

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

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/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[roconnor]

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.




--
Russell O'Connor  
``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.''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Henning Thielemann]

Ashley Yakeley schrieb:

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:
I assume that comparing functions is more oftenly a mistake then 
actually wanted. Say I have compared

f x == f y
and later I add a parameter to 'f'. Then the above expression becomes a 
function comparison. The compiler could not spot this bug but will 
silently compare functions.


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

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

Jonas Almström Duregård 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.


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

[Haskell-cafe] Re: instance Eq (a -> b)

[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ketil Malde]

Ashley Yakeley  writes:

>> 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_.

I won't.

But you are the one proposing this functionality and asking why it
isn't there already.  I thought the obvious fact that it won't work in
practice for many built in or easily constructed types might be one such
reason.

Same for Show instances for functions, of course.

(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.)

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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.

Of course, sometimes we may want to add _additional_ information 
concerning bottom, such as strictness.


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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Jonas Almström Duregård]

>> 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?

/Jonas

2010/4/14 Thomas Davie :
>
> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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"

-- 
Ashley Yakeley

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

[Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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.


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

[Haskell-cafe] Re: instance Eq (a -> b)

[Maciej Piechotka]

On Wed, 2010-04-14 at 01:21 -0700, Ashley Yakeley wrote:
> 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?
> 

Hmm. Lazy semantics? Costs?

Except technical problems with checking it - is every stable sort
equivalent?

Also see second argument.

Regards


signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Maciej Piechotka]

On Tue, 2010-04-13 at 23:03 -0700, Ashley Yakeley wrote:
> Why isn't there an instance Eq (a -> b) ?
> 
>allValues :: (Bounded a,Enum a) => [a]
>allValues = enumFrom minBound
> 
>instance (Bounded a,Enum a,Eq b) => Eq (a -> b) where
>  p == q = fmap p allValues == fmap q allValues
> 
> Of course, it's not perfect, since empty types are finite but not 
> Bounded. One can nevertheless make them instances of Bounded with 
> undefined bounds, and have enumFrom and friends always return the empty 
> list.
> 

I guess that the fact that:
- It is costly. On modern machine comparing Int -> a functions would
take 18446744073709551615 steps. Using optimistic assumption (3 GHz, 1
clock per check) it would take 185948 years. Ok - it can be parallelised
but  it would make it better by factor of 16 (which would be
monumentally offset by the fact you likely have this 16 clock cycles
spent on computation/memory access etc.).
- It is rarely needed. I had much often errors about missing Eq (a -> b)
instances when I had error then I needed it.

> It seems one should also be able to write
> 
>instance (Bounded a,Enum a) => Traversable (a -> b) where ???
> 
> But this turns out to be curiously hard.
> 

To begin with {_|_} -> R - LHS is finite (so bound and enumerable) but
there is uncountable number of such functions.

Q⋂[0,1] -> Q⋂[0,1] -Is not countable (enumerable) as well.
Q⋂[0,1] -> {0,1} - Also uncountable (due to diagonalisation argument)
IIRC

Regards



signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[Ashley Yakeley]

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

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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Jonas Almström Duregård]

> 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

/Jonas

2010/4/14 Thomas Davie :
>
> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Jonas Almström Duregård]

> 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.

/Jonas

2010/4/14 Thomas Davie :
>
> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: instance Eq (a -> b)

[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Jonas Almström Duregård]

> 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 ;).

On 14 April 2010 09: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.
>
> --
> Ashley Yakeley
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[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

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

Re: [Haskell-cafe] Re: instance Eq (a -> b)

[Thomas Davie]

Your instances of Finite are not quite right:

bottom :: a
bottom = doSomethingToLoopInfinitely.

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

instance Finite Nothing where
 allValues = [bottom]

Though at a guess an allValuesExculdingBottom function is also useful, perhaps 
the class should be

class Finite a where
 allValuesExcludingBottom :: [a]

allValues :: Finite a => [a]
allValues = (bottom:) . allValuesExcludingBottom

Bob

On 14 Apr 2010, at 08:01, 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
> 
> 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
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Haskell-cafe] Re: instance Eq (a -> b)

[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe