Here is a considerably longer worked example using the analogy to J, borrowing heavily from Wadler: As J, this doesn't really add any power, but perhaps when used with non-representable functors like Equivalence/Comparison you can do something more interesting. -- Used for Hilbert {-# LANGUAGE DefaultSignatures, TypeOperators #-} -- Used for Representable {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances #-} module Search where import Control.Applicative import Data.Function (on) import Data.Functor.Contravariant import GHC.Generics -- for Hilbert newtype Search f a = Search { optimum :: f a -> a } instance Contravariant f => Functor (Search f) where fmap f (Search g) = Search $ f . g . contramap f instance Contravariant f => Applicative (Search f) where pure a = Search $ \_ -> a Search fs <*> Search as = Search $ \k -> let go f = f (as (contramap f k)) in go (fs (contramap go k)) instance Contravariant f => Monad (Search f) where return a = Search $ \_ -> a Search ma >>= f = Search $ \k -> optimum (f (ma (contramap (\a -> optimum (f a) k) k))) k class Contravariant f => Union f where union :: Search f a -> Search f a -> Search f a instance Union Predicate where union (Search ma) (Search mb) = Search $ \ p -> case ma p of a | getPredicate p a -> a | otherwise -> mb p instance Ord r => Union (Op r) where union (Search ma) (Search mb) = Search $ \ f -> let a = ma f b = mb f in if getOp f a >= getOp f b then a else b both :: Union f => a -> a -> Search f a both = on union pure fromList :: Union f => [a] -> Search f a fromList = foldr1 union . map return class Contravariant f => Neg f where neg :: f a -> f a instance Neg Predicate where neg (Predicate p) = Predicate (not . p) instance Num r => Neg (Op r) where neg (Op f) = Op (negate . f) pessimum :: Neg f => Search f a -> f a -> a pessimum m p = optimum m (neg p) forsome :: Search Predicate a -> (a -> Bool) -> Bool forsome m p = p (optimum m (Predicate p)) forevery :: Search Predicate a -> (a -> Bool) -> Bool forevery m p = p (pessimum m (Predicate p)) member :: Eq a => a -> Search Predicate a -> Bool member a x = forsome x (== a) each :: (Union f, Bounded a, Enum a) => Search f a each = fromList [minBound..maxBound] bit :: Union f => Search f Bool bit = fromList [False,True] cantor :: Union f => Search f [Bool] cantor = sequence (repeat bit) least :: (Int -> Bool) -> Int least p = head [ i | i <- [0..], p i ] infixl 4 --> (-->) :: Bool -> Bool -> Bool p --> q = not p || q fan :: Eq r => ([Bool] -> r) -> Int fan f = least $ \ n -> forevery cantor $ \x -> forevery cantor $ \y -> (take n x == take n y) --> (f x == f y) -- a length check that can handle infinite lists compareLength :: [a] -> Int -> Ordering compareLength xs n = case drop (n - 1) xs of [] -> LT [_] -> EQ _ -> GT -- Now, lets leave Haskell 98 behind -- Using the new GHC generics to derive versions of Hilbert's epsilon class GHilbert t where gepsilon :: Union f => Search f (t a) class Hilbert a where -- http://en.wikipedia.org/wiki/Epsilon_calculus epsilon :: Union f => Search f a default epsilon :: (Union f, GHilbert (Rep a), Generic a) => Search f a epsilon = fmap to gepsilon instance GHilbert U1 where gepsilon = return U1 instance (GHilbert f, GHilbert g) => GHilbert (f :*: g) where gepsilon = liftA2 (:*:) gepsilon gepsilon instance (GHilbert f, GHilbert g) => GHilbert (f :+: g) where gepsilon = fmap L1 gepsilon `union` fmap R1 gepsilon instance GHilbert a => GHilbert (M1 i c a) where gepsilon = fmap M1 gepsilon instance Hilbert a => GHilbert (K1 i a) where gepsilon = fmap K1 epsilon instance Hilbert () instance (Hilbert a, Hilbert b) => Hilbert (a, b) instance (Hilbert a, Hilbert b, Hilbert c) => Hilbert (a, b, c) instance (Hilbert a, Hilbert b, Hilbert c, Hilbert d) => Hilbert (a, b, c, d) instance (Hilbert a, Hilbert b, Hilbert c, Hilbert d, Hilbert e) => Hilbert (a, b, c, d, e) instance Hilbert Bool instance Hilbert Ordering instance Hilbert a => Hilbert [a] instance Hilbert a => Hilbert (Maybe a) instance (Hilbert a, Hilbert b) => Hilbert (Either a b) instance Hilbert Char where epsilon = each instance (Union f, Hilbert a) => Hilbert (Search f a) where epsilon = fmap fromList epsilon search :: (Union f, Hilbert a) => f a -> a search = optimum epsilon find :: Hilbert a => (a -> Bool) -> a find = optimum epsilon . Predicate every :: Hilbert a => (a -> Bool) -> Bool every = forevery epsilon exists :: Hilbert a => (a -> Bool) -> Bool exists = forsome epsilon -- and MPTCs/Fundeps to define representable contravariant functors: class Contravariant f => Representable f r | f -> r where represent :: f a -> a -> r tally :: (a -> r) -> f a instance Representable (Op r) r where represent (Op f) = f tally = Op instance Representable Predicate Bool where represent (Predicate p) = p tally = Predicate supremum :: Representable f r => Search f a -> (a -> r) -> r supremum m p = p (optimum m (tally p)) infimum :: (Representable f r, Neg f) => Search f a -> (a -> r) -> r infimum m p = p (pessimum m (tally p)) A few toy examples: ghci> supremum (fromList [1..10] :: Search (Op Int) Int) id 10 ghci> find (=='a') 'a' ghci> fan (!!4) 5 ghci> find (\xs -> compareLength xs 10 == EQ && (xs !! 4) == 'a') "\NUL\NUL\NUL\NULa\NUL\NUL\NUL\NUL\NUL" -Edward