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

On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer wrote:

On Wed, Apr 14, 2010 at 4:41 AM,   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-fin...

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/