Add List/

Integer/package.dhall

@@ -25,7 +25,7 @@
   , positive = ./positive.dhall
   , product = ./product.dhall
   , show = ./show.dhall
-  , sort = ./sort.dhall
+  , sort = ./sort.dhall nix
   , subtract = ./subtract.dhall
   , sum = ./sum.dhall
   , toDouble = ./toDouble.dhall

List/all.dhall

@@ -0,0 +1,16 @@
+{-|
+Returns `True` if the supplied function returns `True` for all elements in the
+`List`
+-}
+let all
+    : ∀(a : Type) → (a → Bool) → List a → Bool
+    = λ(a : Type) →
+      λ(f : a → Bool) →
+      λ(xs : List a) →
+        List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True
+
+let example0 = assert : all Natural Natural/even [ 2, 3, 5 ] ≡ False
+
+let example1 = assert : all Natural Natural/even ([] : List Natural) ≡ True
+
+in  all

List/any.dhall

@@ -0,0 +1,16 @@
+{-|
+Returns `True` if the supplied function returns `True` for any element in the
+`List`
+-}
+let any
+    : ∀(a : Type) → (a → Bool) → List a → Bool
+    = λ(a : Type) →
+      λ(f : a → Bool) →
+      λ(xs : List a) →
+        List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
+
+let example0 = assert : any Natural Natural/even [ 2, 3, 5 ] ≡ True
+
+let example1 = assert : any Natural Natural/even ([] : List Natural) ≡ False
+
+in  any

List/build.dhall

@@ -0,0 +1,30 @@
+--| `build` is the inverse of `fold`
+let build
+    : ∀(a : Type) →
+      (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) →
+        List a
+    = List/build
+
+let example0 =
+        assert
+      :   build
+            Text
+            ( λ(list : Type) →
+              λ(cons : Text → list → list) →
+              λ(nil : list) →
+                cons "ABC" (cons "DEF" nil)
+            )
+        ≡ [ "ABC", "DEF" ]
+
+let example1 =
+        assert
+      :   build
+            Text
+            ( λ(list : Type) →
+              λ(cons : Text → list → list) →
+              λ(nil : list) →
+                nil
+            )
+        ≡ ([] : List Text)
+
+in  build

List/concat.dhall

@@ -0,0 +1,34 @@
+--| Concatenate a `List` of `List`s into a single `List`
+let concat
+    : ∀(a : Type) → List (List a) → List a
+    = λ(a : Type) →
+      λ(xss : List (List a)) →
+        List/build
+          a
+          ( λ(list : Type) →
+            λ(cons : a → list → list) →
+            λ(nil : list) →
+              List/fold
+                (List a)
+                xss
+                list
+                (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys)
+                nil
+          )
+
+let example0 =
+        assert
+      :   concat Natural [ [ 0, 1, 2 ], [ 3, 4 ], [ 5, 6, 7, 8 ] ]
+        ≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
+
+let example1 =
+        assert
+      :   concat
+            Natural
+            [ [] : List Natural, [] : List Natural, [] : List Natural ]
+        ≡ ([] : List Natural)
+
+let example2 =
+      assert : concat Natural ([] : List (List Natural)) ≡ ([] : List Natural)
+
+in  concat

List/concatMap.dhall

@@ -0,0 +1,32 @@
+{-|
+Transform a list by applying a function to each element and flattening the
+results
+-}
+let concatMap
+    : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b
+    = λ(a : Type) →
+      λ(b : Type) →
+      λ(f : a → List b) →
+      λ(xs : List a) →
+        List/build
+          b
+          ( λ(list : Type) →
+            λ(cons : b → list → list) →
+              List/fold a xs list (λ(x : a) → List/fold b (f x) list cons)
+          )
+
+let example0 =
+        assert
+      :   concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ]
+        ≡ [ 2, 2, 3, 3, 5, 5 ]
+
+let example1 =
+        assert
+      :   concatMap
+            Natural
+            Natural
+            (λ(n : Natural) → [ n, n ])
+            ([] : List Natural)
+        ≡ ([] : List Natural)
+
+in  concatMap

List/default.dhall

@@ -0,0 +1,10 @@
+λ(nix : ../NixPrelude.dhall) →
+  let Optional/default = ../Optional/default.dhall nix
+
+  let default
+      : ∀(a : Type) → Optional (List a) → List a
+      = λ(a : Type) →
+        λ(o : Optional (List a)) →
+          Optional/default (List a) ([] : List a) o
+
+  in  default

List/drop.dhall

@@ -0,0 +1,25 @@
+--| Remove first `n` elements of a list
+let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall
+
+let drop
+    : ∀(n : Natural) → ∀(a : Type) → List a → List a
+    = λ(n : Natural) →
+      λ(a : Type) →
+      λ(xs : List a) →
+        List/fold
+          { index : Natural, value : a }
+          (List/indexed a xs)
+          (List a)
+          ( λ(x : { index : Natural, value : a }) →
+            λ(xs : List a) →
+              if    Natural/greaterThanEqual x.index n
+              then  [ x.value ] # xs
+              else  xs
+          )
+          ([] : List a)
+
+let example = assert : drop 2 Natural [ 2, 3, 5 ] ≡ [ 5 ]
+
+let example = assert : drop 5 Natural [ 2, 3, 5 ] ≡ ([] : List Natural)
+
+in  drop

List/empty.dhall

@@ -0,0 +1,8 @@
+--| An empty list of the given type
+let empty
+    : ∀(a : Type) → List a
+    = λ(a : Type) → [] : List a
+
+let example0 = assert : empty Bool ≡ ([] : List Bool)
+
+in  empty

List/filter.dhall

@@ -0,0 +1,22 @@
+--| Only keep elements of the list where the supplied function returns `True`
+let filter
+    : ∀(a : Type) → (a → Bool) → List a → List a
+    = λ(a : Type) →
+      λ(f : a → Bool) →
+      λ(xs : List a) →
+        List/build
+          a
+          ( λ(list : Type) →
+            λ(cons : a → list → list) →
+              List/fold
+                a
+                xs
+                list
+                (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs)
+          )
+
+let example0 = assert : filter Natural Natural/even [ 2, 3, 5 ] ≡ [ 2 ]
+
+let example1 = assert : filter Natural Natural/odd [ 2, 3, 5 ] ≡ [ 3, 5 ]
+
+in  filter

List/filterMap.dhall

@@ -0,0 +1,13 @@
+λ(nix : ../NixPrelude.dhall) →
+  let List/concatMap = ./concatMap.dhall
+
+  let Optional/toList = ../Optional/toList.dhall nix
+
+  let filterMap
+      : ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b
+      = λ(a : Type) →
+        λ(b : Type) →
+        λ(f : a → Optional b) →
+          List/concatMap a b (λ(x : a) → Optional/toList b (f x))
+
+  in  filterMap

List/fold.dhall

@@ -0,0 +1,43 @@
+{-|
+`fold` is the primitive function for consuming `List`s
+
+If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a
+`fold` just replaces each `cons` and `nil` with something else
+-}
+let fold
+    : ∀(a : Type) →
+      List a →
+      ∀(list : Type) →
+      ∀(cons : a → list → list) →
+      ∀(nil : list) →
+        list
+    = List/fold
+
+let example0 =
+        assert
+      :   fold
+            Natural
+            [ 2, 3, 5 ]
+            Text
+            (λ(x : Natural) → λ(y : Text) → Natural/show x ++ y)
+            "0"
+        ≡ "2350"
+
+let example1 =
+      λ(nil : Text) →
+          assert
+        :   fold
+              Natural
+              [ 2, 3, 5 ]
+              Text
+              (λ(x : Natural) → λ(y : Text) → Natural/show x ++ y)
+              nil
+          ≡ "2" ++ ("3" ++ ("5" ++ nil))
+
+let example2 =
+      λ(cons : Natural → Text → Text) →
+      λ(nil : Text) →
+          assert
+        : fold Natural [ 2, 3, 5 ] Text cons nil ≡ cons 2 (cons 3 (cons 5 nil))
+
+in  fold

List/foldLeft.dhall

@@ -0,0 +1,60 @@
+{-|
+`foldLeft` is like `List/fold` except that the accumulation starts from the left
+
+If you treat the list `[ x, y, z ]` as `cons (cons (cons nil x) y) z`, then
+`foldLeft` just replaces each `cons` and `nil` with something else
+-}
+let foldLeft
+    : ∀(a : Type) →
+      List a →
+      ∀(list : Type) →
+      ∀(cons : list → a → list) →
+      ∀(nil : list) →
+        list
+    = λ(a : Type) →
+      λ(xs : List a) →
+      λ(list : Type) →
+      λ(cons : list → a → list) →
+      λ(nil : list) →
+        List/fold
+          a
+          xs
+          (list → list)
+          (λ(x : a) → λ(f : list → list) → λ(l : list) → f (cons l x))
+          (λ(l : list) → l)
+          nil
+
+let example0 =
+        assert
+      :   foldLeft
+            Natural
+            [ 2, 3, 5 ]
+            Text
+            (λ(x : Text) → λ(y : Natural) → x ++ Natural/show y)
+            "0"
+        ≡ "0235"
+
+let example1 =
+        assert
+      :   ( λ(nil : Text) →
+              foldLeft
+                Natural
+                [ 2, 3, 5 ]
+                Text
+                (λ(x : Text) → λ(y : Natural) → x ++ Natural/show y)
+                nil
+          )
+        ≡ (λ(nil : Text) → nil ++ "2" ++ "3" ++ "5")
+
+let example2 =
+        assert
+      :   ( λ(cons : Text → Natural → Text) →
+            λ(nil : Text) →
+              foldLeft Natural [ 2, 3, 5 ] Text cons nil
+          )
+        ≡ ( λ(cons : Text → Natural → Text) →
+            λ(nil : Text) →
+              cons (cons (cons nil 2) 3) 5
+          )
+
+in  foldLeft

List/generate.dhall

@@ -0,0 +1,35 @@
+{-|
+Build a list by calling the supplied function on all `Natural` numbers from `0`
+up to but not including the supplied `Natural` number
+-}
+let generate
+    : Natural → ∀(a : Type) → (Natural → a) → List a
+    = λ(n : Natural) →
+      λ(a : Type) →
+      λ(f : Natural → a) →
+        List/build
+          a
+          ( λ(list : Type) →
+            λ(cons : a → 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 (f x.index))
+          )
+
+let example0 =
+      assert : generate 5 Bool Natural/even ≡ [ True, False, True, False, True ]
+
+let example1 = assert : generate 0 Bool Natural/even ≡ ([] : List Bool)
+
+in  generate

List/head.dhall

@@ -0,0 +1,10 @@
+--| Retrieve the first element of the list
+let head
+    : ∀(a : Type) → List a → Optional a
+    = List/head
+
+let example0 = assert : head Natural [ 0, 1, 2 ] ≡ Some 0
+
+let example1 = assert : head Natural ([] : List Natural) ≡ None Natural
+
+in  head

List/index.dhall

@@ -0,0 +1,15 @@
+--| Retrieve an element from a `List` using its 0-based index
+let drop = ./drop.dhall
+
+let index
+    : Natural → ∀(a : Type) → List a → Optional a
+    = λ(n : Natural) → λ(a : Type) → λ(xs : List a) → List/head a (drop n a xs)
+
+let property =
+      λ(n : Natural) → λ(a : Type) → assert : index n a ([] : List a) ≡ None a
+
+let example0 = assert : index 1 Natural [ 2, 3, 5 ] ≡ Some 3
+
+let example1 = assert : index 1 Natural ([] : List Natural) ≡ None Natural
+
+in  index

List/indexed.dhall

@@ -0,0 +1,19 @@
+--| Tag each element of the list with its index
+let indexed
+    : ∀(a : Type) → List a → List { index : Natural, value : a }
+    = List/indexed
+
+let example0 =
+        assert
+      :   indexed Bool [ True, False, True ]
+        ≡ [ { index = 0, value = True }
+          , { index = 1, value = False }
+          , { index = 2, value = True }
+          ]
+
+let example1 =
+        assert
+      :   indexed Bool ([] : List Bool)
+        ≡ ([] : List { index : Natural, value : Bool })
+
+in  indexed

List/iterate.dhall

@@ -0,0 +1,42 @@
+{-|
+Generate a list of the specified length given a seed value and transition
+function
+-}
+let iterate
+    : Natural → ∀(a : Type) → (a → a) → a → List a
+    = λ(n : Natural) →
+      λ(a : Type) →
+      λ(f : a → a) →
+      λ(x : a) →
+        List/build
+          a
+          ( λ(list : Type) →
+            λ(cons : a → list → list) →
+              List/fold
+                { index : Natural, value : {} }
+                ( List/indexed
+                    {}
+                    ( List/build
+                        {}
+                        ( λ(list : Type) →
+                          λ(cons : {} → list → list) →
+                            Natural/fold n list (cons {=})
+                        )
+                    )
+                )
+                list
+                ( λ(y : { index : Natural, value : {} }) →
+                    cons (Natural/fold y.index a f x)
+                )
+          )
+
+let example0 =
+        assert
+      :   iterate 10 Natural (λ(x : Natural) → x * 2) 1
+        ≡ [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
+
+let example1 =
+        assert
+      : iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)
+
+in  iterate

List/last.dhall

@@ -0,0 +1,10 @@
+--| Retrieve the last element of the list
+let last
+    : ∀(a : Type) → List a → Optional a
+    = List/last
+
+let example0 = assert : last Natural [ 0, 1, 2 ] ≡ Some 2
+
+let example1 = assert : last Natural ([] : List Natural) ≡ None Natural
+
+in  last

List/length.dhall

@@ -0,0 +1,10 @@
+--| Returns the number of elements in a list
+let length
+    : ∀(a : Type) → List a → Natural
+    = List/length
+
+let example0 = assert : length Natural [ 0, 1, 2 ] ≡ 3
+
+let example1 = assert : length Natural ([] : List Natural) ≡ 0
+
+in  length

List/map.dhall

@@ -0,0 +1,23 @@
+--| Transform a list by applying a function to each element
+let map
+    : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b
+    = λ(a : Type) →
+      λ(b : Type) →
+      λ(f : a → b) →
+      λ(xs : List a) →
+        List/build
+          b
+          ( λ(list : Type) →
+            λ(cons : b → list → list) →
+              List/fold a xs list (λ(x : a) → cons (f x))
+          )
+
+let example0 =
+        assert
+      : map Natural Bool Natural/even [ 2, 3, 5 ] ≡ [ True, False, False ]
+
+let example1 =
+        assert
+      : map Natural Bool Natural/even ([] : List Natural) ≡ ([] : List Bool)
+
+in  map

List/null.dhall

@@ -0,0 +1,10 @@
+--| Returns `True` if the `List` is empty and `False` otherwise
+let null
+    : ∀(a : Type) → List a → Bool
+    = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs)
+
+let example0 = assert : null Natural [ 0, 1, 2 ] ≡ False
+
+let example1 = assert : null Natural ([] : List Natural) ≡ True
+
+in  null

List/package.dhall

@@ -0,0 +1,31 @@
+λ(nix : ../NixPrelude.dhall) →
+  { all = ./all.dhall
+  , any = ./any.dhall
+  , build = ./build.dhall
+  , concat = ./concat.dhall
+  , concatMap = ./concatMap.dhall
+  , default = ./default.dhall nix
+  , drop = ./drop.dhall
+  , empty = ./empty.dhall
+  , filter = ./filter.dhall
+  , filterMap = ./filterMap.dhall nix
+  , fold = ./fold.dhall
+  , foldLeft = ./foldLeft.dhall
+  , generate = ./generate.dhall
+  , head = ./head.dhall
+  , index = ./index.dhall
+  , indexed = ./indexed.dhall
+  , iterate = ./iterate.dhall
+  , last = ./last.dhall
+  , length = ./length.dhall
+  , map = ./map.dhall
+  , null = ./null.dhall
+  , partition = ./partition.dhall
+  , replicate = ./replicate.dhall
+  , reverse = ./reverse.dhall
+  , shifted = ./shifted.dhall
+  , take = ./take.dhall
+  , unpackOptionals = ./unpackOptionals.dhall nix
+  , unzip = ./unzip.dhall
+  , zip = ./zip.dhall nix
+  }

List/replicate.dhall

@@ -0,0 +1,18 @@
+--| Build a list by copying the given element the specified number of times
+let replicate
+    : Natural → ∀(a : Type) → a → List a
+    = λ(n : Natural) →
+      λ(a : Type) →
+      λ(x : a) →
+        List/build
+          a
+          ( λ(list : Type) →
+            λ(cons : a → list → list) →
+              Natural/fold n list (cons x)
+          )
+
+let example0 = assert : replicate 9 Natural 1 ≡ [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
+
+let example1 = assert : replicate 0 Natural 1 ≡ ([] : List Natural)
+
+in  replicate

List/reverse.dhall

@@ -0,0 +1,11 @@
+--| Reverse a list
+let reverse
+    : ∀(a : Type) → List a → List a
+    = List/reverse
+
+let example0 = assert : reverse Natural [ 0, 1, 2 ] ≡ [ 2, 1, 0 ]
+
+let example1 =
+      assert : reverse Natural ([] : List Natural) ≡ ([] : List Natural)
+
+in  reverse

List/shifted.dhall

@@ -0,0 +1,83 @@
+{-|
+Combine a `List` of `List`s, offsetting the `index` of each element by the
+number of elements in preceding lists
+-}
+let shifted
+    : ∀(a : Type) →
+      List (List { index : Natural, value : a }) →
+        List { index : Natural, value : a }
+    = λ(a : Type) →
+      λ(kvss : List (List { index : Natural, value : a })) →
+        List/build
+          { index : Natural, value : a }
+          ( λ(list : Type) →
+            λ(cons : { index : Natural, value : a } → list → list) →
+            λ(nil : list) →
+              let result =
+                    List/fold
+                      (List { index : Natural, value : a })
+                      kvss
+                      { count : Natural, diff : Natural → list }
+                      ( λ(kvs : List { index : Natural, value : a }) →
+                        λ(y : { count : Natural, diff : Natural → list }) →
+                          let length =
+                                List/length { index : Natural, value : a } kvs
+
+                          in  { count = y.count + length
+                              , diff =
+                                  λ(n : Natural) →
+                                    List/fold
+                                      { index : Natural, value : a }
+                                      kvs
+                                      list
+                                      ( λ ( kvOld
+                                          : { index : Natural, value : a }
+                                          ) →
+                                        λ(z : list) →
+                                          let kvNew =
+                                                { index = kvOld.index + n
+                                                , value = kvOld.value
+                                                }
+
+                                          in  cons kvNew z
+                                      )
+                                      (y.diff (n + length))
+                              }
+                      )
+                      { count = 0, diff = λ(_ : Natural) → nil }
+
+              in  result.diff 0
+          )
+
+let example0 =
+        assert
+      :   shifted
+            Bool
+            [ [ { index = 0, value = True }
+              , { index = 1, value = True }
+              , { index = 2, value = True }
+              ]
+            , [ { index = 0, value = False }, { index = 1, value = False } ]
+            , [ { index = 0, value = True }
+              , { index = 1, value = True }
+              , { index = 2, value = True }
+              , { index = 3, value = True }
+              ]
+            ]
+        ≡ [ { index = 0, value = True }
+          , { index = 1, value = True }
+          , { index = 2, value = True }
+          , { index = 3, value = False }
+          , { index = 4, value = False }
+          , { index = 5, value = True }
+          , { index = 6, value = True }
+          , { index = 7, value = True }
+          , { index = 8, value = True }
+          ]
+
+let example1 =
+        assert
+      :   shifted Bool ([] : List (List { index : Natural, value : Bool }))
+        ≡ ([] : List { index : Natural, value : Bool })
+
+in  shifted

List/take.dhall

@@ -0,0 +1,23 @@
+--| Truncate a list to the first `n` elements
+let Natural/lessThan = ../Natural/lessThan.dhall
+
+let take
+    : ∀(n : Natural) → ∀(a : Type) → List a → List a
+    = λ(n : Natural) →
+      λ(a : Type) →
+      λ(xs : List a) →
+        List/fold
+          { index : Natural, value : a }
+          (List/indexed a xs)
+          (List a)
+          ( λ(x : { index : Natural, value : a }) →
+            λ(xs : List a) →
+              if Natural/lessThan x.index n then [ x.value ] # xs else xs
+          )
+          ([] : List a)
+
+let example = assert : take 2 Natural [ 2, 3, 5 ] ≡ [ 2, 3 ]
+
+let example = assert : take 5 Natural [ 2, 3, 5 ] ≡ [ 2, 3, 5 ]
+
+in  take

List/unpackOptionals.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let List/filterMap = ./filterMap.dhall nix
+
+  let unpackOptionals
+      : ∀(a : Type) → ∀(l : List (Optional a)) → List a
+      = λ(a : Type) → List/filterMap (Optional a) a (λ(x : Optional a) → x)
+
+  in  unpackOptionals

List/unzip.dhall

@@ -0,0 +1,50 @@
+--| Unzip a `List` into two separate `List`s
+let unzip
+    : ∀(a : Type) →
+      ∀(b : Type) →
+      List { _1 : a, _2 : b } →
+        { _1 : List a, _2 : List b }
+    = λ(a : Type) →
+      λ(b : Type) →
+      λ(xs : List { _1 : a, _2 : b }) →
+        { _1 =
+            List/build
+              a
+              ( λ(list : Type) →
+                λ(cons : a → list → list) →
+                  List/fold
+                    { _1 : a, _2 : b }
+                    xs
+                    list
+                    (λ(x : { _1 : a, _2 : b }) → cons x._1)
+              )
+        , _2 =
+            List/build
+              b
+              ( λ(list : Type) →
+                λ(cons : b → list → list) →
+                  List/fold
+                    { _1 : a, _2 : b }
+                    xs
+                    list
+                    (λ(x : { _1 : a, _2 : b }) → cons x._2)
+              )
+        }
+
+let example0 =
+        assert
+      :   unzip
+            Text
+            Bool
+            [ { _1 = "ABC", _2 = True }
+            , { _1 = "DEF", _2 = False }
+            , { _1 = "GHI", _2 = True }
+            ]
+        ≡ { _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }
+
+let example1 =
+        assert
+      :   unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
+        ≡ { _1 = [] : List Text, _2 = [] : List Bool }
+
+in  unzip

List/zip.dhall

@@ -0,0 +1,36 @@
+λ(nix : ../NixPrelude.dhall) →
+  let List/index = ./index.dhall
+
+  let List/map = ./map.dhall
+
+  let Natural/min = ../Natural/min.dhall
+
+  let Natural/enumerate = ../Natural/enumerate.dhall
+
+  let Optional/unwrap = ../Optional/unwrap.dhall nix
+
+  let zip
+      : ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b }
+      = λ(a : Type) →
+        λ(xs : List a) →
+        λ(b : Type) →
+        λ(ys : List b) →
+          let xsLen = List/length a xs
+
+          let ysLen = List/length b ys
+
+          let resLen = Natural/min xsLen ysLen
+
+          let indexes = Natural/enumerate resLen
+
+          in  List/map
+                Natural
+                { _1 : a, _2 : b }
+                ( λ(i : Natural) →
+                    { _1 = Optional/unwrap a (List/index i a xs)
+                    , _2 = Optional/unwrap b (List/index i b ys)
+                    }
+                )
+                indexes
+
+  in  zip

Number/package.dhall

@@ -2,7 +2,7 @@
   { Type = ./Type.dhall
   , abs = ./abs.dhall nix
   , add = ./add.dhall nix
-  , build = ./build.dhall
+  , build = ./build.dhall nix
   , clamp = ./clamp.dhall nix
   , divide = ./divide.dhall nix
   , equal = ./equal.dhall nix

Optional/default.dhall

@@ -0,0 +1,13 @@
+λ(nix : ../NixPrelude.dhall) →
+  let identity = ../Function/identity.dhall
+
+  let fold = ./fold.dhall nix
+
+  let default
+      : ∀(a : Type) → a → Optional a → a
+      = λ(a : Type) →
+        λ(default : a) →
+        λ(o : Optional a) →
+          fold a o a (identity a) default
+
+  in  default

Optional/fold.dhall

@@ -0,0 +1,36 @@
+λ(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 fold
+      : ∀(a : Type) →
+        Optional a →
+        ∀(optional : Type) →
+        ∀(some : a → optional) →
+        ∀(none : optional) →
+          optional
+      = λ(a : Type) →
+        λ(o : Optional a) →
+        λ(optional : Type) →
+        λ(some : a → optional) →
+        λ(none : optional) →
+          if isNone a o then none else some (unwrapUnsafe a o)
+
+  in  fold

Optional/map.dhall

@@ -1,23 +1,5 @@
 λ(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 fold = ./fold.dhall nix
 
   let map
       : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b
@@ -25,6 +7,6 @@
         λ(b : Type) →
         λ(f : a → b) →
         λ(o : Optional a) →
-          if isNone a o then None b else Some (f (unwrapUnsafe a o))
+          fold a o (Optional b) (λ(v : a) → Some (f v)) (None b)
 
   in  map

Optional/toList.dhall

@@ -0,0 +1,6 @@
+λ(nix : ../NixPrelude.dhall) →
+  let fold = ./fold.dhall nix
+
+  in  λ(a : Type) →
+      λ(o : Optional a) →
+        fold a o (List a) (λ(v : a) → [ v ]) ([] : List a)

Optional/unwrap.dhall

@@ -0,0 +1,8 @@
+λ(nix : ../NixPrelude.dhall) →
+  let default = ./default.dhall nix
+
+  let Misc/throw = ../Misc/throw.dhall nix
+
+  in  λ(t : Type) →
+      λ(o : Optional t) →
+        default t (Misc/throw t "Tried to unwrap None") o

package.dhall

@@ -4,6 +4,7 @@
   , Double = ./Double/package.dhall nix
   , Function = ./Function/package.dhall
   , Integer = ./Integer/package.dhall nix
+  , List = ./List/package.dhall nix
   , Misc = ./Misc/package.dhall nix
   , Monoid = ./Monoid.dhall
   , Natural = ./Natural/package.dhall nix