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

[Luke Palmer]

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

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/