Add Bool/

Bool/and.dhall

@@ -0,0 +1,14 @@
+{-|
+The `and` function returns `False` if there are any `False` elements in the
+`List` and returns `True` otherwise
+-}
+let and
+    : List Bool → Bool
+    = λ(xs : List Bool) →
+        List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True
+
+let example0 = assert : and [ True, False, True ] ≡ False
+
+let example1 = assert : and ([] : List Bool) ≡ True
+
+in  and

Bool/build.dhall

@@ -0,0 +1,16 @@
+--| `build` is the inverse of `fold`
+let build
+    : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool
+    = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) →
+        f Bool True False
+
+let example0 =
+        assert
+      : build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) ≡ True
+
+let example1 =
+        assert
+      :   build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)
+        ≡ False
+
+in  build

Bool/even.dhall

@@ -0,0 +1,20 @@
+{-|
+Returns `True` if there are an even number of `False` elements in the list and
+returns `False` otherwise.
+
+This function is the `Monoid` for the `==` operation.
+-}
+let even
+    : List Bool → Bool
+    = λ(xs : List Bool) →
+        List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True
+
+let example0 = assert : even [ False, True, False ] ≡ True
+
+let example1 = assert : even [ False, True ] ≡ False
+
+let example2 = assert : even [ False ] ≡ False
+
+let example3 = assert : even ([] : List Bool) ≡ True
+
+in  even

Bool/fold.dhall

@@ -0,0 +1,14 @@
+--| `fold` is essentially the same as `if`/`then`/`else` except as a function
+let fold
+    : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
+    = λ(b : Bool) →
+      λ(bool : Type) →
+      λ(true : bool) →
+      λ(false : bool) →
+        if b then true else false
+
+let example0 = assert : fold True Natural 0 1 ≡ 0
+
+let example1 = assert : fold False Natural 0 1 ≡ 1
+
+in  fold

Bool/fromAny.dhall

@@ -0,0 +1,11 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ../Any/Type.dhall
+
+  let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
+
+  let Misc/throw = ../Misc/throw.dhall nix
+
+  in  λ(v : Any) →
+        if    nix.builtins.isBool v
+        then  Any/toTypeUnchecked Bool v
+        else  Misc/throw Bool "Failed to coerce object into Bool"

Bool/not.dhall

@@ -0,0 +1,10 @@
+--| Flip the value of a `Bool`
+let not
+    : Bool → Bool
+    = λ(b : Bool) → b == False
+
+let example0 = assert : not True ≡ False
+
+let example1 = assert : not False ≡ True
+
+in  not

Bool/odd.dhall

@@ -0,0 +1,20 @@
+{-|
+Returns `True` if there are an odd number of `True` elements in the list and
+returns `False` otherwise.
+
+This function is the `Monoid` for the `!=` operation.
+-}
+let odd
+    : List Bool → Bool
+    = λ(xs : List Bool) →
+        List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False
+
+let example0 = assert : odd [ True, False, True ] ≡ False
+
+let example1 = assert : odd [ True, False ] ≡ True
+
+let example2 = assert : odd [ True ] ≡ True
+
+let example3 = assert : odd ([] : List Bool) ≡ False
+
+in  odd

Bool/or.dhall

@@ -0,0 +1,14 @@
+{-|
+The `or` function returns `True` if there are any `True` elements in the `List`
+and returns `False` otherwise
+-}
+let or
+    : List Bool → Bool
+    = λ(xs : List Bool) →
+        List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False
+
+let example0 = assert : or [ True, False, True ] ≡ True
+
+let example1 = assert : or ([] : List Bool) ≡ False
+
+in  or

Bool/package.dhall

@@ -0,0 +1,12 @@
+λ(nix : ../NixPrelude.dhall) →
+  { Type = Bool
+  , and = ./and.dhall
+  , build = ./build.dhall
+  , even = ./even.dhall
+  , fold = ./fold.dhall
+  , fromAny = ./fromAny.dhall nix
+  , not = ./not.dhall
+  , odd = ./odd.dhall
+  , or = ./or.dhall
+  , show = ./show.dhall
+  }

Bool/show.dhall

@@ -0,0 +1,13 @@
+{-|
+Render a `Bool` as `Text` using the same representation as Dhall source code
+(i.e. beginning with a capital letter)
+-}
+let show
+    : Bool → Text
+    = λ(b : Bool) → if b then "True" else "False"
+
+let example0 = assert : show True ≡ "True"
+
+let example1 = assert : show False ≡ "False"
+
+in  show

Misc/package.dhall

@@ -0,0 +1 @@
+λ(nix : ../NixPrelude.dhall) → { throw = ./throw.dhall nix }

Misc/throw.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
+
+  in  λ(t : Type) →
+      λ(message : Text) →
+        Any/toTypeUnchecked t (nix.builtins.throw message)

Monoid.dhall

@@ -0,0 +1,43 @@
+{-|
+Any function `f` that is a `Monoid` must satisfy the following law:
+
+```
+t  : Type
+f  : ./Monoid t
+xs : List (List t)
+
+f (./List/concat t xs) = f (./map (List t) t f xs)
+```
+
+Examples:
+
+```
+./Bool/and
+    : ./Monoid Bool
+./Bool/or
+    : ./Monoid Bool
+./Bool/even
+    : ./Monoid Bool
+./Bool/odd
+    : ./Monoid Bool
+./List/concat
+    : ∀(a : Type) → ./Monoid (List a)
+./List/shifted
+    : ∀(a : Type) → ./Monoid (List { index : Natural, value : a })
+./Natural/sum
+    : ./Monoid Natural
+./Natural/product
+    : ./Monoid Natural
+./Optional/head
+    : ∀(a : Type) → ./Monoid (Optional a)
+./Optional/last
+    : ∀(a : Type) → ./Monoid (Optional a)
+./Text/concat
+    : ./Monoid Text
+```
+-}
+let Monoid
+    : ∀(m : Type) → Type
+    = λ(m : Type) → List m → m
+
+in  Monoid

package.dhall

@@ -1,5 +1,8 @@
 λ(nix : ./NixPrelude.dhall) →
   { Any = ./Any/package.dhall nix
+  , Bool = ./Bool/package.dhall nix
+  , Misc = ./Misc/package.dhall nix
+  , Monoid = ./Monoid.dhall
   , Number = ./Number/package.dhall nix
   , Path = ./Path/package.dhall nix
   , Set = ./Set/package.dhall nix