Safe Haskell	Safe-Inferred
Language	Haskell2010

Haskus.Utils.Types.Bool

Contents

Generic

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
- boolValue :: Bool
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

boolValue :: Bool Source #

Get a bool value from a Bool at type level

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

Instances

Instances details

KnownBool 'False Source #
Instance details Defined in Haskus.Utils.Types.Bool Methods boolValue :: Bool Source #
KnownBool 'True Source #
Instance details Defined in Haskus.Utils.Types.Bool Methods boolValue :: Bool Source #

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