{-# LANGUAGE DataKinds #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE Safe #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeOperators #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Bool -- License : BSD-style (see the LICENSE file in the distribution) -- -- Maintainer : libraries@haskell.org -- Stability : stable -- Portability : not portable -- -- Basic operations on type-level Booleans. -- -- @since 4.7.0.0 ----------------------------------------------------------------------------- module Data.Type.Bool ( If, type (&&), type (||), Not ) where import Data.Bool -- This needs to be in base because (&&) is used in Data.Type.Equality. -- The other functions do not need to be in base, but seemed to be appropriate -- here. -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@ type family If cond tru fls where If 'True tru fls = tru If 'False tru fls = fls -- | Type-level "and" type family a && b where 'False && a = 'False 'True && a = a a && 'False = 'False a && 'True = a a && a = a infixr 3 && -- | Type-level "or" type family a || b where 'False || a = a 'True || a = 'True a || 'False = a a || 'True = 'True a || a = a infixr 2 || -- | Type-level "not". An injective type family since @4.10.0.0@. -- -- @since 4.7.0.0 type family Not a = res | res -> a where Not 'False = 'True Not 'True = 'False