{-# 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])