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

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

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

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

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

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

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

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

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

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

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

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

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

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