[Haskell-cafe] Re: instance Eq (a -> b)
lrpalmer at gmail.com
Wed Apr 14 07:35:15 EDT 2010
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.
> 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 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.
 On hackage: http://hackage.haskell.org/package/infinite-search
 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  (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