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

[Luke Palmer]

On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer <lrpalmer at gmail.com> wrote:
> On Wed, Apr 14, 2010 at 4:41 AM,  <roconnor at 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
(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/
>