
roconnor@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's a first attempt, which works when I tried comparing values of type ((Integer -> Bool) -> Bool). It needs some generalisation, however. I want to be able to write these: instance (Countable a,Countable b) => Countable (a,b) instance (Countable c,Compact b) => Compact (c -> b) ... {-# LANGUAGE FlexibleInstances #-} module Compact where import Data.List import Data.Maybe import Prelude class Countable a where countPrevious :: a -> Maybe a countDown :: (Countable a) => a -> [a] countDown a = case countPrevious a of Just a' -> a':(countDown a') Nothing -> [] instance Countable () where countPrevious () = Nothing instance Countable Bool where countPrevious True = Just False countPrevious False = Nothing instance Countable Integer where countPrevious 0 = Nothing countPrevious a | a < 0 = Just (- a - 1) countPrevious a = Just (- a) instance (Countable a) => Countable (Maybe a) where countPrevious = fmap countPrevious class Compact a where search :: (a -> Bool) -> Maybe a forsome :: (a -> Bool) -> Bool forsome = isJust . search forevery :: (Compact a) => (a -> Bool) -> Bool forevery p = not (forsome (not . p)) instance (Compact a) => Compact (Maybe a) where search mab = if mab Nothing then Just Nothing else fmap Just (search (mab . Just)) prepend :: (Countable c) => b -> (c -> b) -> c -> b prepend b cb c = case countPrevious c of Just c' -> cb c' Nothing -> b find_i :: (Countable c) => ((c -> Bool) -> Bool) -> c -> Bool find_i cbb = let b = forsome(cbb . (prepend True)) in prepend b (find_i (cbb . (prepend b))) instance (Countable c) => Compact (c -> Bool) where forsome cbb = cbb (find_i cbb) search cbb = if forsome cbb then Just(find_i cbb) else Nothing instance (Compact a,Eq b) => Eq (a -> b) where p == q = forevery (\a -> p a == q a) class (Compact a,Countable a) => Finite a where allValues :: [a] finiteSearch :: (Finite a) => (a -> Bool) -> Maybe a finiteSearch p = find p allValues instance Compact () where search = finiteSearch instance Finite () where allValues = [()] instance Compact Bool where search = finiteSearch instance Finite Bool where allValues = [False,True] instance (Finite a) => Finite (Maybe a) where allValues = Nothing:(fmap Just allValues)