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

[roconnor at theorem.ca]

On Wed, 14 Apr 2010, Ashley Yakeley wrote:

> On 2010-04-14 14:58, Ashley Yakeley wrote:
>> On 2010-04-14 13:59, roconnor at 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.''