{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE EmptyDataDecls        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module TypeLevel.Boolean ( True
                     , False
                       -- * Boolean operations
                     , Not
                     , notT
                     , And
                     , andT
                     , Or
                     , orT
                     , Xor
                     , xorT
                     ) where

import TypeLevel.Reify

-- | Data type for truth
data True
-- | Data type for false.
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

----------------------------------------------------------------
-- | Negation

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

----------------------------------------------------------------
-- | And for boolean types
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

----------------------------------------------------------------
-- | Or for boolean types
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

----------------------------------------------------------------
-- | Exlusive or for boolean types
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