{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module TypeLevel.Boolean ( True
, False
, Not
, notT
, And
, andT
, Or
, orT
, Xor
, xorT
) where
import TypeLevel.Reify
data True
data False
instance Show False where show :: False -> String
show False
_ = String
"False"
instance Show True where show :: True -> String
show True
_ = String
"True"
instance Reify True Bool where witness :: Witness True Bool
witness = Bool -> Witness True Bool
forall t a. a -> Witness t a
Witness Bool
True
instance Reify False Bool where witness :: Witness False Bool
witness = Bool -> Witness False Bool
forall t a. a -> Witness t a
Witness Bool
False
type family Not a :: *
notT :: a -> Not a
notT :: a -> Not a
notT a
_ = Not a
forall a. HasCallStack => a
undefined
type instance Not False = True
type instance Not True = False
type family And a b :: *
andT :: a -> b -> And a b
andT :: a -> b -> And a b
andT a
_ b
_ = And a b
forall a. HasCallStack => a
undefined
type instance And False False = False
type instance And False True = False
type instance And True False = False
type instance And True True = True
type family Or a b :: *
orT :: a -> b -> Or a b
orT :: a -> b -> Or a b
orT a
_ b
_ = Or a b
forall a. HasCallStack => a
undefined
type instance Or False False = True
type instance Or False True = True
type instance Or True False = True
type instance Or True True = False
type family Xor a b :: *
xorT :: a -> b -> Xor a b
xorT :: a -> b -> Xor a b
xorT a
_ b
_ = Xor a b
forall a. HasCallStack => a
undefined
type instance Xor False False = False
type instance Xor False True = True
type instance Xor True False = True
type instance Xor True True = False