add Natural

List/partition.dhall

@@ -0,0 +1,31 @@
+{-|
+`partition` divides a `List` of elements into those that satisfy a predicate
+and those that do not
+-}
+let Partition
+    : Type → Type
+    = λ(a : Type) → { true : List a, false : List a }
+
+let partition
+    : ∀(a : Type) → (a → Bool) → List a → Partition a
+    = λ(a : Type) →
+      λ(f : a → Bool) →
+      λ(xs : List a) →
+        List/fold
+          a
+          xs
+          (Partition a)
+          ( λ(x : a) →
+            λ(p : Partition a) →
+              if    f x
+              then  { true = [ x ] # p.true, false = p.false }
+              else  { true = p.true, false = [ x ] # p.false }
+          )
+          { true = [] : List a, false = [] : List a }
+
+let example0 =
+        assert
+      :   partition Natural Natural/even [ 0, 1, 2, 3 ]
+        ≡ { true = [ 0, 2 ], false = [ 1, 3 ] }
+
+in  partition

Natural/build.dhall

@@ -0,0 +1,31 @@
+--| `build` is the inverse of `fold`
+let build
+    : ( ∀(natural : Type) →
+        ∀(succ : natural → natural) →
+        ∀(zero : natural) →
+          natural
+      ) →
+        Natural
+    = Natural/build
+
+let example0 =
+        assert
+      :   build
+            ( λ(natural : Type) →
+              λ(succ : natural → natural) →
+              λ(zero : natural) →
+                succ (succ (succ zero))
+            )
+        ≡ 3
+
+let example1 =
+        assert
+      :   build
+            ( λ(natural : Type) →
+              λ(succ : natural → natural) →
+              λ(zero : natural) →
+                zero
+            )
+        ≡ 0
+
+in  build

Natural/divide.dhall

@@ -0,0 +1,11 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Number/fromNatural = ../Number/fromNatural.dhall nix
+
+  let Number/divide = ../Number/divide.dhall nix
+
+  let Number/toNatural = ../Number/toNatural.dhall nix
+
+  in  λ(a : Natural) →
+      λ(b : Natural) →
+        Number/toNatural
+          (Number/divide (Number/fromNatural a) (Number/fromNatural b))

Natural/enumerate.dhall

@@ -0,0 +1,32 @@
+{-|
+Generate a list of numbers from `0` up to but not including the specified
+number
+-}
+let enumerate
+    : Natural → List Natural
+    = λ(n : Natural) →
+        List/build
+          Natural
+          ( λ(list : Type) →
+            λ(cons : Natural → list → list) →
+              List/fold
+                { index : Natural, value : {} }
+                ( List/indexed
+                    {}
+                    ( List/build
+                        {}
+                        ( λ(list : Type) →
+                          λ(cons : {} → list → list) →
+                            Natural/fold n list (cons {=})
+                        )
+                    )
+                )
+                list
+                (λ(x : { index : Natural, value : {} }) → cons x.index)
+          )
+
+let example0 = assert : enumerate 10 ≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]
+
+let example1 = assert : enumerate 0 ≡ ([] : List Natural)
+
+in  enumerate

Natural/equal.dhall

@@ -1,8 +1,5 @@
 --| `equal` checks if two Naturals are equal.
-let lessThanEqual =
+let lessThanEqual = ./lessThanEqual.dhall
-        ./lessThanEqual.dhall
-          sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
-      ? ./lessThanEqual.dhall
 
 let equal
     : Natural → Natural → Bool

Natural/even.dhall

@@ -0,0 +1,10 @@
+--| Returns `True` if a number if even and returns `False` otherwise
+let even
+    : Natural → Bool
+    = Natural/even
+
+let example0 = assert : even 3 ≡ False
+
+let example1 = assert : even 0 ≡ True
+
+in  even

Natural/fold.dhall

@@ -0,0 +1,28 @@
+{-|
+`fold` is the primitive function for consuming `Natural` numbers
+
+If you treat the number `3` as `succ (succ (succ zero))` then a `fold` just
+replaces each `succ` and `zero` with something else
+-}
+let fold
+    : Natural →
+      ∀(natural : Type) →
+      ∀(succ : natural → natural) →
+      ∀(zero : natural) →
+        natural
+    = Natural/fold
+
+let example0 = assert : fold 3 Text (λ(x : Text) → "A" ++ x) "B" ≡ "AAAB"
+
+let example1 =
+      λ(zero : Text) →
+          assert
+        :   fold 3 Text (λ(x : Text) → "A" ++ x) zero
+          ≡ "A" ++ ("A" ++ ("A" ++ zero))
+
+let example2 =
+      λ(succ : Text → Text) →
+      λ(zero : Text) →
+        assert : fold 3 Text succ zero ≡ succ (succ (succ zero))
+
+in  fold

Natural/greaterThan.dhall

@@ -0,0 +1,18 @@
+--| `greaterThan` checks if one Natural is strictly greater than another.
+let lessThan = ./lessThan.dhall
+
+let greaterThan
+    : Natural → Natural → Bool
+    = λ(x : Natural) → λ(y : Natural) → lessThan y x
+
+let example0 = assert : greaterThan 5 6 ≡ False
+
+let example1 = assert : greaterThan 5 5 ≡ False
+
+let example2 = assert : greaterThan 5 4 ≡ True
+
+let property0 = λ(n : Natural) → assert : greaterThan 0 n ≡ False
+
+let property1 = λ(n : Natural) → assert : greaterThan n n ≡ False
+
+in  greaterThan

Natural/greaterThanEqual.dhall

@@ -1,10 +1,7 @@
 {-|
 `greaterThanEqual` checks if one Natural is greater than or equal to another.
 -}
-let lessThanEqual =
+let lessThanEqual = ./lessThanEqual.dhall
-        ./lessThanEqual.dhall
-          sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
-      ? ./lessThanEqual.dhall
 
 let greaterThanEqual
     : Natural → Natural → Bool

Natural/isZero.dhall

@@ -0,0 +1,10 @@
+--| Returns `True` if a number is `0` and returns `False` otherwise
+let isZero
+    : Natural → Bool
+    = Natural/isZero
+
+let example0 = assert : isZero 2 ≡ False
+
+let example1 = assert : isZero 0 ≡ True
+
+in  isZero

Natural/lessThan.dhall

@@ -0,0 +1,20 @@
+--| `lessThan` checks if one Natural is strictly less than another.
+let greaterThanEqual = ./greaterThanEqual.dhall
+
+let Bool/not = ../Bool/not.dhall
+
+let lessThan
+    : Natural → Natural → Bool
+    = λ(x : Natural) → λ(y : Natural) → Bool/not (greaterThanEqual x y)
+
+let example0 = assert : lessThan 5 6 ≡ True
+
+let example1 = assert : lessThan 5 5 ≡ False
+
+let example2 = assert : lessThan 5 4 ≡ False
+
+let property0 = λ(n : Natural) → assert : lessThan n 0 ≡ False
+
+let property1 = λ(n : Natural) → assert : lessThan n n ≡ False
+
+in  lessThan

Natural/listMax.dhall

@@ -0,0 +1,15 @@
+λ(nix : ../NixPrelude.dhall) →
+  let max = ./max.dhall
+
+  let Optional/map = ../Optional/map.dhall nix
+
+  let listMax
+      : List Natural → Optional Natural
+      = λ(xs : List Natural) →
+          Optional/map
+            Natural
+            Natural
+            (λ(n : Natural) → List/fold Natural xs Natural max n)
+            (List/head Natural xs)
+
+  in  listMax

Natural/listMin.dhall

@@ -0,0 +1,19 @@
+λ(nix : ../NixPrelude.dhall) →
+  let min = ./min.dhall
+
+  let Optional/map = ../Optional/map.dhall nix
+
+  let listMin
+      : List Natural → Optional Natural
+      = λ(xs : List Natural) →
+          Optional/map
+            Natural
+            Natural
+            ( λ(n : Natural) →
+                if    Natural/isZero n
+                then  n
+                else  List/fold Natural xs Natural min n
+            )
+            (List/head Natural xs)
+
+  in  listMin

Natural/max.dhall

@@ -0,0 +1,16 @@
+--| `max a b` returns the larger of `a` or `b`
+let lessThanEqual = ./lessThanEqual.dhall
+
+let max
+    : Natural → Natural → Natural
+    = λ(a : Natural) → λ(b : Natural) → if lessThanEqual a b then b else a
+
+let example0 = assert : max 1 2 ≡ 2
+
+let example1 = assert : max 2 1 ≡ 2
+
+let property0 = λ(n : Natural) → assert : max n n ≡ n
+
+let property1 = λ(n : Natural) → assert : max 0 n ≡ n
+
+in  max

Natural/min.dhall

@@ -0,0 +1,14 @@
+--| `min a b` returns the smaller of `a` or `b`
+let lessThanEqual = ./lessThanEqual.dhall
+
+let min
+    : Natural → Natural → Natural
+    = λ(a : Natural) → λ(b : Natural) → if lessThanEqual a b then a else b
+
+let example0 = assert : min 1 2 ≡ 1
+
+let example1 = assert : min 2 1 ≡ 1
+
+let property0 = λ(n : Natural) → assert : min n n ≡ n
+
+in  min

Natural/odd.dhall

@@ -0,0 +1,10 @@
+--| Returns `True` if a number is odd and returns `False` otherwise
+let odd
+    : Natural → Bool
+    = Natural/odd
+
+let example0 = assert : odd 3 ≡ True
+
+let example1 = assert : odd 0 ≡ False
+
+in  odd

Natural/package.dhall

@@ -0,0 +1,26 @@
+λ(nix : ../NixPrelude.dhall) →
+  { Type = Natural
+  , build = ./build.dhall
+  , divide = ./divide.dhall nix
+  , enumerate = ./enumerate.dhall
+  , even = ./even.dhall
+  , fold = ./fold.dhall
+  , isZero = ./isZero.dhall
+  , odd = ./odd.dhall
+  , product = ./product.dhall
+  , sum = ./sum.dhall
+  , show = ./show.dhall
+  , toDouble = ./toDouble.dhall
+  , toInteger = ./toInteger.dhall
+  , lessThan = ./lessThan.dhall
+  , lessThanEqual = ./lessThanEqual.dhall
+  , equal = ./equal.dhall
+  , greaterThanEqual = ./greaterThanEqual.dhall
+  , greaterThan = ./greaterThan.dhall
+  , min = ./min.dhall
+  , max = ./max.dhall
+  , listMin = ./listMin.dhall nix
+  , listMax = ./listMax.dhall nix
+  , sort = ./sort.dhall nix
+  , subtract = ./subtract.dhall
+  }

Natural/product.dhall

@@ -0,0 +1,11 @@
+--| Multiply all the numbers in a `List`
+let product
+    : List Natural → Natural
+    = λ(xs : List Natural) →
+        List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) 1
+
+let example0 = assert : product [ 2, 3, 5 ] ≡ 30
+
+let example1 = assert : product ([] : List Natural) ≡ 1
+
+in  product

Natural/show.dhall

@@ -0,0 +1,13 @@
+{-|
+Render a `Natural` number as `Text` using the same representation as Dhall
+source code (i.e. a decimal number)
+-}
+let show
+    : Natural → Text
+    = Natural/show
+
+let example0 = assert : show 3 ≡ "3"
+
+let example1 = assert : show 0 ≡ "0"
+
+in  show

Natural/sort.dhall

@@ -0,0 +1,21 @@
+--| `sort` sorts a `List` of `Natural`s in ascending order
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ../Any/Type.dhall
+
+  let Any/toAny = ../Any/toAny.dhall nix
+
+  let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
+
+  let Any/lessThan = ../Any/lessThan.dhall nix
+
+  let coerceList =
+        λ(from : Type) →
+        λ(to : Type) →
+        λ(list : List from) →
+          Any/toTypeUnchecked (List to) (Any/toAny (List from) list)
+
+  in  λ(xs : List Natural) →
+        coerceList
+          Any
+          Natural
+          (nix.builtins.sort Any/lessThan (coerceList Natural Any xs))

Natural/subtract.dhall

@@ -0,0 +1,18 @@
+--| `subtract m n` computes `n - m`, truncating to `0` if `m > n`
+let subtract
+    : Natural → Natural → Natural
+    = Natural/subtract
+
+let example0 = assert : subtract 1 2 ≡ 1
+
+let example1 = assert : subtract 1 1 ≡ 0
+
+let example2 = assert : subtract 2 1 ≡ 0
+
+let property0 = λ(n : Natural) → assert : subtract 0 n ≡ n
+
+let property1 = λ(n : Natural) → assert : subtract n 0 ≡ 0
+
+let property2 = λ(n : Natural) → assert : subtract n n ≡ 0
+
+in  subtract

Natural/sum.dhall

@@ -0,0 +1,11 @@
+--| Add all the numbers in a `List`
+let sum
+    : List Natural → Natural
+    = λ(xs : List Natural) →
+        List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) 0
+
+let example = assert : sum [ 2, 3, 5 ] ≡ 10
+
+let example = assert : sum ([] : List Natural) ≡ 0
+
+in  sum

Natural/toDouble.dhall

@@ -0,0 +1,10 @@
+--| Convert a `Natural` number to the corresponding `Double`
+let toDouble
+    : Natural → Double
+    = λ(n : Natural) → Integer/toDouble (Natural/toInteger n)
+
+let example0 = assert : toDouble 3 ≡ 3.0
+
+let example1 = assert : toDouble 0 ≡ 0.0
+
+in  toDouble

Natural/toInteger.dhall

@@ -0,0 +1,10 @@
+--| Convert a `Natural` number to the corresponding `Integer`
+let toInteger
+    : Natural → Integer
+    = Natural/toInteger
+
+let example0 = assert : toInteger 3 ≡ +3
+
+let example1 = assert : toInteger 0 ≡ +0
+
+in  toInteger

Optional/map.dhall

@@ -0,0 +1,30 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Any = ../Any/Type.dhall
+
+  let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
+
+  let Any/equal = ../Any/equal.dhall nix
+
+  let Any/toAny = ../Any/toAny.dhall nix
+
+  let null = Any/toAny (Optional Any) (None Any)
+
+  let isNone =
+        λ(t : Type) →
+        λ(o : Optional t) →
+          Any/equal (Any/toAny (Optional t) o) null
+
+  let unwrapUnsafe =
+        λ(t : Type) →
+        λ(o : Optional t) →
+          Any/toTypeUnchecked t (Any/toAny (Optional t) o)
+
+  let map
+      : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b
+      = λ(a : Type) →
+        λ(b : Type) →
+        λ(f : a → b) →
+        λ(o : Optional a) →
+          if isNone a o then None b else Some (f (unwrapUnsafe a o))
+
+  in  map

package.dhall

@@ -6,6 +6,7 @@
   , Integer = ./Integer/package.dhall nix
   , Misc = ./Misc/package.dhall nix
   , Monoid = ./Monoid.dhall
+  , Natural = ./Natural/package.dhall nix
   , Number = ./Number/package.dhall nix
   , Path = ./Path/package.dhall nix
   , Set = ./Set/package.dhall nix