haskus-utils-types-1.5: Haskus types utility modules

Safe HaskellSafe
LanguageHaskell2010

Haskus.Utils.Types.Bool

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

type family AndB x y where ... Source #

Boolean And

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

type family XorB x y where ... Source #

Boolean Xor

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

class KnownBool a where Source #

Type-level Bool known at compile time

Methods

boolValue :: Bool Source #

Get a bool value from a Bool at type level

>>> boolValue @'True
True
>>> boolValue @(AndB 'True 'False)
False
Instances
KnownBool False Source # 
Instance details

Defined in Haskus.Utils.Types.Bool

KnownBool True Source # 
Instance details

Defined in Haskus.Utils.Types.Bool

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