On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer <lrpal...@gmail.com> wrote: > On Wed, Apr 14, 2010 at 4:41 AM, <rocon...@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/ > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
