diff --git a/Prelude/Bool/and b/Prelude/Bool/and new file mode 100644 index 0000000..3d86338 --- /dev/null +++ b/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 diff --git a/Prelude/Bool/build b/Prelude/Bool/build new file mode 100644 index 0000000..85ca484 --- /dev/null +++ b/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 diff --git a/Prelude/Bool/even b/Prelude/Bool/even new file mode 100644 index 0000000..b4eb5e9 --- /dev/null +++ b/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 diff --git a/Prelude/Bool/fold b/Prelude/Bool/fold new file mode 100644 index 0000000..e8e2b56 --- /dev/null +++ b/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 diff --git a/Prelude/Bool/not b/Prelude/Bool/not new file mode 100644 index 0000000..c0599a6 --- /dev/null +++ b/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 diff --git a/Prelude/Bool/odd b/Prelude/Bool/odd new file mode 100644 index 0000000..8ad485a --- /dev/null +++ b/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 diff --git a/Prelude/Bool/or b/Prelude/Bool/or new file mode 100644 index 0000000..e3ae1e2 --- /dev/null +++ b/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 diff --git a/Prelude/Bool/package.dhall b/Prelude/Bool/package.dhall new file mode 100644 index 0000000..c776940 --- /dev/null +++ b/Prelude/Bool/package.dhall @@ -0,0 +1,17 @@ +{ and = + ./and +, build = + ./build +, even = + ./even +, fold = + ./fold +, not = + ./not +, odd = + ./odd +, or = + ./or +, show = + ./show +} diff --git a/Prelude/Bool/show b/Prelude/Bool/show new file mode 100644 index 0000000..1801875 --- /dev/null +++ b/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 diff --git a/Prelude/Double/package.dhall b/Prelude/Double/package.dhall new file mode 100644 index 0000000..46f0272 --- /dev/null +++ b/Prelude/Double/package.dhall @@ -0,0 +1 @@ +{ show = ./show } diff --git a/Prelude/Double/show b/Prelude/Double/show new file mode 100644 index 0000000..36aae65 --- /dev/null +++ b/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 diff --git a/Prelude/Function/compose b/Prelude/Function/compose new file mode 100644 index 0000000..bae6a66 --- /dev/null +++ b/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 diff --git a/Prelude/Function/package.dhall b/Prelude/Function/package.dhall new file mode 100644 index 0000000..ecb64da --- /dev/null +++ b/Prelude/Function/package.dhall @@ -0,0 +1 @@ +{ compose = ./compose } diff --git a/Prelude/Integer/package.dhall b/Prelude/Integer/package.dhall new file mode 100644 index 0000000..46f0272 --- /dev/null +++ b/Prelude/Integer/package.dhall @@ -0,0 +1 @@ +{ show = ./show } diff --git a/Prelude/Integer/show b/Prelude/Integer/show new file mode 100644 index 0000000..13b6eb8 --- /dev/null +++ b/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 diff --git a/Prelude/Integer/toDouble b/Prelude/Integer/toDouble new file mode 100644 index 0000000..8b30c78 --- /dev/null +++ b/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 diff --git a/Prelude/JSON/Nesting b/Prelude/JSON/Nesting new file mode 100644 index 0000000..bf0de50 --- /dev/null +++ b/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 diff --git a/Prelude/JSON/Tagged b/Prelude/JSON/Tagged new file mode 100644 index 0000000..9b731d6 --- /dev/null +++ b/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 diff --git a/Prelude/JSON/keyText b/Prelude/JSON/keyText new file mode 100644 index 0000000..eabb77d --- /dev/null +++ b/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 diff --git a/Prelude/JSON/keyValue b/Prelude/JSON/keyValue new file mode 100644 index 0000000..0e5e362 --- /dev/null +++ b/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 diff --git a/Prelude/JSON/package.dhall b/Prelude/JSON/package.dhall new file mode 100644 index 0000000..9c4b605 --- /dev/null +++ b/Prelude/JSON/package.dhall @@ -0,0 +1 @@ +{ keyText = ./keyText, keyValue = ./keyValue } diff --git a/Prelude/List/all b/Prelude/List/all new file mode 100644 index 0000000..f7456d9 --- /dev/null +++ b/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 diff --git a/Prelude/List/any b/Prelude/List/any new file mode 100644 index 0000000..225da84 --- /dev/null +++ b/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 diff --git a/Prelude/List/build b/Prelude/List/build new file mode 100644 index 0000000..c05572e --- /dev/null +++ b/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 diff --git a/Prelude/List/concat b/Prelude/List/concat new file mode 100644 index 0000000..2f7291b --- /dev/null +++ b/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 diff --git a/Prelude/List/concatMap b/Prelude/List/concatMap new file mode 100644 index 0000000..f54f491 --- /dev/null +++ b/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 diff --git a/Prelude/List/filter b/Prelude/List/filter new file mode 100644 index 0000000..3edeb58 --- /dev/null +++ b/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 diff --git a/Prelude/List/fold b/Prelude/List/fold new file mode 100644 index 0000000..5307ea7 --- /dev/null +++ b/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 diff --git a/Prelude/List/generate b/Prelude/List/generate new file mode 100644 index 0000000..3397fa8 --- /dev/null +++ b/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 diff --git a/Prelude/List/head b/Prelude/List/head new file mode 100644 index 0000000..0e2186e --- /dev/null +++ b/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 diff --git a/Prelude/List/indexed b/Prelude/List/indexed new file mode 100644 index 0000000..06bb227 --- /dev/null +++ b/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 diff --git a/Prelude/List/iterate b/Prelude/List/iterate new file mode 100644 index 0000000..fd6e11d --- /dev/null +++ b/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 diff --git a/Prelude/List/last b/Prelude/List/last new file mode 100644 index 0000000..ca0cf7b --- /dev/null +++ b/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 diff --git a/Prelude/List/length b/Prelude/List/length new file mode 100644 index 0000000..397d0ce --- /dev/null +++ b/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 diff --git a/Prelude/List/map b/Prelude/List/map new file mode 100644 index 0000000..e82c40d --- /dev/null +++ b/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 diff --git a/Prelude/List/null b/Prelude/List/null new file mode 100644 index 0000000..e38f925 --- /dev/null +++ b/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 diff --git a/Prelude/List/package.dhall b/Prelude/List/package.dhall new file mode 100644 index 0000000..9555bbb --- /dev/null +++ b/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 +} diff --git a/Prelude/List/replicate b/Prelude/List/replicate new file mode 100644 index 0000000..3f2fede --- /dev/null +++ b/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 diff --git a/Prelude/List/reverse b/Prelude/List/reverse new file mode 100644 index 0000000..bed5ddc --- /dev/null +++ b/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 diff --git a/Prelude/List/shifted b/Prelude/List/shifted new file mode 100644 index 0000000..80551dc --- /dev/null +++ b/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 diff --git a/Prelude/List/unzip b/Prelude/List/unzip new file mode 100644 index 0000000..8293ced --- /dev/null +++ b/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 diff --git a/Prelude/Monoid b/Prelude/Monoid new file mode 100644 index 0000000..fe5bd7a --- /dev/null +++ b/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 diff --git a/Prelude/Natural/build b/Prelude/Natural/build new file mode 100644 index 0000000..a01ef7e --- /dev/null +++ b/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 diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate new file mode 100644 index 0000000..c90612f --- /dev/null +++ b/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 diff --git a/Prelude/Natural/even b/Prelude/Natural/even new file mode 100644 index 0000000..b9e7b1e --- /dev/null +++ b/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 diff --git a/Prelude/Natural/fold b/Prelude/Natural/fold new file mode 100644 index 0000000..2150d3e --- /dev/null +++ b/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 diff --git a/Prelude/Natural/isZero b/Prelude/Natural/isZero new file mode 100644 index 0000000..0811317 --- /dev/null +++ b/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 diff --git a/Prelude/Natural/odd b/Prelude/Natural/odd new file mode 100644 index 0000000..54d5090 --- /dev/null +++ b/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 diff --git a/Prelude/Natural/package.dhall b/Prelude/Natural/package.dhall new file mode 100644 index 0000000..513cb97 --- /dev/null +++ b/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 +} diff --git a/Prelude/Natural/product b/Prelude/Natural/product new file mode 100644 index 0000000..dcc5235 --- /dev/null +++ b/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 diff --git a/Prelude/Natural/show b/Prelude/Natural/show new file mode 100644 index 0000000..3e9e6be --- /dev/null +++ b/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 diff --git a/Prelude/Natural/sum b/Prelude/Natural/sum new file mode 100644 index 0000000..0f0f697 --- /dev/null +++ b/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 diff --git a/Prelude/Natural/toDouble b/Prelude/Natural/toDouble new file mode 100644 index 0000000..12f9392 --- /dev/null +++ b/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 diff --git a/Prelude/Natural/toInteger b/Prelude/Natural/toInteger new file mode 100644 index 0000000..1d53874 --- /dev/null +++ b/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 diff --git a/Prelude/Optional/all b/Prelude/Optional/all new file mode 100644 index 0000000..0db2c8f --- /dev/null +++ b/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 diff --git a/Prelude/Optional/any b/Prelude/Optional/any new file mode 100644 index 0000000..172cebc --- /dev/null +++ b/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 diff --git a/Prelude/Optional/build b/Prelude/Optional/build new file mode 100644 index 0000000..dde5fa6 --- /dev/null +++ b/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 diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat new file mode 100644 index 0000000..8bbd36f --- /dev/null +++ b/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 diff --git a/Prelude/Optional/filter b/Prelude/Optional/filter new file mode 100644 index 0000000..3c0d4eb --- /dev/null +++ b/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 diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold new file mode 100644 index 0000000..602fba2 --- /dev/null +++ b/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 diff --git a/Prelude/Optional/head b/Prelude/Optional/head new file mode 100644 index 0000000..9cbce3c --- /dev/null +++ b/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 diff --git a/Prelude/Optional/last b/Prelude/Optional/last new file mode 100644 index 0000000..8c70d9e --- /dev/null +++ b/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 diff --git a/Prelude/Optional/length b/Prelude/Optional/length new file mode 100644 index 0000000..c8df433 --- /dev/null +++ b/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 diff --git a/Prelude/Optional/map b/Prelude/Optional/map new file mode 100644 index 0000000..d08329e --- /dev/null +++ b/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 diff --git a/Prelude/Optional/null b/Prelude/Optional/null new file mode 100644 index 0000000..6854edb --- /dev/null +++ b/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 diff --git a/Prelude/Optional/package.dhall b/Prelude/Optional/package.dhall new file mode 100644 index 0000000..97a4d0c --- /dev/null +++ b/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 +} diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList new file mode 100644 index 0000000..6dc7ccb --- /dev/null +++ b/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 diff --git a/Prelude/Optional/unzip b/Prelude/Optional/unzip new file mode 100644 index 0000000..af4b99f --- /dev/null +++ b/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 diff --git a/Prelude/Text/concat b/Prelude/Text/concat new file mode 100644 index 0000000..7f14e5a --- /dev/null +++ b/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 diff --git a/Prelude/Text/concatMap b/Prelude/Text/concatMap new file mode 100644 index 0000000..86db318 --- /dev/null +++ b/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 diff --git a/Prelude/Text/concatMapSep b/Prelude/Text/concatMapSep new file mode 100644 index 0000000..5d5b0be --- /dev/null +++ b/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 diff --git a/Prelude/Text/concatSep b/Prelude/Text/concatSep new file mode 100644 index 0000000..d25df38 --- /dev/null +++ b/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 diff --git a/Prelude/Text/package.dhall b/Prelude/Text/package.dhall new file mode 100644 index 0000000..863d06c --- /dev/null +++ b/Prelude/Text/package.dhall @@ -0,0 +1,9 @@ +{ concat = + ./concat +, concatMap = + ./concatMap +, concatMapSep = + ./concatMapSep +, concatSep = + ./concatSep +} diff --git a/Prelude/package.dhall b/Prelude/package.dhall new file mode 100644 index 0000000..7b88b79 --- /dev/null +++ b/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 +} diff --git a/api/Deployment/mkDeployment b/api/Deployment/mkDeployment index 2f042e0..7b9828d 100644 --- a/api/Deployment/mkDeployment +++ b/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