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

[Ashley Yakeley]

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