Cache the whole Prelude so we can test without internet

Prelude/Bool/and

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

Prelude/Bool/build

@@ -0,0 +1,17 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) = True
+
+./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) = False
+```
+-}
+    let build
+        : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool
+        =   λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool)
+          → f Bool True False
+
+in  build

Prelude/Bool/even

@@ -0,0 +1,22 @@
+{-
+Returns `True` if there are an even number of `False` elements in the list and
+returns `False` otherwise
+
+Examples:
+
+```
+./even [ False, True, False ] = True
+
+./even [ False, True ] = False
+
+./even [ False ] = False
+
+./even ([] : List Bool) = True
+```
+-}
+    let even
+        : List Bool → Bool
+        =   λ(xs : List Bool)
+          → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True
+
+in  even

Prelude/Bool/fold

@@ -0,0 +1,20 @@
+{-
+`fold` is essentially the same as `if`/`then`/else` except as a function
+
+Examples:
+
+```
+./fold True Natural 0 1 = 0
+
+./fold False Natural 0 1 = 1
+```
+-}
+    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
+
+in  fold

Prelude/Bool/not

@@ -0,0 +1,12 @@
+{-
+Flip the value of a `Bool`
+
+Examples:
+
+```
+./not True = False
+
+./not False = True
+```
+-}
+let not : Bool → Bool = λ(b : Bool) → b == False in not

Prelude/Bool/odd

@@ -0,0 +1,22 @@
+{-
+Returns `True` if there are an odd number of `True` elements in the list and
+returns `False` otherwise
+
+Examples:
+
+```
+./odd [ True, False, True ] = False
+
+./odd [ True, False ] = True
+
+./odd [ True ] = True
+
+./odd ([] : List Bool) = False
+```
+-}
+    let odd
+        : List Bool → Bool
+        =   λ(xs : List Bool)
+          → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False
+
+in  odd

Prelude/Bool/or

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

Prelude/Bool/package.dhall

@@ -0,0 +1,17 @@
+{ and =
+    ./and
+, build =
+    ./build
+, even =
+    ./even
+, fold =
+    ./fold
+, not =
+    ./not
+, odd =
+    ./odd
+, or =
+    ./or
+, show =
+    ./show
+}

Prelude/Bool/show

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

Prelude/Double/package.dhall

@@ -0,0 +1 @@
+{ show = ./show }

Prelude/Double/show

@@ -0,0 +1,13 @@
+{-
+Render a `Double` as `Text` using the same representation as Dhall source
+code (i.e. a decimal floating point number with a leading `-` sign if negative)
+
+Examples:
+
+```
+./show -3.1 = "-3.1"
+
+./show  0.4 =  "0.4"
+```
+-}
+let show : Double → Text = Double/show in show

Prelude/Function/compose

@@ -0,0 +1,21 @@
+{-
+Compose two functions into one.
+
+Examples:
+
+```
+./compose Natural Natural Bool (λ(n : Natural) → n + n) ../Natural/even 3
+= True
+```
+-}
+    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)
+
+in  compose

Prelude/Function/package.dhall

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

Prelude/Integer/package.dhall

@@ -0,0 +1 @@
+{ show = ./show }

Prelude/Integer/show

@@ -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)
+
+Examples:
+
+```
+./show -3 = "-3"
+
+./show +0 = "+0"
+```
+-}
+let show : Integer → Text = Integer/show in show

Prelude/Integer/toDouble

@@ -0,0 +1,12 @@
+{-
+Convert an `Integer` to the corresponding `Double`
+
+Examples:
+
+```
+./toDouble -3 = -3.0
+
+./toDouble +2 = 2.0
+```
+-}
+let toDouble : Integer → Double = Integer/toDouble in toDouble

Prelude/JSON/Nesting

@@ -0,0 +1,32 @@
+{-
+This type is used as part of `dhall-json`'s support for preserving alternative
+names
+
+For example, this Dhall code:
+
+```
+    let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
+
+in  let example = constructors Example
+
+in  let Nesting = < Inline : {} | Nested : Text >
+
+in  let nesting = constructors Nesting
+
+in  { field    = "name"
+    , nesting  = nesting.Inline {=}
+    , contents = example.Left { foo = 2 }
+    }
+```
+
+... generates this JSON:
+
+```
+{
+  "foo": 2,
+  "name": "Left"
+ }
+```
+
+-}
+let Nesting : Type = < Inline : {} | Nested : Text > in Nesting

Prelude/JSON/Tagged

@@ -0,0 +1,69 @@
+{-
+This is a convenient type-level function when using `dhall-to-json`'s support
+for preserving alternative names
+
+For example, this code:
+
+```
+    let map = ../List/map
+
+in  let Provisioner =
+          < shell :
+              { inline : List Text }
+          | file :
+              { source : Text, destination : Text }
+          >
+
+in  let provisioner = constructors Provisioner
+
+in  let Tagged = ./Tagged
+
+in  let nesting = constructors ./Nesting
+
+in  let wrap
+        : Provisioner → Tagged Provisioner
+        =   λ(x : Provisioner)
+          → { field = "type", nesting = nesting.Nested "params", contents = x }
+
+in  { provisioners =
+        map
+        Provisioner
+        (Tagged Provisioner)
+        wrap
+        [ provisioner.shell { inline = [ "echo foo" ] }
+        , provisioner.file
+          { source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
+        ]
+    }
+```
+
+... produces this JSON:
+
+```
+{
+  "provisioners": [
+    {
+      "params": {
+        "inline": [
+          "echo foo"
+        ]
+      },
+      "type": "shell"
+    },
+    {
+      "params": {
+        "destination": "/tmp/app.tar.gz",
+        "source": "app.tar.gz"
+      },
+      "type": "file"
+    }
+  ]
+}
+```
+
+-}
+    let Tagged
+        : Type → Type
+        = λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a }
+
+in  Tagged

Prelude/JSON/keyText

@@ -0,0 +1,17 @@
+{-
+Builds a key-value record such that a List of them will be converted to a
+homogeneous record by dhall-to-json and dhall-to-yaml.
+Both key and value are fixed to Text.
+Take a look at `Record/keyValue` for a polymorphic version.
+
+Example:
+
+```
+./keyText "foo" "bar" = { mapKey = "foo", mapValue = "bar" }
+```
+-}
+
+    let keyText =
+          λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
+
+in  keyText

Prelude/JSON/keyValue

@@ -0,0 +1,20 @@
+{-
+Builds a key-value record such that a List of them will be converted to a
+homogeneous record by dhall-to-json and dhall-to-yaml.
+
+Examples:
+
+```
+./keyValue Natural "foo" 2 = { mapKey = "foo", mapValue = 2 }
+
+./keyValue Text "bar" "baz" = { mapKey = "bar", mapValue = "baz" }
+```
+-}
+
+    let keyValue =
+            λ(v : Type)
+          → λ(key : Text)
+          → λ(value : v)
+          → { mapKey = key, mapValue = value }
+
+in  keyValue

Prelude/JSON/package.dhall

@@ -0,0 +1 @@
+{ keyText = ./keyText, keyValue = ./keyValue }

Prelude/List/all

@@ -0,0 +1,20 @@
+{-
+Returns `True` if the supplied function returns `True` for all elements in the
+`List`
+
+Examples:
+
+```
+./all Natural Natural/even [ 2, 3, 5 ] = False
+
+./all Natural Natural/even ([] : List Natural) = True
+```
+-}
+    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
+
+in  all

Prelude/List/any

@@ -0,0 +1,20 @@
+{-
+Returns `True` if the supplied function returns `True` for any element in the
+`List`
+
+Examples:
+
+```
+./any Natural Natural/even [ 2, 3, 5 ] = True
+
+./any Natural Natural/even ([] : List Natural) = False
+```
+-}
+    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
+
+in  any

Prelude/List/build

@@ -0,0 +1,32 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build
+Text
+(   λ(list : Type)
+→   λ(cons : Text → list → list)
+→   λ(nil : list)
+→   cons "ABC" (cons "DEF" nil)
+)
+= [ "ABC", "DEF" ]
+
+./build
+Text
+(   λ(list : Type)
+→   λ(cons : Text → list → list)
+→   λ(nil : list)
+→   nil
+)
+= [] : List Text
+```
+-}
+    let build
+        :   ∀(a : Type)
+          → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
+          → List a
+        = List/build
+
+in  build

Prelude/List/concat

@@ -0,0 +1,42 @@
+{-
+Concatenate a `List` of `List`s into a single `List`
+
+Examples:
+
+```
+./concat Natural
+[   [0, 1, 2]
+,   [3, 4]
+,   [5, 6, 7, 8]
+]
+= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
+
+./concat Natural
+(   [   [] : List Natural
+    ,   [] : List Natural
+    ,   [] : List Natural
+    ]
+)
+= [] : List Natural
+
+./concat Natural ([] : List (List Natural)) = [] : List Natural
+```
+-}
+    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
+            )
+
+in  concat

Prelude/List/concatMap

@@ -0,0 +1,28 @@
+{-
+Transform a list by applying a function to each element and flattening the
+results
+
+Examples:
+
+```
+./concatMap Natural Natural (λ(n : Natural) → [n, n]) [2, 3, 5]
+= [ 2, 2, 3, 3, 5, 5 ]
+
+./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural)
+= [] : List Natural
+```
+-}
+    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)
+            )
+
+in  concatMap

Prelude/List/filter

@@ -0,0 +1,30 @@
+{-
+Only keep elements of the list where the supplied function returns `True`
+
+Examples:
+
+```
+./filter Natural Natural/even [ 2, 3, 5 ]
+= [ 2 ]
+
+./filter Natural Natural/odd [ 2, 3, 5 ]
+= [ 3, 5 ]
+```
+-}
+    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)
+            )
+
+in  filter

Prelude/List/fold

@@ -0,0 +1,46 @@
+{-
+`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
+
+Examples:
+
+```
+    ./fold
+    Natural
+    [ 2, 3, 5 ]
+    Natural
+    (λ(x : Natural) → λ(y : Natural) → x + y)
+    0
+=   10
+
+    λ(nil : Natural)
+→   ./fold
+    Natural
+    [ 2, 3, 5 ]
+    Natural
+    (λ(x : Natural) → λ(y : Natural) → x + y)
+    nil
+=   λ(nil : Natural) → 2 + (3 + (5 + nil))
+
+    λ(list : Type)
+→   λ(cons : Natural → list → list)
+→   λ(nil : list)
+→   ./fold Natural [ 2, 3, 5 ] list cons nil
+=   λ(list : Type)
+→   λ(cons : Natural → list → list)
+→   λ(nil : list)
+→   cons 2 (cons 3 (cons 5 nil))
+```
+-}
+    let fold
+        :   ∀(a : Type)
+          → List a
+          → ∀(list : Type)
+          → ∀(cons : a → list → list)
+          → ∀(nil : list)
+          → list
+        = List/fold
+
+in  fold

Prelude/List/generate

@@ -0,0 +1,38 @@
+{-
+Build a list by calling the supplied function on all `Natural` numbers from `0`
+up to but not including the supplied `Natural` number
+
+Examples:
+
+```
+./generate 5 Bool Natural/even = [ True, False, True, False, True ]
+
+./generate 0 Bool Natural/even = [] : List Bool
+```
+-}
+    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))
+            )
+
+in  generate

Prelude/List/head

@@ -0,0 +1,12 @@
+{-
+Retrieve the first element of the list
+
+Examples:
+
+```
+./head Natural [ 0, 1, 2 ] = Some 0
+
+./head Natural ([] : List Natural) = None Natural
+```
+-}
+let head : ∀(a : Type) → List a → Optional a = List/head in head

Prelude/List/indexed

@@ -0,0 +1,21 @@
+{-
+Tag each element of the list with its index
+
+Examples:
+
+```
+./indexed Bool [ True, False, True ]
+=   [   { index = 0, value = True  }
+    ,   { index = 1, value = False }
+    ,   { index = 2, value = True  }
+    ] : List { index : Natural, value : Bool }
+
+./indexed Bool ([] : List Bool)
+= [] : List { index : Natural, value : Bool }
+```
+-}
+    let indexed
+        : ∀(a : Type) → List a → List { index : Natural, value : a }
+        = List/indexed
+
+in  indexed

Prelude/List/iterate

@@ -0,0 +1,43 @@
+{-
+Generate a list of the specified length given a seed value and transition
+function
+
+Examples:
+
+```
+./iterate 10 Natural (λ(x : Natural) → x * 2) 1
+= [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
+
+./iterate 0 Natural (λ(x : Natural) → x * 2) 1
+= [] : List Natural
+```
+-}
+    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)
+                )
+            )
+
+in  iterate

Prelude/List/last

@@ -0,0 +1,12 @@
+{-
+Retrieve the last element of the list
+
+Examples:
+
+```
+./last Natural [ 0, 1, 2 ] = Some 2
+
+./last Natural ([] : List Natural) = None Natural
+```
+-}
+let last : ∀(a : Type) → List a → Optional a = List/last in last

Prelude/List/length

@@ -0,0 +1,12 @@
+{-
+Returns the number of elements in a list
+
+Examples:
+
+```
+./length Natural [ 0, 1, 2 ] = 3
+
+./length Natural ([] : List Natural) = 0
+```
+-}
+let length : ∀(a : Type) → List a → Natural = List/length in length

Prelude/List/map

@@ -0,0 +1,27 @@
+{-
+Transform a list by applying a function to each element
+
+Examples:
+
+```
+./map Natural Bool Natural/even [ 2, 3, 5 ]
+= [ True, False, False ]
+
+./map Natural Bool Natural/even ([] : List Natural)
+= [] : List Bool
+```
+-}
+    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))
+            )
+
+in  map

Prelude/List/null

@@ -0,0 +1,16 @@
+{-
+Returns `True` if the `List` is empty and `False` otherwise
+
+Examples:
+
+```
+./null Natural [ 0, 1, 2 ] = False
+
+./null Natural ([] : List Natural) = True
+```
+-}
+    let null
+        : ∀(a : Type) → List a → Bool
+        = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs)
+
+in  null

Prelude/List/package.dhall

@@ -0,0 +1,39 @@
+{ all =
+    ./all
+, any =
+    ./any
+, build =
+    ./build
+, concat =
+    ./concat
+, concatMap =
+    ./concatMap
+, filter =
+    ./filter
+, fold =
+    ./fold
+, generate =
+    ./generate
+, head =
+    ./head
+, indexed =
+    ./indexed
+, iterate =
+    ./iterate
+, last =
+    ./last
+, length =
+    ./length
+, map =
+    ./map
+, null =
+    ./null
+, replicate =
+    ./replicate
+, reverse =
+    ./reverse
+, shifted =
+    ./shifted
+, unzip =
+    ./unzip
+}

Prelude/List/replicate

@@ -0,0 +1,24 @@
+{-
+Build a list by copying the given element the specified number of times
+
+Examples:
+
+```
+./replicate 9 Natural 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
+
+./replicate 0 Natural 1 = [] : List Natural
+```
+-}
+    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)
+            )
+
+in  replicate

Prelude/List/reverse

@@ -0,0 +1,12 @@
+{-
+Reverse a list
+
+Examples:
+
+```
+./reverse Natural [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Natural
+
+./reverse Natural ([] : List Natural) = [] : List Natural
+```
+-}
+let reverse : ∀(a : Type) → List a → List a = List/reverse in reverse

Prelude/List/shifted

@@ -0,0 +1,90 @@
+{-
+Combine a `List` of `List`s, offsetting the `index` of each element by the
+number of elements in preceding lists
+
+Examples:
+
+```
+./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  }
+    ]
+
+./shifted Bool ([] : List (List { index : Natural, value : Bool }))
+= [] : List { index : Natural, value : Bool }
+```
+-}
+    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
+            )
+
+in  shifted

Prelude/List/unzip

@@ -0,0 +1,55 @@
+{-
+Unzip a `List` into two separate `List`s
+
+Examples:
+
+```
+./unzip
+Text
+Bool
+(   [   { _1 = "ABC", _2 = True  }
+    ,   { _1 = "DEF", _2 = False }
+    ,   { _1 = "GHI", _2 = True  }
+    ]
+)
+=   { _1 = [ "ABC", "DEF", "GHI" ]
+    , _2 = [ True, False, True ]
+    }
+
+./unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
+= { _1 = [] : List Text, _2 = [] : List Bool }
+```
+-}
+    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)
+                )
+            }
+
+in  unzip

Prelude/Monoid

@@ -0,0 +1,39 @@
+{-
+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

Prelude/Natural/build

@@ -0,0 +1,33 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build
+(   λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   succ (succ (succ zero))
+)
+= 3
+
+./build
+(   λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   zero
+)
+= 0
+```
+-}
+    let build
+        :   (   ∀(natural : Type)
+              → ∀(succ : natural → natural)
+              → ∀(zero : natural)
+              → natural
+            )
+          → Natural
+        = Natural/build
+
+in  build

Prelude/Natural/enumerate

@@ -0,0 +1,36 @@
+{-
+Generate a list of numbers from `0` up to but not including the specified
+number
+
+Examples:
+
+```
+./enumerate 10 = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]
+
+./enumerate 0 = [] : List Natural
+```
+-}
+    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)
+            )
+
+in  enumerate

Prelude/Natural/even

@@ -0,0 +1,12 @@
+{-
+Returns `True` if a number if even and returns `False` otherwise
+
+Examples:
+
+```
+./even 3 = False
+
+./even 0 = True
+```
+-}
+let even : Natural → Bool = Natural/even in even

Prelude/Natural/fold

@@ -0,0 +1,33 @@
+{-
+`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
+
+Examples:
+
+```
+./fold 3 Natural (λ(x : Natural) → 5 * x) 1 = 125
+
+λ(zero : Natural) → ./fold 3 Natural (λ(x : Natural) → 5 * x) zero
+= λ(zero : Natural) → 5 * (5 * (5 * zero))
+
+    λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   ./fold 3 natural succ zero
+=   λ(natural : Type)
+→   λ(succ : natural → natural)
+→   λ(zero : natural)
+→   succ (succ (succ zero))
+```
+-}
+    let fold
+        :   Natural
+          → ∀(natural : Type)
+          → ∀(succ : natural → natural)
+          → ∀(zero : natural)
+          → natural
+        = Natural/fold
+
+in  fold

Prelude/Natural/isZero

@@ -0,0 +1,12 @@
+{-
+Returns `True` if a number is `0` and returns `False` otherwise
+
+Examples:
+
+```
+./isZero 2 = False
+
+./isZero 0 = True
+```
+-}
+let isZero : Natural → Bool = Natural/isZero in isZero

Prelude/Natural/odd

@@ -0,0 +1,12 @@
+{-
+Returns `True` if a number is odd and returns `False` otherwise
+
+Examples:
+
+```
+./odd 3 = True
+
+./odd 0 = False
+```
+-}
+let odd : Natural → Bool = Natural/odd in odd

Prelude/Natural/package.dhall

@@ -0,0 +1,21 @@
+{ build =
+    ./build
+, enumerate =
+    ./enumerate
+, even =
+    ./even
+, fold =
+    ./fold
+, isZero =
+    ./isZero
+, odd =
+    ./odd
+, product =
+    ./product
+, sum =
+    ./sum
+, show =
+    ./show
+, toInteger =
+    ./toInteger
+}

Prelude/Natural/product

@@ -0,0 +1,22 @@
+{-
+Multiply all the numbers in a `List`
+
+Examples:
+
+```
+./product [ 2, 3, 5 ] = 30
+
+./product ([] : List Natural) = 1
+```
+-}
+    let product
+        : List Natural → Natural
+        =   λ(xs : List Natural)
+          → List/fold
+            Natural
+            xs
+            Natural
+            (λ(l : Natural) → λ(r : Natural) → l * r)
+            1
+
+in  product

Prelude/Natural/show

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

Prelude/Natural/sum

@@ -0,0 +1,22 @@
+{-
+Add all the numbers in a `List`
+
+Examples:
+
+```
+./sum [ 2, 3, 5 ] = 10
+
+./sum ([] : List Natural) = 0
+```
+-}
+    let sum
+        : List Natural → Natural
+        =   λ(xs : List Natural)
+          → List/fold
+            Natural
+            xs
+            Natural
+            (λ(l : Natural) → λ(r : Natural) → l + r)
+            0
+
+in  sum

Prelude/Natural/toDouble

@@ -0,0 +1,16 @@
+{-
+Convert a `Natural` number to the corresponding `Double`
+
+Examples:
+
+```
+./toDouble 3 = 3.0
+
+./toDouble 0 = 0.0
+```
+-}
+    let toDouble
+        : Natural → Double
+        = λ(n : Natural) → Integer/toDouble (Natural/toInteger n)
+
+in  toDouble

Prelude/Natural/toInteger

@@ -0,0 +1,12 @@
+{-
+Convert a `Natural` number to the corresponding `Integer`
+
+Examples:
+
+```
+./toInteger 3 = +3
+
+./toInteger 0 = +0
+```
+-}
+let toInteger : Natural → Integer = Natural/toInteger in toInteger

Prelude/Optional/all

@@ -0,0 +1,20 @@
+{-
+Returns `False` if the supplied function returns `False` for a present element
+and `True` otherwise:
+
+Examples:
+
+```
+./all Natural Natural/even (Some 3) = False
+
+./all Natural Natural/even (None Natural) = True
+```
+-}
+    let all
+        : ∀(a : Type) → (a → Bool) → Optional a → Bool
+        =   λ(a : Type)
+          → λ(f : a → Bool)
+          → λ(xs : Optional a)
+          → Optional/fold a xs Bool f True
+
+in  all

Prelude/Optional/any

@@ -0,0 +1,20 @@
+{-
+Returns `True` if the supplied function returns `True` for a present element and
+`False` otherwise
+
+Examples:
+
+```
+./any Natural Natural/even (Some 2) = True
+
+./any Natural Natural/even (None Natural) = False
+```
+-}
+    let any
+        : ∀(a : Type) → (a → Bool) → Optional a → Bool
+        =   λ(a : Type)
+          → λ(f : a → Bool)
+          → λ(xs : Optional a)
+          → Optional/fold a xs Bool f False
+
+in  any

Prelude/Optional/build

@@ -0,0 +1,36 @@
+{-
+`build` is the inverse of `fold`
+
+Examples:
+
+```
+./build
+Natural
+(   λ(optional : Type)
+→   λ(some : Natural → optional)
+→   λ(none : optional)
+→   some 1
+)
+= Some 1
+
+./build
+Natural
+(   λ(optional : Type)
+→   λ(some : Natural → optional)
+→   λ(none : optional)
+→   none
+)
+= None Natural
+```
+-}
+    let build
+        :   ∀(a : Type)
+          → (   ∀(optional : Type)
+              → ∀(some : a → optional)
+              → ∀(none : optional)
+              → optional
+            )
+          → Optional a
+        = Optional/build
+
+in  build

Prelude/Optional/concat

@@ -0,0 +1,28 @@
+{-
+Flatten two `Optional` layers into a single `Optional` layer
+
+Examples:
+
+```
+./concat Natural (Some (Some 1))
+= Some 1
+
+./concat Natural (Some (None Natural))
+= None Natural
+
+./concat Natural (None (Optional Natural))
+= None Natural
+```
+-}
+    let concat
+        : ∀(a : Type) → Optional (Optional a) → Optional a
+        =   λ(a : Type)
+          → λ(x : Optional (Optional a))
+          → Optional/fold
+            (Optional a)
+            x
+            (Optional a)
+            (λ(y : Optional a) → y)
+            (None a)
+
+in  concat

Prelude/Optional/filter

@@ -0,0 +1,32 @@
+{-
+Only keep an `Optional` element if the supplied function returns `True`
+
+Examples:
+
+```
+./filter Natural Natural/even (Some 2)
+= Some 2
+
+./filter Natural Natural/odd (Some 2)
+= None Natural
+```
+-}
+    let filter
+        : ∀(a : Type) → (a → Bool) → Optional a → Optional a
+        =   λ(a : Type)
+          → λ(f : a → Bool)
+          → λ(xs : Optional a)
+          → Optional/build
+            a
+            (   λ(optional : Type)
+              → λ(some : a → optional)
+              → λ(none : optional)
+              → Optional/fold
+                a
+                xs
+                optional
+                (λ(x : a) → if f x then some x else none)
+                none
+            )
+
+in  filter

Prelude/Optional/fold

@@ -0,0 +1,21 @@
+{-
+`fold` is the primitive function for consuming `Optional` values
+
+Examples:
+
+```
+./fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 = 2
+
+./fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 = 0
+```
+-}
+    let fold
+        :   ∀(a : Type)
+          → Optional a
+          → ∀(optional : Type)
+          → ∀(some : a → optional)
+          → ∀(none : optional)
+          → optional
+        = Optional/fold
+
+in  fold

Prelude/Optional/head

@@ -0,0 +1,28 @@
+{-
+Returns the first non-empty `Optional` value in a `List`
+
+Examples:
+
+```
+./head Natural [ None Natural, Some 1, Some 2 ] = Some 1
+
+./head Natural [ None Natural, None Natural ] = None Natural
+
+./head Natural ([] : List (Optional Natural)) = None Natural
+```
+-}
+    let head
+        : ∀(a : Type) → List (Optional a) → Optional a
+        =   λ(a : Type)
+          → λ(xs : List (Optional a))
+          → List/fold
+            (Optional a)
+            xs
+            (Optional a)
+            (   λ(l : Optional a)
+              → λ(r : Optional a)
+              → Optional/fold a l (Optional a) (λ(x : a) → Some x) r
+            )
+            (None a)
+
+in  head

Prelude/Optional/last

@@ -0,0 +1,28 @@
+{-
+Returns the last non-empty `Optional` value in a `List`
+
+Examples:
+
+```
+./last Natural [ None Natural, Some 1, Some 2 ] = Some 2
+
+./last Natural [ None Natural, None Natural ] = None Natural
+
+./last Natural ([] : List (Optional Natural)) = None Natural
+```
+-}
+    let last
+        : ∀(a : Type) → List (Optional a) → Optional a
+        =   λ(a : Type)
+          → λ(xs : List (Optional a))
+          → List/fold
+            (Optional a)
+            xs
+            (Optional a)
+            (   λ(l : Optional a)
+              → λ(r : Optional a)
+              → Optional/fold a r (Optional a) (λ(x : a) → Some x) l
+            )
+            (None a)
+
+in  last

Prelude/Optional/length

@@ -0,0 +1,18 @@
+{-
+Returns `1` if the `Optional` value is present and `0` if the value is absent
+
+Examples:
+
+```
+./length Natural (Some 2) = 1
+
+./length Natural (None Natural) = 0
+```
+-}
+    let length
+        : ∀(a : Type) → Optional a → Natural
+        =   λ(a : Type)
+          → λ(xs : Optional a)
+          → Optional/fold a xs Natural (λ(_ : a) → 1) 0
+
+in  length

Prelude/Optional/map

@@ -0,0 +1,20 @@
+{-
+Transform an `Optional` value with a function
+
+Examples:
+
+```
+./map Natural Bool Natural/even (Some 3) = Some False
+
+./map Natural Bool Natural/even (None Natural) = None Bool
+```
+-}
+    let map
+        : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b
+        =   λ(a : Type)
+          → λ(b : Type)
+          → λ(f : a → b)
+          → λ(o : Optional a)
+          → Optional/fold a o (Optional b) (λ(x : a) → Some (f x)) (None b)
+
+in  map

Prelude/Optional/null

@@ -0,0 +1,18 @@
+{-
+Returns `True` if the `Optional` value is absent and `False` if present
+
+Examples:
+
+```
+./null Natural (Some 2) = False
+
+./null Natural (None Natural) = True
+```
+-}
+    let null
+        : ∀(a : Type) → Optional a → Bool
+        =   λ(a : Type)
+          → λ(xs : Optional a)
+          → Optional/fold a xs Bool (λ(_ : a) → False) True
+
+in  null

Prelude/Optional/package.dhall

@@ -0,0 +1,27 @@
+{ all =
+    ./all
+, any =
+    ./any
+, build =
+    ./build
+, concat =
+    ./concat
+, filter =
+    ./filter
+, fold =
+    ./fold
+, head =
+    ./head
+, last =
+    ./last
+, length =
+    ./length
+, map =
+    ./map
+, null =
+    ./null
+, toList =
+    ./toList
+, unzip =
+    ./unzip
+}

Prelude/Optional/toList

@@ -0,0 +1,18 @@
+{-
+Convert an `Optional` value into the equivalent `List`
+
+Examples:
+
+```
+./toList Natural (Some 1) = [ 1 ]
+
+./toList Natural (None Natural) = [] : List Natural
+```
+-}
+    let toList
+        : ∀(a : Type) → Optional a → List a
+        =   λ(a : Type)
+          → λ(o : Optional a)
+          → Optional/fold a o (List a) (λ(x : a) → [ x ] : List a) ([] : List a)
+
+in  toList

Prelude/Optional/unzip

@@ -0,0 +1,38 @@
+{-
+Unzip an `Optional` value into two separate `Optional` values
+
+Examples:
+
+```
+./unzip Text Bool (Some { _1 = "ABC", _2 = True  })
+= { _1 = Some "ABC", _2 = Some True }
+
+./unzip Text Bool (None { _1 : Text, _2 : Bool })
+= { _1 = None Text, _2 = None Bool }
+```
+-}
+    let unzip
+        :   ∀(a : Type)
+          → ∀(b : Type)
+          → Optional { _1 : a, _2 : b }
+          → { _1 : Optional a, _2 : Optional b }
+        =   λ(a : Type)
+          → λ(b : Type)
+          → λ(xs : Optional { _1 : a, _2 : b })
+          → { _1 =
+                Optional/fold
+                { _1 : a, _2 : b }
+                xs
+                (Optional a)
+                (λ(x : { _1 : a, _2 : b }) → Some x._1)
+                (None a)
+            , _2 =
+                Optional/fold
+                { _1 : a, _2 : b }
+                xs
+                (Optional b)
+                (λ(x : { _1 : a, _2 : b }) → Some x._2)
+                (None b)
+            }
+
+in  unzip

Prelude/Text/concat

@@ -0,0 +1,17 @@
+{-
+Concatenate all the `Text` values in a `List`
+
+Examples:
+
+```
+./concat [ "ABC", "DEF", "GHI" ] = "ABCDEFGHI"
+
+./concat ([] : List Text) = ""
+```
+-}
+    let concat
+        : List Text → Text
+        =   λ(xs : List Text)
+          → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) ""
+
+in  concat

Prelude/Text/concatMap

@@ -0,0 +1,21 @@
+{-
+Transform each value in a `List` into `Text` and concatenate the result
+
+Examples:
+
+```
+./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ]
+= "0 1 2 "
+
+./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural)
+= ""
+```
+-}
+    let concatMap
+        : ∀(a : Type) → (a → Text) → List a → Text
+        =   λ(a : Type)
+          → λ(f : a → Text)
+          → λ(xs : List a)
+          → List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) ""
+
+in  concatMap

Prelude/Text/concatMapSep

@@ -0,0 +1,47 @@
+{-
+Transform each value in a `List` to `Text` and then concatenate them with a
+separator in between each value
+
+Examples:
+
+```
+./concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] = "0, 1, 2"
+
+./concatMapSep ", " Natural Natural/show ([] : List Natural) = ""
+```
+-}
+    let concatMapSep
+        : ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text
+        =   λ(separator : Text)
+          → λ(a : Type)
+          → λ(f : a → Text)
+          → λ(elements : List a)
+          →     let status =
+                      List/fold
+                      a
+                      elements
+                      < Empty : {} | NonEmpty : Text >
+                      (   λ(element : a)
+                        → λ(status : < Empty : {} | NonEmpty : Text >)
+                        → merge
+                          { Empty =
+                              λ(_ : {}) → < NonEmpty = f element | Empty : {} >
+                          , NonEmpty =
+                                λ(result : Text)
+                              → < NonEmpty =
+                                    f element ++ separator ++ result
+                                | Empty :
+                                    {}
+                                >
+                          }
+                          status
+                          : < Empty : {} | NonEmpty : Text >
+                      )
+                      < Empty = {=} | NonEmpty : Text >
+            
+            in  merge
+                { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result }
+                status
+                : Text
+
+in  concatMapSep

Prelude/Text/concatSep

@@ -0,0 +1,44 @@
+{-
+Concatenate a `List` of `Text` values with a separator in between each value
+
+Examples:
+
+```
+./concatSep ", " [ "ABC", "DEF", "GHI" ] = "ABC, DEF, GHI"
+
+./concatSep ", " ([] : List Text) = ""
+```
+-}
+    let concatSep
+        : ∀(separator : Text) → ∀(elements : List Text) → Text
+        =   λ(separator : Text)
+          → λ(elements : List Text)
+          →     let status =
+                      List/fold
+                      Text
+                      elements
+                      < Empty : {} | NonEmpty : Text >
+                      (   λ(element : Text)
+                        → λ(status : < Empty : {} | NonEmpty : Text >)
+                        → merge
+                          { Empty =
+                              λ(_ : {}) → < NonEmpty = element | Empty : {} >
+                          , NonEmpty =
+                                λ(result : Text)
+                              → < NonEmpty =
+                                    element ++ separator ++ result
+                                | Empty :
+                                    {}
+                                >
+                          }
+                          status
+                          : < Empty : {} | NonEmpty : Text >
+                      )
+                      < Empty = {=} | NonEmpty : Text >
+            
+            in  merge
+                { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result }
+                status
+                : Text
+
+in  concatSep

Prelude/Text/package.dhall

@@ -0,0 +1,9 @@
+{ concat =
+    ./concat
+, concatMap =
+    ./concatMap
+, concatMapSep =
+    ./concatMapSep
+, concatSep =
+    ./concatSep
+}

Prelude/package.dhall

@@ -0,0 +1,19 @@
+{ `Bool` =
+    ./Bool/package.dhall
+, `Double` =
+    ./Double/package.dhall
+, Function =
+    ./Function/package.dhall
+, `Integer` =
+    ./Integer/package.dhall
+, `List` =
+    ./List/package.dhall
+, `Natural` =
+    ./Natural/package.dhall
+, `Optional` =
+    ./Optional/package.dhall
+, JSON =
+    ./JSON/package.dhall
+, `Text` =
+    ./Text/package.dhall
+}

api/Deployment/mkDeployment

@@ -1,5 +1,5 @@
 -- Prelude
-   let Prelude = https://raw.githubusercontent.com/dhall-lang/Prelude/master/package.dhall
+   let Prelude = ../../Prelude/package.dhall
 in let map  = Prelude.`List`.map
 in let kv   = Prelude.JSON.keyText