Contents

Description

Type level booleans

Synopsis
• type family If (c :: Bool) (t :: k) (e :: k) where ...
• type family NotB x where ...
• type family OrB x y where ...
• type family AndB x y where ...
• type family XorB x y where ...
• class KnownBool a where
• type family Not (t :: b) (f :: b) (x :: b) :: b where ...
• type family And (t :: b) (f :: b) (x :: b) (y :: b) :: b where ...
• type family Or (t :: b) (f :: b) (x :: b) (y :: b) :: b where ...
• type family Xor (t :: b) (f :: b) (x :: b) (y :: b) :: b where ...
• type family AndMany (t :: b) (f :: b) (xs :: [b]) :: b where ...
• type family OrMany (t :: b) (f :: b) (xs :: [b]) :: b where ...
• type family XorMany (t :: b) (f :: b) (xs :: [b]) :: b where ...
• type family AllFalse (t :: b) (f :: b) (xs :: [b]) :: b where ...
• type family AllTrue (t :: b) (f :: b) (xs :: [b]) :: b where ...

# Documentation

type family If (c :: Bool) (t :: k) (e :: k) where ... Source #

If-then-else

Equations

 If True t e = t If False t e = e

type family NotB x where ... Source #

Boolean Not

>>> boolValue @(NotB 'True)
False
>>> boolValue @(NotB 'False)
True


Equations

 NotB True = False NotB False = True

type family OrB x y where ... Source #

Boolean Or

>>> boolValue @(OrB 'True 'False)
True
>>> boolValue @(OrB 'False 'False)
False


Equations

 OrB True True = True OrB False True = True OrB True False = True OrB False False = False

type family AndB x y where ... Source #

Boolean And

>>> boolValue @(AndB 'True 'False)
False
>>> boolValue @(AndB 'True 'True)
True


Equations

 AndB True True = True AndB True False = False AndB False True = False AndB False False = False

type family XorB x y where ... Source #

Boolean Xor

>>> boolValue @(XorB 'True 'False)
True
>>> boolValue @(XorB 'False 'False)
False
>>> boolValue @(XorB 'True 'True)
False


Equations

 XorB True True = False XorB False True = True XorB True False = True XorB False False = False

class KnownBool a where Source #

Type-level Bool known at compile time

Methods

Get a bool value from a Bool at type level

>>> boolValue @'True
True
>>> boolValue @(AndB 'True 'False)
False

Instances
 Source # Instance detailsDefined in Haskus.Utils.Types.Bool Methods Source # Instance detailsDefined in Haskus.Utils.Types.Bool Methods

# Generic

type family Not (t :: b) (f :: b) (x :: b) :: b where ... Source #

Generic boolean Not

>>> natValue' @(Not 1 0 1 :: Nat)
0
>>> natValue' @(Not 1 0 0 :: Nat)
1


Equations

 Not t f t = f Not t f f = t

type family And (t :: b) (f :: b) (x :: b) (y :: b) :: b where ... Source #

Generic boolean And

>>> natValue' @(And 1 0 1 0 :: Nat)
0
>>> natValue' @(And 1 0 1 1 :: Nat)
1


Equations

 And t f t t = t And t f t f = f And t f f t = f And t f f f = f

type family Or (t :: b) (f :: b) (x :: b) (y :: b) :: b where ... Source #

Generic boolean Or

>>> natValue' @(Or 1 0 1 0 :: Nat)
1
>>> natValue' @(Or 1 0 0 0 :: Nat)
0


Equations

 Or t f t t = t Or t f f t = t Or t f t f = t Or t f f f = f

type family Xor (t :: b) (f :: b) (x :: b) (y :: b) :: b where ... Source #

Generic boolean Xor

>>> natValue' @(Xor 1 0 1 0 :: Nat)
1
>>> natValue' @(Xor 1 0 0 0 :: Nat)
0
>>> natValue' @(Xor 1 0 1 1 :: Nat)
0


Equations

 Xor t f t t = f Xor t f f t = t Xor t f t f = t Xor t f f f = f

type family AndMany (t :: b) (f :: b) (xs :: [b]) :: b where ... Source #

Generic boolean And on a list

>>> natValue' @(AndMany 1 0 '[1,0,1] :: Nat)
0
>>> natValue' @(AndMany 1 0 '[1,1,1] :: Nat)
1


Equations

 AndMany t f '[t] = t AndMany t f '[f] = f AndMany t f (f ': xs) = f AndMany t f (t ': xs) = AndMany t f xs

type family OrMany (t :: b) (f :: b) (xs :: [b]) :: b where ... Source #

Generic boolean Or on a list

>>> natValue' @(OrMany 1 0 '[1,0,1] :: Nat)
1
>>> natValue' @(OrMany 1 0 '[1,1,1] :: Nat)
1
>>> natValue' @(OrMany 1 0 '[0,0,0] :: Nat)
0


Equations

 OrMany t f '[t] = t OrMany t f '[f] = f OrMany t f (t ': xs) = t OrMany t f (f ': xs) = OrMany t f xs

type family XorMany (t :: b) (f :: b) (xs :: [b]) :: b where ... Source #

Generic boolean Xor on a list (i.e. check if there is a single true element in the list)

>>> natValue' @(XorMany 1 0 '[0,0,1] :: Nat)
1
>>> natValue' @(XorMany 1 0 '[1,0,1] :: Nat)
0
>>> natValue' @(XorMany 1 0 '[0,0,0] :: Nat)
0


Equations

 XorMany t f '[t] = t XorMany t f '[f] = f XorMany t f (t ': xs) = AllFalse t f xs XorMany t f (f ': xs) = XorMany t f xs

type family AllFalse (t :: b) (f :: b) (xs :: [b]) :: b where ... Source #

Check if all the elements are false

>>> natValue' @(AllFalse 1 0 '[0,0,1] :: Nat)
0
>>> natValue' @(AllFalse 1 0 '[0,0,0] :: Nat)
1


Equations

 AllFalse t f '[t] = f AllFalse t f '[f] = t AllFalse t f (t ': xs) = f AllFalse t f (f ': xs) = AllFalse t f xs

type family AllTrue (t :: b) (f :: b) (xs :: [b]) :: b where ... Source #

Check if all the elements are true

>>> natValue' @(AllTrue 1 0 '[0,0,1] :: Nat)
0
>>> natValue' @(AllTrue 1 0 '[1,1,1] :: Nat)
1


Equations

 AllTrue t f '[t] = t AllTrue t f '[f] = f AllTrue t f (f ': xs) = f AllTrue t f (t ': xs) = AllTrue t f xs