FunMaybeA.hs

{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-- Richard Bird, Thinking Functionally with Haskell.
-- Chapter 2, Exercise E:
-- Count the number of functions with type Maybe a -> Maybe a.

import Control.Exception (SomeException, catch)
import Data.Foldable (Foldable)
import Data.Maybe (fromJust)
import Data.Traversable (Traversable, traverse)
import Control.Applicative ((<$>), (<*>))

-- The strict functions by definition return bottom when given bottom.
-- So we might as well systematically pattern-match.
-- Given Nothing, a function can return either:
--   - undefined
--   - Nothing
--   - Just undefined
-- Given Just x, a function can return either:
--   - undefined
--   - Nothing
--   - Just undefined
--   - Just x
-- So there are 3 * 4 = 12 possible strict functions.

f01 :: Maybe a -> Maybe a
f01 Nothing = undefined
f01 (Just _) = undefined

f02 :: Maybe a -> Maybe a
f02 Nothing = undefined
f02 (Just _) = Nothing

f03 :: Maybe a -> Maybe a
f03 Nothing = undefined
f03 (Just _) = Just undefined

f04 :: Maybe a -> Maybe a
f04 Nothing = undefined
f04 (Just x) = Just x

f05 :: Maybe a -> Maybe a
f05 Nothing = Nothing
f05 (Just _) = undefined

f06 :: Maybe a -> Maybe a
f06 Nothing = Nothing
f06 (Just _) = Nothing

f07 :: Maybe a -> Maybe a
f07 Nothing = Nothing
f07 (Just _) = Just undefined

f08 :: Maybe a -> Maybe a
f08 Nothing = Nothing
f08 (Just x) = Just x

f09 :: Maybe a -> Maybe a
f09 Nothing = Just undefined
f09 (Just _) = undefined

f10 :: Maybe a -> Maybe a
f10 Nothing = Just undefined
f10 (Just _) = Nothing

f11 :: Maybe a -> Maybe a
f11 Nothing = Just undefined
f11 (Just _) = Just undefined

f12 :: Maybe a -> Maybe a
f12 Nothing = Just undefined
f12 (Just x) = Just x

-- The non-strict functions must always return partially-defined values.
-- Therefore, these must unconditionally return either:
--   - Nothing
--   - Just e
-- Where only (e :: a) may pattern-match on the argument.

f13 :: Maybe a -> Maybe a
f13 _ = Nothing

f14 :: Maybe a -> Maybe a
f14 _ = Just undefined

f15 :: Maybe a -> Maybe a
f15 = Just . fromJust

-- We use this to reify bottom, so we can compare
-- possibly-undefined function results.
data Lifted a = Bottom | Defined a
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

-- Reify undefined as Bottom, up to the outermost constructor.
reify :: forall a. a -> IO (Lifted a)
reify val = (return . Defined $! val) `catch` handler
  where
    handler :: SomeException -> IO (Lifted a)
    handler _ = return Bottom

-- We use this to reify bottom immediately inside the outermost constructor.
type LiftedTwice f t = Lifted (f (Lifted t))

-- Like getLifted, but dig one level deeper under the outermost constructor.
-- This is as far as we go with our (Maybe a) types.
reifyTwice :: Traversable f => f a -> IO (LiftedTwice f a)
reifyTwice ma = reify ma >>= traverse (traverse reify)

-- Natural transformations.
type f ~> g = forall a. f a -> g a

-- Reify the values of a function over a test domain.
range :: Traversable g => (f ~> g) -> [ f t ] -> IO [ LiftedTwice g t ]
range f = traverse (reifyTwice . f)

data Pair a = Pair a a

-- Compare the reified values of a pair of functions over a domain.
cmpFun :: Eq t => [ f t ] -> Pair (f ~> Maybe) -> IO Bool
cmpFun dom (Pair f g) = (==) <$> range f dom <*> range g dom

-- Given a list, generate all pairs of distinct elements.
pairs :: [a] -> [Pair a]
pairs [] = []
pairs (x:xs) = map (Pair x) xs ++ pairs xs

-- Pair each element with itself.
diag :: [a] -> [Pair a]
diag = map (\x -> Pair x x)

-- Prove that for every pair of distinct functions,
-- there is at least one point in the test domain on which the
-- two functions disagree.
unique :: Eq t => [ f t ] -> [ f ~> Maybe ] -> IO Bool
unique dom fs = not . or <$> traverse (cmpFun dom) (pairs fs)

-- Sanity check: Show that our function comparator does not trivially
-- return False always, by showing that each function is at least consistent
-- with itself on the test domain.
reflexive :: Eq t => [ f t ] -> [ f ~> Maybe ] -> IO Bool
reflexive dom fs = and <$> traverse (cmpFun dom) (diag fs)

-- The functions we wish to prove distinct.
functions :: [ Maybe ~> Maybe ]
functions = [f01,f02,f03,f04,f05,f06,f07,f08,f09,f10,f11,f12,f13,f14,f15]

-- 3 points are sufficient to show that the 15 functions are distinct.
domain :: [ Maybe () ]
domain = [ undefined, Nothing, Just () ]

main :: IO ()
main = do
  res <- (&&) <$> reflexive domain functions <*> unique domain functions
  putStrLn (if res then "Yay!" else "Boo!")