{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE GADTs #-} module Type.Data.Bool ( C(switch) , Singleton(False, True) , singleton , True , true , False , false , Not , not , (:&&:) , and , (:||:) , or , If , if_ ) where import Type.Base.Proxy (Proxy(Proxy)) import Data.Typeable (Typeable) import qualified Prelude class C bool where switch :: f False -> f True -> f bool instance C False where switch :: f False -> f True -> f False switch f False f f True _ = f False f instance C True where switch :: f False -> f True -> f True switch f False _ f True f = f True f data Singleton bool where False :: Singleton False True :: Singleton True singleton :: (C bool) => Singleton bool singleton :: Singleton bool singleton = Singleton False -> Singleton True -> Singleton bool forall bool (f :: * -> *). C bool => f False -> f True -> f bool switch Singleton False False Singleton True True data True deriving (Typeable) true :: Proxy True true :: Proxy True true = Proxy True forall a. Proxy a Proxy instance Prelude.Show True where show :: True -> String show True _ = String "True" data False deriving (Typeable) false :: Proxy False false :: Proxy False false = Proxy False forall a. Proxy a Proxy instance Prelude.Show False where show :: False -> String show False _ = String "False" type family Not x type instance Not False = True type instance Not True = False not :: Proxy x -> Proxy (Not x) not :: Proxy x -> Proxy (Not x) not Proxy x Proxy = Proxy (Not x) forall a. Proxy a Proxy type family x :&&: y type instance False :&&: _x = False type instance True :&&: x = x and :: Proxy x -> Proxy y -> Proxy (x :&&: y) and :: Proxy x -> Proxy y -> Proxy (x :&&: y) and Proxy x Proxy Proxy y Proxy = Proxy (x :&&: y) forall a. Proxy a Proxy type family x :||: y type instance True :||: _x = True type instance False :||: x = x or :: Proxy x -> Proxy y -> Proxy (x :||: y) or :: Proxy x -> Proxy y -> Proxy (x :||: y) or Proxy x Proxy Proxy y Proxy = Proxy (x :||: y) forall a. Proxy a Proxy type family If x y z type instance If True y _z = y type instance If False _y z = z if_ :: Proxy x -> Proxy y -> Proxy z -> Proxy (If x y z) if_ :: Proxy x -> Proxy y -> Proxy z -> Proxy (If x y z) if_ Proxy x Proxy Proxy y Proxy Proxy z Proxy = Proxy (If x y z) forall a. Proxy a Proxy