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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
Free forum by Nabble | Edit this page |