From c74b46c3e8a65c2ded6ebf5082a454e6f00f43a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Charlotte=20=F0=9F=A6=9D=20Delenk?= Date: Thu, 1 Sep 2022 19:37:49 +0100 Subject: [PATCH] Add List/ --- Integer/package.dhall | 2 +- List/all.dhall | 16 ++++++++ List/any.dhall | 16 ++++++++ List/build.dhall | 30 ++++++++++++++ List/concat.dhall | 34 ++++++++++++++++ List/concatMap.dhall | 32 +++++++++++++++ List/default.dhall | 10 +++++ List/drop.dhall | 25 ++++++++++++ List/empty.dhall | 8 ++++ List/filter.dhall | 22 ++++++++++ List/filterMap.dhall | 13 ++++++ List/fold.dhall | 43 ++++++++++++++++++++ List/foldLeft.dhall | 60 +++++++++++++++++++++++++++ List/generate.dhall | 35 ++++++++++++++++ List/head.dhall | 10 +++++ List/index.dhall | 15 +++++++ List/indexed.dhall | 19 +++++++++ List/iterate.dhall | 42 +++++++++++++++++++ List/last.dhall | 10 +++++ List/length.dhall | 10 +++++ List/map.dhall | 23 +++++++++++ List/null.dhall | 10 +++++ List/package.dhall | 31 ++++++++++++++ List/replicate.dhall | 18 +++++++++ List/reverse.dhall | 11 +++++ List/shifted.dhall | 83 ++++++++++++++++++++++++++++++++++++++ List/take.dhall | 23 +++++++++++ List/unpackOptionals.dhall | 8 ++++ List/unzip.dhall | 50 +++++++++++++++++++++++ List/zip.dhall | 36 +++++++++++++++++ Number/package.dhall | 2 +- Optional/default.dhall | 13 ++++++ Optional/fold.dhall | 36 +++++++++++++++++ Optional/map.dhall | 22 +--------- Optional/toList.dhall | 6 +++ Optional/unwrap.dhall | 8 ++++ package.dhall | 1 + 37 files changed, 811 insertions(+), 22 deletions(-) create mode 100644 List/all.dhall create mode 100644 List/any.dhall create mode 100644 List/build.dhall create mode 100644 List/concat.dhall create mode 100644 List/concatMap.dhall create mode 100644 List/default.dhall create mode 100644 List/drop.dhall create mode 100644 List/empty.dhall create mode 100644 List/filter.dhall create mode 100644 List/filterMap.dhall create mode 100644 List/fold.dhall create mode 100644 List/foldLeft.dhall create mode 100644 List/generate.dhall create mode 100644 List/head.dhall create mode 100644 List/index.dhall create mode 100644 List/indexed.dhall create mode 100644 List/iterate.dhall create mode 100644 List/last.dhall create mode 100644 List/length.dhall create mode 100644 List/map.dhall create mode 100644 List/null.dhall create mode 100644 List/package.dhall create mode 100644 List/replicate.dhall create mode 100644 List/reverse.dhall create mode 100644 List/shifted.dhall create mode 100644 List/take.dhall create mode 100644 List/unpackOptionals.dhall create mode 100644 List/unzip.dhall create mode 100644 List/zip.dhall create mode 100644 Optional/default.dhall create mode 100644 Optional/fold.dhall create mode 100644 Optional/toList.dhall create mode 100644 Optional/unwrap.dhall diff --git a/Integer/package.dhall b/Integer/package.dhall index 75fb079..7fcbaed 100644 --- a/Integer/package.dhall +++ b/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 diff --git a/List/all.dhall b/List/all.dhall new file mode 100644 index 0000000..11b1613 --- /dev/null +++ b/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 diff --git a/List/any.dhall b/List/any.dhall new file mode 100644 index 0000000..130bf0b --- /dev/null +++ b/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 diff --git a/List/build.dhall b/List/build.dhall new file mode 100644 index 0000000..c59c3c5 --- /dev/null +++ b/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 diff --git a/List/concat.dhall b/List/concat.dhall new file mode 100644 index 0000000..ee17d84 --- /dev/null +++ b/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 diff --git a/List/concatMap.dhall b/List/concatMap.dhall new file mode 100644 index 0000000..4cc2e77 --- /dev/null +++ b/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 diff --git a/List/default.dhall b/List/default.dhall new file mode 100644 index 0000000..0d9bf6d --- /dev/null +++ b/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 diff --git a/List/drop.dhall b/List/drop.dhall new file mode 100644 index 0000000..329c752 --- /dev/null +++ b/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 diff --git a/List/empty.dhall b/List/empty.dhall new file mode 100644 index 0000000..fe66a71 --- /dev/null +++ b/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 diff --git a/List/filter.dhall b/List/filter.dhall new file mode 100644 index 0000000..6b2a63f --- /dev/null +++ b/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 diff --git a/List/filterMap.dhall b/List/filterMap.dhall new file mode 100644 index 0000000..5a4e722 --- /dev/null +++ b/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 diff --git a/List/fold.dhall b/List/fold.dhall new file mode 100644 index 0000000..ee8b8e9 --- /dev/null +++ b/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 diff --git a/List/foldLeft.dhall b/List/foldLeft.dhall new file mode 100644 index 0000000..c943877 --- /dev/null +++ b/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 diff --git a/List/generate.dhall b/List/generate.dhall new file mode 100644 index 0000000..2afdeb7 --- /dev/null +++ b/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 diff --git a/List/head.dhall b/List/head.dhall new file mode 100644 index 0000000..a50f692 --- /dev/null +++ b/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 diff --git a/List/index.dhall b/List/index.dhall new file mode 100644 index 0000000..6e19329 --- /dev/null +++ b/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 diff --git a/List/indexed.dhall b/List/indexed.dhall new file mode 100644 index 0000000..20500e1 --- /dev/null +++ b/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 diff --git a/List/iterate.dhall b/List/iterate.dhall new file mode 100644 index 0000000..02fed82 --- /dev/null +++ b/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 diff --git a/List/last.dhall b/List/last.dhall new file mode 100644 index 0000000..2e695fb --- /dev/null +++ b/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 diff --git a/List/length.dhall b/List/length.dhall new file mode 100644 index 0000000..1238fd5 --- /dev/null +++ b/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 diff --git a/List/map.dhall b/List/map.dhall new file mode 100644 index 0000000..70fc570 --- /dev/null +++ b/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 diff --git a/List/null.dhall b/List/null.dhall new file mode 100644 index 0000000..fd11976 --- /dev/null +++ b/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 diff --git a/List/package.dhall b/List/package.dhall new file mode 100644 index 0000000..f845798 --- /dev/null +++ b/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 + } diff --git a/List/replicate.dhall b/List/replicate.dhall new file mode 100644 index 0000000..90bfbd0 --- /dev/null +++ b/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 diff --git a/List/reverse.dhall b/List/reverse.dhall new file mode 100644 index 0000000..d958987 --- /dev/null +++ b/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 diff --git a/List/shifted.dhall b/List/shifted.dhall new file mode 100644 index 0000000..0db406d --- /dev/null +++ b/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 diff --git a/List/take.dhall b/List/take.dhall new file mode 100644 index 0000000..da66287 --- /dev/null +++ b/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 diff --git a/List/unpackOptionals.dhall b/List/unpackOptionals.dhall new file mode 100644 index 0000000..665a189 --- /dev/null +++ b/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 diff --git a/List/unzip.dhall b/List/unzip.dhall new file mode 100644 index 0000000..3ce4f76 --- /dev/null +++ b/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 diff --git a/List/zip.dhall b/List/zip.dhall new file mode 100644 index 0000000..8bc25b4 --- /dev/null +++ b/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 diff --git a/Number/package.dhall b/Number/package.dhall index beb9eb3..d5d4235 100644 --- a/Number/package.dhall +++ b/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 diff --git a/Optional/default.dhall b/Optional/default.dhall new file mode 100644 index 0000000..cfd37d0 --- /dev/null +++ b/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 diff --git a/Optional/fold.dhall b/Optional/fold.dhall new file mode 100644 index 0000000..f2900cc --- /dev/null +++ b/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 diff --git a/Optional/map.dhall b/Optional/map.dhall index 2741e00..7ee91e1 100644 --- a/Optional/map.dhall +++ b/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 diff --git a/Optional/toList.dhall b/Optional/toList.dhall new file mode 100644 index 0000000..4ded163 --- /dev/null +++ b/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) diff --git a/Optional/unwrap.dhall b/Optional/unwrap.dhall new file mode 100644 index 0000000..1c6523f --- /dev/null +++ b/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 diff --git a/package.dhall b/package.dhall index 14b63ea..ee7b7e9 100644 --- a/package.dhall +++ b/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