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
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
