module Control.Concurrent.Session.Bool where
infixr 1 :$
infixr 9 :.
type (:$) (a :: * -> *) b = a b
type (:.) (a :: (* -> *)) (b :: (* -> *)) (c :: *) = a (b c)
data True = TT deriving (Show)
data False = FF deriving (Show)
class And x y z | x y -> z where
tyAnd :: x -> y -> z
instance And True True True where
tyAnd TT TT = TT
instance And True False False where
tyAnd TT FF = FF
instance And False y False where
tyAnd FF _ = FF
class Or x y z | x y -> z where
tyOr :: x -> y -> z
instance Or True y True where
tyOr TT _ = TT
instance Or False True True where
tyOr FF TT = TT
instance Or False False False where
tyOr FF FF = FF
class If c x y z | c x y -> z where
tyIf :: c -> x -> y -> z
instance If True x y x where
tyIf TT x _ = x
instance If False x y y where
tyIf FF _ y = y
class Not x y | x -> y where
type NotT x
tyNot :: x -> y
instance Not True False where
type NotT True = False
tyNot TT = FF
instance Not False True where
type NotT False = True
tyNot FF = TT