[Haskell-cafe] Re: instance Eq (a -> b)
lrpalmer at gmail.com
Wed Apr 14 07:13:05 EDT 2010
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.
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.
(\/) :: 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  (in which I am
still a noob -- not that I am not a topology noob), etc.
 Abstract Stone Duality -- a formalization of computable topology.
More information about the Haskell-Cafe