instance Eq (a -> b)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
70 messages Options
1234
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
In reply to this post by Thomas Davie
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Jonas Almström Duregård
In reply to this post by Thomas Davie
>> 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 <[hidden email]>:

>
> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Thomas Davie
In reply to this post by Ashley Yakeley

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Thomas Davie
In reply to this post by Jonas Almström Duregård

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
In reply to this post by Thomas Davie
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ketil Malde-5
In reply to this post by Ashley Yakeley
Ashley Yakeley <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ivan Lazar Miljenovic
In reply to this post by Ashley Yakeley
Ashley Yakeley <[hidden email]> 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.


--
Ivan Lazar Miljenovic
[hidden email]
IvanMiljenovic.wordpress.com
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
In reply to this post by Jonas Almström Duregård
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
In reply to this post by Ivan Lazar Miljenovic
Ivan Lazar Miljenovic wrote:
> Ashley Yakeley <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Henning Thielemann-4
In reply to this post by Ashley Yakeley
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

roconnor
In reply to this post by Ashley Yakeley
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.''
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Luke Palmer-2
On Wed, Apr 14, 2010 at 4:41 AM,  <[hidden email]> 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

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Luke Palmer-2
On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer <[hidden email]> wrote:

> On Wed, Apr 14, 2010 at 4:41 AM,  <[hidden email]> 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-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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
In reply to this post by roconnor
On 2010-04-14 03:41, [hidden email] 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
1234