module Data.Type.Boolean where
import Data.Type.Quantifier (Some(..))
import Type.Family.Bool
import Type.Family.Constraint
import Type.Class.Known
import Type.Class.Higher
data Boolean :: Bool -> * where
False_ :: Boolean False
True_ :: Boolean True
deriving instance Eq (Boolean b)
deriving instance Ord (Boolean b)
deriving instance Show (Boolean b)
instance Eq1 Boolean
instance Ord1 Boolean
instance Show1 Boolean
instance Read1 Boolean where
readsPrec1 _ s0 =
[ (Some True_,s1)
| ("True_",s1) <- lex s0
] ++
[ (Some False_,s1)
| ("False_",s1) <- lex s0
]
not' :: Boolean a -> Boolean (Not a)
not' = \case
False_ -> True_
True_ -> False_
(.||) :: Boolean a -> Boolean b -> Boolean (a || b)
(.||) = \case
False_ -> id
True_ -> const True_
infixr 2 .||
(.&&) :: Boolean a -> Boolean b -> Boolean (a && b)
(.&&) = \case
False_ -> const False_
True_ -> id
infixr 3 .&&
(.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)
a .^^ b = (a .|| b) .&& not' (a .&& b)
infixr 4 .^^
(==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)
a ==> b = not' a .|| b
infixr 1 ==>
(<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)
(<==>) = (.==)
infixr 1 <==>
class BoolEquality (f :: k -> *) where
type BoolEqC f (a :: k) (b :: k) :: Constraint
type BoolEqC f a b = ØC
(.==) :: BoolEqC f a b => f a -> f b -> Boolean (a == b)
infix 4 .==
instance BoolEquality Boolean where
(.==) = \case
False_ -> \case
False_ -> True_
True_ -> False_
True_ -> \case
False_ -> False_
True_ -> True_
instance Known Boolean True where
known = True_
instance Known Boolean False where
known = False_