Re: [Haskell-cafe] Re: instance Eq (a - b)
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 ash...@semantic.org 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)
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.
http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
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
[Haskell-cafe] Re: instance Eq (a - b)
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)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
Ashley Yakeley ash...@semantic.org 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)
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 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: instance Eq (a - b)
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 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: instance Eq (a - b)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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. snip from other post Try using the (x == y) == (f x = g y) test yourself. Your definitions seem very strange, because according to this, the functions f :: Double - Double f x = 1/x and g :: Double - Double g x = 1/x are not equal, since (-0.0 == 0.0) yet f (-0.0) /= g (0.0). -- Nick Bowler, Elliptic Technologies (http://www.elliptictech.com/) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
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
[Haskell-cafe] Re: instance Eq (a - b)
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
[Haskell-cafe] Re: instance Eq (a - b)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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)
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 ash...@semantic.org 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)
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)
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)
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)
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 tom.da...@gmail.com: 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)
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 tom.da...@gmail.com: 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)
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)
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)
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
[Haskell-cafe] Re: instance Eq (a - b)
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)
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 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)
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)
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)
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)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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 tom.da...@gmail.com: 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)
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)
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 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
[Haskell-cafe] Re: instance Eq (a - b)
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 ash...@semantic.org 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)
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)
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)
Ivan Lazar Miljenovic wrote: Ashley Yakeley ash...@semantic.org 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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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)
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 4:41 AM, 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. 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer lrpal...@gmail.com wrote: On Wed, Apr 14, 2010 at 4:41 AM, 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. 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 (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
[Haskell-cafe] Re: instance Eq (a - b)
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)
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)
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 dirtyfast 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
[Haskell-cafe] Re: instance Eq (a - b)
Stefan Monnier monn...@iro.umontreal.ca wrote: While we're here, I'd be more interested in a dirtyfast 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
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 2:22 PM, Stefan Monnier monn...@iro.umontreal.ca wrote: While we're here, I'd be more interested in a dirtyfast 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)
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 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: instance Eq (a - b)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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)
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
[Haskell-cafe] Re: instance Eq (a - b)
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)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, 14 Apr 2010, Ashley Yakeley wrote: On 2010-04-14 13:03, Alexander Solla wrote: If you're willing to accept that distinct functions can represent the same moral function, you should be willing to accept that different bottoms represent the same moral value. Bottoms should not be considered values. They are failures to calculate values, because your calculation would never terminate (or similar condition). Let's not get muddled too much in semantics here. There is some notion of value, let's call it proper value, such that bottom is not one. In other words bottom is not a proper value. Define a proper value to be a value x such that x == x. So neither undefined nor (0.0/0.0) are proper values In fact proper values are not just subsets of values but are also quotients. thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: instance Eq (a - b)
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
[Haskell-cafe] Re: instance Eq (a - b)
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
Re: [Haskell-cafe] Re: instance Eq (a - b)
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)
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
