{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances, FlexibleInstances, OverlappingInstances #-}
module Main where
import Control.Applicative (liftA,liftA2,liftA3)
import Data.List (intercalate)
import Data.Countable
import Data.Searchable
implies :: Bool -> Bool -> Bool
implies False _ = True
implies True x = x
type Set x = x -> Bool -- is it a member?
empty :: Set x
empty _ = False
full :: Set x
full _ = True
union :: Set x -> Set x -> Set x
union p q a = p a || q a
intersection :: Set x -> Set x -> Set x
intersection p q a = p a && q a
instance (Finite x,Show x) => Show (Set x) where
show s = "{" ++ (intercalate "," (fmap show (filter s allValues))) ++ "}"
-- Given a function, find the preimage of a set.
preimage :: (x -> y) -> Set y -> Set x
preimage f s a = s (f a)
type Topology x = Set (Set x) -- set of open sets
isTopology :: (Countable x) => Topology x -> Bool
isTopology top = hasEmpty && hasFull && hasIntersections && hasUnions where
hasEmpty = top empty
hasFull = top full
hasIntersections = forevery (\(p,q) -> (top p && top q) `implies` top (intersection p q))
hasUnions = forevery (\(p,q) -> (top p && top q) `implies` top (union p q))
-- Given topologies on x and y, find the set of continuous functions
continuous :: (Countable y) => Topology x -> Topology y -> Set (x -> y)
continuous topx topy f = forevery (\set -> implies (topy set) (topx (preimage f set)))
class (Finite x) => Model x where
-- definable functions in this model
definable :: Set (x -> x)
-- U1 models the unit type in a strict language
-- T1 represents the only possibility, termination with the unit value
data U1 = T1 deriving (Eq, Show)
instance Countable U1 where
countPrevious = finiteCountPrevious
countMaybeNext = finiteCountMaybeNext
instance Searchable U1 where
search = finiteSearch
instance Finite U1 where
allValues = [T1]
assemble afb = liftA (\t a -> case a of
T1 -> t
) (afb T1)
instance Model U1 where
definable f = af (f T1) where
af T1 = True -- there is only one possible function, which is definable
-- U2 represents the unit type in a lazy language with no exceptions besides non-termination
-- T2 is termination with the unit value,
-- N2 is non-termination
data U2 = T2 | N2 deriving (Eq, Show)
instance Countable U2 where
countPrevious = finiteCountPrevious
countMaybeNext = finiteCountMaybeNext
instance Searchable U2 where
search = finiteSearch
instance Finite U2 where
allValues = [T2,N2]
assemble afb = liftA2 (\t n a -> case a of
T2 -> t
N2 -> n
) (afb T2) (afb N2)
instance Model U2 where
definable f = af (f T2) (f N2) where
af T2 T2 = True -- f _ = always termination
af N2 N2 = True -- f _ = always non-termination
af T2 N2 = True -- f x = x
af N2 T2 = False -- "inversion", not definable
-- U3 represents the unit type in a lazy language with an additional "exception" possibility
-- T3 is termination with the unit value,
-- E3 is termination with the exception
-- N3 is non-termination
-- (E3 and N3 are both "bottoms")
data U3 = T3 | E3 | N3 deriving (Eq, Show)
instance Countable U3 where
countPrevious = finiteCountPrevious
countMaybeNext = finiteCountMaybeNext
instance Searchable U3 where
search = finiteSearch
instance Finite U3 where
allValues = [T3,E3,N3]
assemble afb = liftA3 (\t e n a -> case a of
T3 -> t
E3 -> e
N3 -> n
) (afb T3) (afb E3) (afb N3)
instance Model U3 where
definable f = af (f T3) (f E3) (f N3) where
-- functions that ignore the argument are definable
af t e n | n == e && n == t = True
-- otherwise, the function must not terminate when passed non-termination:
af _ _ T3 = False
af _ _ E3 = False
-- more generally, the function must return a bottom when passed a bottom:
af _ T3 _ = False
-- all other functions are definable
af _ _ _ = True
-- this topology matches if its continous functions are exactly the definable functions
matching :: (Model x) => Topology x -> Bool
matching top = (continuous top top) == definable
-- all matching topologies
goodtops :: (Model x) => [Topology x]
goodtops = filter (\top -> matching top && isTopology top) allValues
printOnLines :: (Show s) => [s] -> IO ()
printOnLines = mapM_ (putStrLn . show)
main :: IO ()
main = do
putStrLn "Topologies for U1:"
printOnLines (goodtops :: [Topology U1])
putStrLn "Topologies for U2:"
printOnLines (goodtops :: [Topology U2])
putStrLn "Topologies for U3:"
printOnLines (goodtops :: [Topology U3])