add Integer

Double/package.dhall

@@ -18,4 +18,5 @@
   , show = ./show.dhall
   , subtract = ./subtract.dhall nix
   , toInteger = ./toInteger.dhall nix
+  , toNatural = ./toNatural.dhall nix
   }

Double/toNatural.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Number/fromDouble = ../Number/fromDouble.dhall nix
+
+  let Number/toNatural = ../Number/toNatural.dhall nix
+
+  in  λ(a : Double) → Number/toNatural (Number/fromDouble a)

Function/compose.dhall

@@ -0,0 +1,17 @@
+--| Compose two functions into one.
+let compose
+    : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
+    = λ(A : Type) →
+      λ(B : Type) →
+      λ(C : Type) →
+      λ(f : A → B) →
+      λ(g : B → C) →
+      λ(x : A) →
+        g (f x)
+
+let example0 =
+        assert
+      :   compose Natural Natural Bool (λ(n : Natural) → n + n) Natural/even 3
+        ≡ True
+
+in  compose

Function/identity.dhall

@@ -0,0 +1,10 @@
+--| The identity function simply returns its input
+let identity
+    : ∀(a : Type) → ∀(x : a) → a
+    = λ(a : Type) → λ(x : a) → x
+
+let example0 = assert : identity Natural 1 ≡ 1
+
+let example1 = assert : identity Bool ≡ (λ(x : Bool) → x)
+
+in  identity

Function/package.dhall

@@ -0,0 +1 @@
+{ compose = ./compose.dhall, identity = ./identity.dhall }

Integer/abs.dhall

@@ -0,0 +1,15 @@
+--| Returns the absolute value of an `Integer`, i.e. its non-negative value.
+let abs
+    : Integer → Natural
+    = λ(n : Integer) →
+        if    Natural/isZero (Integer/clamp n)
+        then  Integer/clamp (Integer/negate n)
+        else  Integer/clamp n
+
+let example0 = assert : abs +7 ≡ 7
+
+let example2 = assert : abs +0 ≡ 0
+
+let example3 = assert : abs -3 ≡ 3
+
+in  abs

Integer/add.dhall

@@ -0,0 +1,22 @@
+--| `add m n` computes `m + n`.
+let Integer/subtract = ./subtract.dhall
+
+let add
+    : Integer → Integer → Integer
+    = λ(m : Integer) → λ(n : Integer) → Integer/subtract (Integer/negate m) n
+
+let example0 = assert : add +3 +5 ≡ +8
+
+let example1 = assert : add -3 -5 ≡ -8
+
+let example2 = assert : add -4 +4 ≡ +0
+
+let example3 = assert : add -3 +5 ≡ +2
+
+let example4 = assert : add +3 -5 ≡ -2
+
+let example5 = assert : add +0 -3 ≡ -3
+
+let example6 = assert : add +0 +3 ≡ +3
+
+in  add

Integer/clamp.dhall

@@ -0,0 +1,14 @@
+{-|
+Convert an `Integer` to a `Natural` number, with negative numbers becoming zero.
+-}
+let clamp
+    : Integer → Natural
+    = Integer/clamp
+
+let example0 = assert : clamp +7 ≡ 7
+
+let example2 = assert : clamp +0 ≡ 0
+
+let example3 = assert : clamp -3 ≡ 0
+
+in  clamp

Integer/divide.dhall

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

Integer/equal.dhall

@@ -0,0 +1,21 @@
+--| `equal` checks if two Integers are equal.
+let Natural/equal = ../Natural/equal.dhall
+
+let equal
+    : Integer → Integer → Bool
+    = λ(a : Integer) →
+      λ(b : Integer) →
+            Natural/equal (Integer/clamp a) (Integer/clamp b)
+        &&  Natural/equal
+              (Integer/clamp (Integer/negate a))
+              (Integer/clamp (Integer/negate b))
+
+let example0 = assert : equal +5 +5 ≡ True
+
+let example1 = assert : equal +5 +6 ≡ False
+
+let example2 = assert : equal +5 -5 ≡ False
+
+let example3 = assert : equal -5 -5 ≡ True
+
+in  equal

Integer/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.isInt v
+        then  Any/toTypeUnchecked Integer v
+        else  Misc/throw Integer "Failed to coerce object into Double"

Integer/greaterThan.dhall

@@ -0,0 +1,24 @@
+--| `greaterThan` checks if one Integer is greater than another.
+let Bool/not = ../Bool/not.dhall
+
+let lessThanEqual = ./lessThanEqual.dhall
+
+let greaterThan
+    : Integer → Integer → Bool
+    = λ(x : Integer) → λ(y : Integer) → Bool/not (lessThanEqual x y)
+
+let example0 = assert : greaterThan +5 +6 ≡ False
+
+let example1 = assert : greaterThan +5 +5 ≡ False
+
+let example2 = assert : greaterThan +5 +4 ≡ True
+
+let example3 = assert : greaterThan -5 +8 ≡ False
+
+let example4 = assert : greaterThan -5 -3 ≡ False
+
+let example5 = assert : greaterThan -3 -5 ≡ True
+
+let example6 = assert : greaterThan -3 -3 ≡ False
+
+in  greaterThan

Integer/greaterThanEqual.dhall

@@ -0,0 +1,24 @@
+{-|
+`greaterThanEqual` checks if one Integer is greater than or equal to another.
+-}
+let lessThanEqual = ./lessThanEqual.dhall
+
+let greaterThanEqual
+    : Integer → Integer → Bool
+    = λ(x : Integer) → λ(y : Integer) → lessThanEqual y x
+
+let example0 = assert : greaterThanEqual +5 +6 ≡ False
+
+let example1 = assert : greaterThanEqual +5 +5 ≡ True
+
+let example2 = assert : greaterThanEqual +5 +4 ≡ True
+
+let example3 = assert : greaterThanEqual -5 +8 ≡ False
+
+let example4 = assert : greaterThanEqual -5 -3 ≡ False
+
+let example5 = assert : greaterThanEqual -3 -5 ≡ True
+
+let example6 = assert : greaterThanEqual -3 -3 ≡ True
+
+in  greaterThanEqual

Integer/lessThan.dhall

@@ -0,0 +1,22 @@
+--| `lessThan` checks if one Integer is less than another.
+let greaterThan = ./greaterThan.dhall
+
+let lessThan
+    : Integer → Integer → Bool
+    = λ(x : Integer) → λ(y : Integer) → greaterThan y x
+
+let example0 = assert : lessThan +5 +6 ≡ True
+
+let example1 = assert : lessThan +5 +5 ≡ False
+
+let example2 = assert : lessThan +5 +4 ≡ False
+
+let example3 = assert : lessThan -5 +8 ≡ True
+
+let example4 = assert : lessThan -5 -3 ≡ True
+
+let example5 = assert : lessThan -3 -5 ≡ False
+
+let example6 = assert : lessThan -3 -3 ≡ False
+
+in  lessThan

Integer/lessThanEqual.dhall

@@ -0,0 +1,35 @@
+--| `lessThanEqual` checks if one Integer is less than or equal to another.
+let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall
+
+let Natural/lessThanEqual = ../Natural/lessThanEqual.dhall
+
+let nonPositive = ./nonPositive.dhall
+
+let nonNegative = ./nonNegative.dhall
+
+let lessThanEqual
+    : Integer → Integer → Bool
+    = λ(x : Integer) →
+      λ(y : Integer) →
+        if    nonPositive x
+        then      nonNegative y
+              ||  Natural/greaterThanEqual
+                    (Integer/clamp (Integer/negate x))
+                    (Integer/clamp (Integer/negate y))
+        else  Natural/lessThanEqual (Integer/clamp x) (Integer/clamp y)
+
+let example0 = assert : lessThanEqual +5 +6 ≡ True
+
+let example1 = assert : lessThanEqual +5 +5 ≡ True
+
+let example2 = assert : lessThanEqual +5 +4 ≡ False
+
+let example3 = assert : lessThanEqual -5 +8 ≡ True
+
+let example4 = assert : lessThanEqual -5 -3 ≡ True
+
+let example5 = assert : lessThanEqual -3 -5 ≡ False
+
+let example6 = assert : lessThanEqual -3 -3 ≡ True
+
+in  lessThanEqual

Integer/multiply.dhall

@@ -0,0 +1,37 @@
+--| `multiply m n` computes `m * n`.
+let nonPositive = ./nonPositive.dhall
+
+let multiplyNonNegative =
+      λ(x : Integer) →
+      λ(y : Integer) →
+        Natural/toInteger (Integer/clamp x * Integer/clamp y)
+
+let multiply
+    : Integer → Integer → Integer
+    = λ(m : Integer) →
+      λ(n : Integer) →
+        if    nonPositive m
+        then  if    nonPositive n
+              then  multiplyNonNegative (Integer/negate m) (Integer/negate n)
+              else  Integer/negate (multiplyNonNegative (Integer/negate m) n)
+        else  if nonPositive n
+        then  Integer/negate (multiplyNonNegative m (Integer/negate n))
+        else  multiplyNonNegative m n
+
+let example0 = assert : multiply +3 +5 ≡ +15
+
+let example1 = assert : multiply -3 +5 ≡ -15
+
+let example2 = assert : multiply -3 -5 ≡ +15
+
+let example3 = assert : multiply +0 +5 ≡ +0
+
+let example4 = assert : multiply +5 +0 ≡ +0
+
+let example5 = assert : multiply +0 +0 ≡ +0
+
+let example6 = assert : multiply +1 +5 ≡ +5
+
+let example7 = assert : multiply +3 -1 ≡ -3
+
+in  multiply

Integer/negate.dhall

@@ -0,0 +1,12 @@
+--| Invert the sign of an `Integer`, with zero remaining unchanged.
+let negate
+    : Integer → Integer
+    = Integer/negate
+
+let example0 = assert : negate -3 ≡ +3
+
+let example2 = assert : negate +7 ≡ -7
+
+let example3 = assert : negate +0 ≡ +0
+
+in  negate

Integer/negative.dhall

@@ -0,0 +1,18 @@
+{-|
+Returns `True` for any `Integer` less than `+0`.
+
+`negative` is more efficient than `./lessThan +0` or `./lessThanEqual -1`.
+-}
+let positive = ./positive.dhall
+
+let negative
+    : Integer → Bool
+    = λ(n : Integer) → positive (Integer/negate n)
+
+let example0 = assert : negative +1 ≡ False
+
+let example1 = assert : negative +0 ≡ False
+
+let example2 = assert : negative -1 ≡ True
+
+in  negative

Integer/nonNegative.dhall

@@ -0,0 +1,18 @@
+{-|
+Returns `True` for `+0` and any positive `Integer`.
+
+`nonNegative` is more efficient than `./greaterThanEqual +0` or `./greaterThan -1`.
+-}
+let nonPositive = ./nonPositive.dhall
+
+let nonNegative
+    : Integer → Bool
+    = λ(n : Integer) → nonPositive (Integer/negate n)
+
+let example0 = assert : nonNegative +1 ≡ True
+
+let example1 = assert : nonNegative +0 ≡ True
+
+let example2 = assert : nonNegative -1 ≡ False
+
+in  nonNegative

Integer/nonPositive.dhall

@@ -0,0 +1,16 @@
+{-|
+Returns `True` for `+0` and any negative `Integer`.
+
+`nonPositive` is more efficient than `./lessThanEqual +0` or `./lessThan +1`.
+-}
+let nonPositive
+    : Integer → Bool
+    = λ(n : Integer) → Natural/isZero (Integer/clamp n)
+
+let example0 = assert : nonPositive +1 ≡ False
+
+let example1 = assert : nonPositive +0 ≡ True
+
+let example2 = assert : nonPositive -1 ≡ True
+
+in  nonPositive

Integer/package.dhall

@@ -0,0 +1,23 @@
+λ(nix : ../NixPrelude.dhall) →
+  { Type = Integer
+  , abs = ./abs.dhall
+  , add = ./add.dhall
+  , clamp = ./clamp.dhall
+  , divide = ./divide.dhall nix
+  , equal = ./equal.dhall
+  , fromAny = ./fromAny.dhall nix
+  , greaterThan = ./greaterThan.dhall
+  , greaterThanEqual = ./greaterThanEqual.dhall
+  , lessThan = ./lessThan.dhall
+  , lessThanEqual = ./lessThanEqual.dhall
+  , multiply = ./multiply.dhall
+  , negate = ./negate.dhall
+  , negative = ./negative.dhall
+  , nonNegative = ./nonNegative.dhall
+  , nonPositive = ./nonPositive.dhall
+  , positive = ./positive.dhall
+  , show = ./show.dhall
+  , subtract = ./subtract.dhall
+  , toDouble = ./toDouble.dhall
+  , toNatural = ./toNatural.dhall
+  }

Integer/positive.dhall

@@ -0,0 +1,20 @@
+{-|
+Returns `True` for any `Integer` greater than `+0`.
+
+`positive` is more efficient than `./greaterThan +0` or `./greaterThanEqual +1`.
+-}
+let not = ../Bool/not.dhall
+
+let nonPositive = ./nonPositive.dhall
+
+let positive
+    : Integer → Bool
+    = λ(n : Integer) → not (nonPositive n)
+
+let example0 = assert : positive +1 ≡ True
+
+let example1 = assert : positive +0 ≡ False
+
+let example2 = assert : positive -1 ≡ False
+
+in  positive

Integer/show.dhall

@@ -0,0 +1,14 @@
+{-|
+Render an `Integer` as `Text` using the same representation as Dhall source
+code (i.e. a decimal number with a leading `-` sign if negative and a leading
+`+` sign if non-negative)
+-}
+let show
+    : Integer → Text
+    = Integer/show
+
+let example0 = assert : show -3 ≡ "-3"
+
+let example1 = assert : show +0 ≡ "+0"
+
+in  show

Integer/subtract.dhall

@@ -0,0 +1,51 @@
+--| `subtract m n` computes `n - m`.
+let nonPositive = ./nonPositive.dhall
+
+let subtractNonNegative =
+      λ(xi : Integer) →
+      λ(yi : Integer) →
+        let xn = Integer/clamp xi
+
+        let yn = Integer/clamp yi
+
+        let dn = Natural/subtract xn yn
+
+        in  if    Natural/isZero dn
+            then  Integer/negate (Natural/toInteger (Natural/subtract yn xn))
+            else  Natural/toInteger dn
+
+let subtract
+    : Integer → Integer → Integer
+    = λ(m : Integer) →
+      λ(n : Integer) →
+        if    nonPositive m
+        then  if    nonPositive n
+              then  subtractNonNegative (Integer/negate n) (Integer/negate m)
+              else  Natural/toInteger
+                      (Integer/clamp (Integer/negate m) + Integer/clamp n)
+        else  if nonPositive n
+        then  Integer/negate
+                ( Natural/toInteger
+                    (Integer/clamp m + Integer/clamp (Integer/negate n))
+                )
+        else  subtractNonNegative m n
+
+let example0 = assert : subtract +3 +5 ≡ +2
+
+let example1 = assert : subtract +4 +4 ≡ +0
+
+let example2 = assert : subtract +5 +3 ≡ -2
+
+let example3 = assert : subtract -3 -5 ≡ -2
+
+let example4 = assert : subtract -4 -4 ≡ +0
+
+let example5 = assert : subtract -5 -3 ≡ +2
+
+let example6 = assert : subtract -3 +5 ≡ +8
+
+let example7 = assert : subtract +3 -5 ≡ -8
+
+let example8 = assert : subtract +0 -3 ≡ -3
+
+in  subtract

Integer/toDouble.dhall

@@ -0,0 +1,10 @@
+--| Convert an `Integer` to the corresponding `Double`
+let toDouble
+    : Integer → Double
+    = Integer/toDouble
+
+let example0 = assert : toDouble -3 ≡ -3.0
+
+let example1 = assert : toDouble +2 ≡ 2.0
+
+in  toDouble

Integer/toNatural.dhall

@@ -0,0 +1,17 @@
+{-|
+Convert an `Integer` to an `Optional Natural`, with negative numbers becoming `None Natural`.
+-}
+let nonNegative = ./nonNegative.dhall
+
+let toNatural
+    : Integer → Optional Natural
+    = λ(n : Integer) →
+        if nonNegative n then Some (Integer/clamp n) else None Natural
+
+let example0 = assert : toNatural +7 ≡ Some 7
+
+let example2 = assert : toNatural +0 ≡ Some 0
+
+let example3 = assert : toNatural -3 ≡ None Natural
+
+in  toNatural

Natural/equal.dhall

@@ -0,0 +1,17 @@
+--| `equal` checks if two Naturals are equal.
+let lessThanEqual =
+        ./lessThanEqual.dhall
+          sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
+      ? ./lessThanEqual.dhall
+
+let equal
+    : Natural → Natural → Bool
+    = λ(a : Natural) → λ(b : Natural) → lessThanEqual a b && lessThanEqual b a
+
+let example0 = assert : equal 5 5 ≡ True
+
+let example1 = assert : equal 5 6 ≡ False
+
+let property0 = λ(n : Natural) → assert : equal n n ≡ True
+
+in  equal

Natural/greaterThanEqual.dhall

@@ -0,0 +1,23 @@
+{-|
+`greaterThanEqual` checks if one Natural is greater than or equal to another.
+-}
+let lessThanEqual =
+        ./lessThanEqual.dhall
+          sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
+      ? ./lessThanEqual.dhall
+
+let greaterThanEqual
+    : Natural → Natural → Bool
+    = λ(x : Natural) → λ(y : Natural) → lessThanEqual y x
+
+let example0 = assert : greaterThanEqual 5 6 ≡ False
+
+let example1 = assert : greaterThanEqual 5 5 ≡ True
+
+let example2 = assert : greaterThanEqual 5 4 ≡ True
+
+let property0 = λ(n : Natural) → assert : greaterThanEqual n 0 ≡ True
+
+let property1 = λ(n : Natural) → assert : greaterThanEqual n n ≡ True
+
+in  greaterThanEqual

Natural/lessThanEqual.dhall

@@ -0,0 +1,16 @@
+--| `lessThanEqual` checks if one Natural is less than or equal to another.
+let lessThanEqual
+    : Natural → Natural → Bool
+    = λ(x : Natural) → λ(y : Natural) → Natural/isZero (Natural/subtract y x)
+
+let example0 = assert : lessThanEqual 5 6 ≡ True
+
+let example1 = assert : lessThanEqual 5 5 ≡ True
+
+let example2 = assert : lessThanEqual 5 4 ≡ False
+
+let property0 = λ(n : Natural) → assert : lessThanEqual 0 n ≡ True
+
+let property1 = λ(n : Natural) → assert : lessThanEqual n n ≡ True
+
+in  lessThanEqual

Number/package.dhall

@@ -22,4 +22,5 @@
   , subtract = ./subtract.dhall nix
   , toDouble = ./toDouble.dhall nix
   , toInteger = ./toInteger.dhall nix
+  , toNatural = ./toNatural.dhall nix
   }

Number/toNatural.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Number = ./Type.dhall
+
+  let Integer/toNatural = ../Integer/toNatural.dhall
+
+  let Number/toInteger = ./toInteger.dhall nix
+
+  in  λ(a : Number) → Integer/toNatural (Number/toInteger a)

package.dhall

@@ -2,6 +2,8 @@
   { Any = ./Any/package.dhall nix
   , Bool = ./Bool/package.dhall nix
   , Double = ./Double/package.dhall nix
+  , Function = ./Function/package.dhall
+  , Integer = ./Integer/package.dhall nix
   , Misc = ./Misc/package.dhall nix
   , Monoid = ./Monoid.dhall
   , Number = ./Number/package.dhall nix