diff --git a/Bool/and.dhall b/Bool/and.dhall new file mode 100644 index 0000000..6b4e35c --- /dev/null +++ b/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 diff --git a/Bool/build.dhall b/Bool/build.dhall new file mode 100644 index 0000000..03f3c81 --- /dev/null +++ b/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 diff --git a/Bool/even.dhall b/Bool/even.dhall new file mode 100644 index 0000000..9f5515e --- /dev/null +++ b/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 diff --git a/Bool/fold.dhall b/Bool/fold.dhall new file mode 100644 index 0000000..5bfcfbf --- /dev/null +++ b/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 diff --git a/Bool/fromAny.dhall b/Bool/fromAny.dhall new file mode 100644 index 0000000..c22ca9e --- /dev/null +++ b/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" diff --git a/Bool/not.dhall b/Bool/not.dhall new file mode 100644 index 0000000..3d58e9e --- /dev/null +++ b/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 diff --git a/Bool/odd.dhall b/Bool/odd.dhall new file mode 100644 index 0000000..2c0d1d9 --- /dev/null +++ b/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 diff --git a/Bool/or.dhall b/Bool/or.dhall new file mode 100644 index 0000000..6f1642c --- /dev/null +++ b/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 diff --git a/Bool/package.dhall b/Bool/package.dhall new file mode 100644 index 0000000..883ac99 --- /dev/null +++ b/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 + } diff --git a/Bool/show.dhall b/Bool/show.dhall new file mode 100644 index 0000000..434001e --- /dev/null +++ b/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 diff --git a/Misc/package.dhall b/Misc/package.dhall new file mode 100644 index 0000000..c0afb3d --- /dev/null +++ b/Misc/package.dhall @@ -0,0 +1 @@ +λ(nix : ../NixPrelude.dhall) → { throw = ./throw.dhall nix } diff --git a/Misc/throw.dhall b/Misc/throw.dhall new file mode 100644 index 0000000..b068e45 --- /dev/null +++ b/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) diff --git a/Monoid.dhall b/Monoid.dhall new file mode 100644 index 0000000..e52d8f1 --- /dev/null +++ b/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 diff --git a/package.dhall b/package.dhall index a4636e4..f63d79e 100644 --- a/package.dhall +++ b/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