From 8fc7b60c0e9c438413816899ea77f09ce68736b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Charlotte=20=F0=9F=A6=9D=20Delenk?= Date: Thu, 1 Sep 2022 20:25:02 +0100 Subject: [PATCH] Import NonEmpty/ --- NonEmpty/Type.dhall | 9 ++++ NonEmpty/all.dhall | 28 +++++++++++++ NonEmpty/any.dhall | 28 +++++++++++++ NonEmpty/concat.dhall | 52 +++++++++++++++++++++++ NonEmpty/concatMap.dhall | 47 +++++++++++++++++++++ NonEmpty/head.dhall | 10 +++++ NonEmpty/index.dhall | 27 ++++++++++++ NonEmpty/indexed.dhall | 35 ++++++++++++++++ NonEmpty/last.dhall | 12 ++++++ NonEmpty/length.dhall | 13 ++++++ NonEmpty/make.dhall | 15 +++++++ NonEmpty/map.dhall | 24 +++++++++++ NonEmpty/package.dhall | 20 +++++++++ NonEmpty/reverse.dhall | 21 ++++++++++ NonEmpty/shifted.dhall | 89 ++++++++++++++++++++++++++++++++++++++++ NonEmpty/singleton.dhall | 11 +++++ NonEmpty/toList.dhall | 14 +++++++ NonEmpty/unzip.dhall | 52 +++++++++++++++++++++++ NonEmpty/zip.dhall | 20 +++++++++ package.dhall | 1 + 20 files changed, 528 insertions(+) create mode 100644 NonEmpty/Type.dhall create mode 100644 NonEmpty/all.dhall create mode 100644 NonEmpty/any.dhall create mode 100644 NonEmpty/concat.dhall create mode 100644 NonEmpty/concatMap.dhall create mode 100644 NonEmpty/head.dhall create mode 100644 NonEmpty/index.dhall create mode 100644 NonEmpty/indexed.dhall create mode 100644 NonEmpty/last.dhall create mode 100644 NonEmpty/length.dhall create mode 100644 NonEmpty/make.dhall create mode 100644 NonEmpty/map.dhall create mode 100644 NonEmpty/package.dhall create mode 100644 NonEmpty/reverse.dhall create mode 100644 NonEmpty/shifted.dhall create mode 100644 NonEmpty/singleton.dhall create mode 100644 NonEmpty/toList.dhall create mode 100644 NonEmpty/unzip.dhall create mode 100644 NonEmpty/zip.dhall diff --git a/NonEmpty/Type.dhall b/NonEmpty/Type.dhall new file mode 100644 index 0000000..300bb67 --- /dev/null +++ b/NonEmpty/Type.dhall @@ -0,0 +1,9 @@ +{-| +A `NonEmpty` list has at least one element and supports many of the same +operations as `List`s +-} +let NonEmpty + : Type → Type + = λ(a : Type) → { head : a, tail : List a } + +in NonEmpty diff --git a/NonEmpty/all.dhall b/NonEmpty/all.dhall new file mode 100644 index 0000000..9398e95 --- /dev/null +++ b/NonEmpty/all.dhall @@ -0,0 +1,28 @@ +{-| +Returns `True` if the supplied function returns `True` for all elements in the +`NonEmpty` list +-} +let NonEmpty = ./Type.dhall + +let NonEmpty/toList = ./toList.dhall + +let all + : ∀(a : Type) → (a → Bool) → NonEmpty a → Bool + = λ(a : Type) → + λ(f : a → Bool) → + λ(xs : NonEmpty a) → + List/fold + a + (NonEmpty/toList a xs) + Bool + (λ(x : a) → λ(r : Bool) → f x && r) + True + +let example0 = + assert : all Natural Natural/even { head = 2, tail = [ 3, 5 ] } ≡ False + +let example1 = + assert + : all Natural Natural/even { head = 2, tail = [] : List Natural } ≡ True + +in all diff --git a/NonEmpty/any.dhall b/NonEmpty/any.dhall new file mode 100644 index 0000000..8245ee2 --- /dev/null +++ b/NonEmpty/any.dhall @@ -0,0 +1,28 @@ +{-| +Returns `True` if the supplied function returns `True` for any element in the +`NonEmpty` list +-} +let NonEmpty = ./Type.dhall + +let NonEmpty/toList = ./toList.dhall + +let any + : ∀(a : Type) → (a → Bool) → NonEmpty a → Bool + = λ(a : Type) → + λ(f : a → Bool) → + λ(xs : NonEmpty a) → + List/fold + a + (NonEmpty/toList a xs) + Bool + (λ(x : a) → λ(r : Bool) → f x || r) + False + +let example0 = + assert : any Natural Natural/even { head = 2, tail = [ 3, 5 ] } ≡ True + +let example1 = + assert + : any Natural Natural/even { head = 3, tail = [] : List Natural } ≡ False + +in any diff --git a/NonEmpty/concat.dhall b/NonEmpty/concat.dhall new file mode 100644 index 0000000..d696302 --- /dev/null +++ b/NonEmpty/concat.dhall @@ -0,0 +1,52 @@ +{-| +Concatenate a `NonEmpty` list of `NonEmpty` lists into a single `NonEmpty` +list +-} +let NonEmpty = ./Type.dhall + +let NonEmpty/toList = ./toList.dhall + +let List/concatMap = ../List/concatMap.dhall + +let concat + : ∀(a : Type) → NonEmpty (NonEmpty a) → NonEmpty a + = λ(a : Type) → + λ(xss : NonEmpty (NonEmpty a)) → + { head = xss.head.head + , tail = + xss.head.tail + # List/concatMap (NonEmpty a) a (NonEmpty/toList a) xss.tail + } + +let example0 = + assert + : concat + Natural + { head = { head = 0, tail = [ 1, 2 ] } + , tail = + [ { head = 3, tail = [ 4 ] }, { head = 5, tail = [ 6, 7, 8 ] } ] + } + ≡ { head = 0, tail = [ 1, 2, 3, 4, 5, 6, 7, 8 ] } + +let example1 = + assert + : concat + Natural + { head = { head = 0, tail = [] : List Natural } + , tail = + [ { head = 1, tail = [] : List Natural } + , { head = 2, tail = [] : List Natural } + ] + } + ≡ { head = 0, tail = [ 1, 2 ] : List Natural } + +let example2 = + assert + : concat + Natural + { head = { head = 0, tail = [] : List Natural } + , tail = [] : List (NonEmpty Natural) + } + ≡ { head = 0, tail = [] : List Natural } + +in concat diff --git a/NonEmpty/concatMap.dhall b/NonEmpty/concatMap.dhall new file mode 100644 index 0000000..acf0eba --- /dev/null +++ b/NonEmpty/concatMap.dhall @@ -0,0 +1,47 @@ +{-| +Transform a `NonEmpty` list by applying a function to each element and +flattening the results +-} +let NonEmpty = ./Type.dhall + +let NonEmpty/toList = ./toList.dhall + +let List/concatMap = ../List/concatMap.dhall + +let concatMap + : ∀(a : Type) → ∀(b : Type) → (a → NonEmpty b) → NonEmpty a → NonEmpty b + = λ(a : Type) → + λ(b : Type) → + λ(f : a → NonEmpty b) → + λ(xs : NonEmpty a) → + let ys = f xs.head + + in { head = ys.head + , tail = + ys.tail + # List/concatMap + a + b + (λ(x : a) → NonEmpty/toList b (f x)) + xs.tail + } + +let example0 = + assert + : concatMap + Natural + Natural + (λ(n : Natural) → { head = n, tail = [ n ] }) + { head = 2, tail = [ 3, 5 ] } + ≡ { head = 2, tail = [ 2, 3, 3, 5, 5 ] } + +let example1 = + assert + : concatMap + Natural + Natural + (λ(n : Natural) → { head = n, tail = [ n ] }) + { head = 2, tail = [] : List Natural } + ≡ { head = 2, tail = [ 2 ] } + +in concatMap diff --git a/NonEmpty/head.dhall b/NonEmpty/head.dhall new file mode 100644 index 0000000..ee3dac4 --- /dev/null +++ b/NonEmpty/head.dhall @@ -0,0 +1,10 @@ +--| Retrieve the first element of the `NonEmpty` list +let NonEmpty = ./Type.dhall + +let head + : ∀(a : Type) → NonEmpty a → a + = λ(a : Type) → λ(xs : NonEmpty a) → xs.head + +let example = assert : head Natural { head = 0, tail = [ 1, 2 ] } ≡ 0 + +in head diff --git a/NonEmpty/index.dhall b/NonEmpty/index.dhall new file mode 100644 index 0000000..dd05b72 --- /dev/null +++ b/NonEmpty/index.dhall @@ -0,0 +1,27 @@ +--| Retrieve an element from a `NonEmpty` list using its 0-based index +let NonEmpty = ./Type.dhall + +let List/index = ../List/index.dhall + +let index + : Natural → ∀(a : Type) → NonEmpty a → Optional a + = λ(n : Natural) → + λ(a : Type) → + λ(xs : NonEmpty a) → + if Natural/isZero n + then Some xs.head + else List/index (Natural/subtract 1 n) a xs.tail + +let property = + λ(n : Natural) → + λ(a : Type) → + λ(xs : NonEmpty a) → + assert : index 0 a xs ≡ Some xs.head + +let example0 = assert : index 1 Natural { head = 2, tail = [ 3, 5 ] } ≡ Some 3 + +let example1 = + assert + : index 1 Natural { head = 2, tail = [] : List Natural } ≡ None Natural + +in index diff --git a/NonEmpty/indexed.dhall b/NonEmpty/indexed.dhall new file mode 100644 index 0000000..c91351f --- /dev/null +++ b/NonEmpty/indexed.dhall @@ -0,0 +1,35 @@ +--| Tag each element of the `NonEmpty` list with its index +let NonEmpty = ./Type.dhall + +let List/map = ../List/map.dhall + +let indexed + : ∀(a : Type) → NonEmpty a → NonEmpty { index : Natural, value : a } + = λ(a : Type) → + λ(xs : NonEmpty a) → + { head = { index = 0, value = xs.head } + , tail = + List/map + { index : Natural, value : a } + { index : Natural, value : a } + ( λ(ix : { index : Natural, value : a }) → + { index = ix.index + 1, value = ix.value } + ) + (List/indexed a xs.tail) + } + +let example0 = + assert + : indexed Bool { head = True, tail = [ False, True ] } + ≡ { head = { index = 0, value = True } + , tail = [ { index = 1, value = False }, { index = 2, value = True } ] + } + +let example1 = + assert + : indexed Bool { head = True, tail = [] : List Bool } + ≡ { head = { index = 0, value = True } + , tail = [] : List { index : Natural, value : Bool } + } + +in indexed diff --git a/NonEmpty/last.dhall b/NonEmpty/last.dhall new file mode 100644 index 0000000..496e272 --- /dev/null +++ b/NonEmpty/last.dhall @@ -0,0 +1,12 @@ +λ(nix : ../NixPrelude.dhall) → + let NonEmpty = ./Type.dhall + + let Optional/default = ../Optional/default.dhall nix + + let last + : ∀(a : Type) → NonEmpty a → a + = λ(a : Type) → + λ(xs : NonEmpty a) → + Optional/default a xs.head (List/last a xs.tail) + + in last diff --git a/NonEmpty/length.dhall b/NonEmpty/length.dhall new file mode 100644 index 0000000..d7132ff --- /dev/null +++ b/NonEmpty/length.dhall @@ -0,0 +1,13 @@ +--| Returns the number of elements in a `NonEmpty` list +let NonEmpty = ./Type.dhall + +let length + : ∀(a : Type) → NonEmpty a → Natural + = λ(a : Type) → λ(xs : NonEmpty a) → List/length a xs.tail + 1 + +let example0 = assert : length Natural { head = 0, tail = [ 1, 2 ] } ≡ 3 + +let example1 = + assert : length Natural { head = 0, tail = [] : List Natural } ≡ 1 + +in length diff --git a/NonEmpty/make.dhall b/NonEmpty/make.dhall new file mode 100644 index 0000000..685726d --- /dev/null +++ b/NonEmpty/make.dhall @@ -0,0 +1,15 @@ +{-| +Create a `NonEmpty` list using a function instead of a record + +This might come in handy if you want to decouple the `NonEmpty` list +construction from the specific names of the fields. +-} +let NonEmpty = ./Type.dhall + +let make + : ∀(a : Type) → ∀(head : a) → ∀(tail : List a) → NonEmpty a + = λ(a : Type) → λ(head : a) → λ(tail : List a) → { head, tail } + +let example = assert : make Natural 1 [ 2, 3 ] ≡ { head = 1, tail = [ 2, 3 ] } + +in make diff --git a/NonEmpty/map.dhall b/NonEmpty/map.dhall new file mode 100644 index 0000000..bf72019 --- /dev/null +++ b/NonEmpty/map.dhall @@ -0,0 +1,24 @@ +--| Transform a `NonEmpty` list by applying a function to each element +let NonEmpty = ./Type.dhall + +let List/map = ../List/map.dhall + +let map + : ∀(a : Type) → ∀(b : Type) → (a → b) → NonEmpty a → NonEmpty b + = λ(a : Type) → + λ(b : Type) → + λ(f : a → b) → + λ(xs : NonEmpty a) → + { head = f xs.head, tail = List/map a b f xs.tail } + +let example0 = + assert + : map Natural Bool Natural/even { head = 2, tail = [ 3, 5 ] } + ≡ { head = True, tail = [ False, False ] } + +let example1 = + assert + : map Natural Bool Natural/even { head = 2, tail = [] : List Natural } + ≡ { head = True, tail = [] : List Bool } + +in map diff --git a/NonEmpty/package.dhall b/NonEmpty/package.dhall new file mode 100644 index 0000000..74cc6bb --- /dev/null +++ b/NonEmpty/package.dhall @@ -0,0 +1,20 @@ +λ(nix : ../NixPrelude.dhall) → + { Type = ./Type.dhall + , all = ./all.dhall + , any = ./any.dhall + , concat = ./concat.dhall + , concatMap = ./concatMap.dhall + , head = ./head.dhall + , index = ./index.dhall + , indexed = ./indexed.dhall + , last = ./last.dhall nix + , length = ./length.dhall + , make = ./make.dhall + , map = ./map.dhall + , reverse = ./reverse.dhall nix + , shifted = ./shifted.dhall + , singleton = ./singleton.dhall + , toList = ./toList.dhall + , unzip = ./unzip.dhall + , zip = ./zip.dhall nix + } diff --git a/NonEmpty/reverse.dhall b/NonEmpty/reverse.dhall new file mode 100644 index 0000000..474778b --- /dev/null +++ b/NonEmpty/reverse.dhall @@ -0,0 +1,21 @@ +λ(nix : ../NixPrelude.dhall) → + let NonEmpty = ./Type.dhall + + let List/drop = ../List/drop.dhall + + let Optional/fold = ../Optional/fold.dhall nix + + let reverse + : ∀(a : Type) → NonEmpty a → NonEmpty a + = λ(a : Type) → + λ(xs : NonEmpty a) → + let ys = List/reverse a xs.tail + + in Optional/fold + a + (List/head a ys) + (NonEmpty a) + (λ(y : a) → { head = y, tail = List/drop 1 a ys # [ xs.head ] }) + { head = xs.head, tail = [] : List a } + + in reverse diff --git a/NonEmpty/shifted.dhall b/NonEmpty/shifted.dhall new file mode 100644 index 0000000..2fbf0f6 --- /dev/null +++ b/NonEmpty/shifted.dhall @@ -0,0 +1,89 @@ +{-| +Combine a `NonEmpty` list of `NonEmpty` lists, offsetting the `index` of each +element by the number of elements in preceding lists +-} +let NonEmpty = ./Type.dhall + +let NonEmpty/toList = ./toList.dhall + +let List/map = ../List/map.dhall + +let List/shifted = ../List/shifted.dhall + +let shifted + : ∀(a : Type) → + NonEmpty (NonEmpty { index : Natural, value : a }) → + NonEmpty { index : Natural, value : a } + = λ(a : Type) → + λ(kvss : NonEmpty (NonEmpty { index : Natural, value : a })) → + { head = kvss.head.head + , tail = + List/shifted + a + ( [ kvss.head.tail ] + # List/map + (NonEmpty { index : Natural, value : a }) + (List { index : Natural, value : a }) + ( λ(kvs : NonEmpty { index : Natural, value : a }) → + List/map + { index : Natural, value : a } + { index : Natural, value : a } + ( λ(kv : { index : Natural, value : a }) → + { index = kv.index + 1, value = kv.value } + ) + (NonEmpty/toList { index : Natural, value : a } kvs) + ) + kvss.tail + ) + } + +let example0 = + assert + : shifted + Bool + { head = + { head = { index = 0, value = True } + , tail = + [ { index = 1, value = True }, { index = 2, value = True } ] + } + , tail = + [ { head = { index = 0, value = False } + , tail = [ { index = 1, value = False } ] + } + , { head = { index = 0, value = True } + , tail = + [ { index = 1, value = True } + , { index = 2, value = True } + , { index = 3, value = True } + ] + } + ] + } + ≡ { head = { index = 0, value = True } + , tail = + [ { 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 + { head = + { head = { index = 0, value = True } + , tail = [] : List { index : Natural, value : Bool } + } + , tail = [] : List (NonEmpty { index : Natural, value : Bool }) + } + ≡ { head = { index = 0, value = True } + , tail = [] : List { index : Natural, value : Bool } + } + +in shifted diff --git a/NonEmpty/singleton.dhall b/NonEmpty/singleton.dhall new file mode 100644 index 0000000..24a4360 --- /dev/null +++ b/NonEmpty/singleton.dhall @@ -0,0 +1,11 @@ +--| Create a `NonEmpty` list with just one element +let NonEmpty = ./Type.dhall + +let singleton + : ∀(a : Type) → a → NonEmpty a + = λ(a : Type) → λ(x : a) → { head = x, tail = [] : List a } + +let example = + assert : singleton Natural 2 ≡ { head = 2, tail = [] : List Natural } + +in singleton diff --git a/NonEmpty/toList.dhall b/NonEmpty/toList.dhall new file mode 100644 index 0000000..2add232 --- /dev/null +++ b/NonEmpty/toList.dhall @@ -0,0 +1,14 @@ +--| Convert a `NonEmpty` list into the equivalent `List` +let NonEmpty = ./Type.dhall + +let toList + : ∀(a : Type) → NonEmpty a → List a + = λ(a : Type) → λ(xs : NonEmpty a) → [ xs.head ] # xs.tail + +let example0 = + assert : toList Natural { head = 2, tail = [ 3, 5 ] } ≡ [ 2, 3, 5 ] + +let example1 = + assert : toList Natural { head = 2, tail = [] : List Natural } ≡ [ 2 ] + +in toList diff --git a/NonEmpty/unzip.dhall b/NonEmpty/unzip.dhall new file mode 100644 index 0000000..f48bd28 --- /dev/null +++ b/NonEmpty/unzip.dhall @@ -0,0 +1,52 @@ +--| Unzip a `NonEmpty` list into two separate `NonEmpty` lists +let NonEmpty = ./Type.dhall + +let NonEmpty/map = ./map.dhall + +let unzip + : ∀(a : Type) → + ∀(b : Type) → + NonEmpty { _1 : a, _2 : b } → + { _1 : NonEmpty a, _2 : NonEmpty b } + = λ(a : Type) → + λ(b : Type) → + λ(xs : NonEmpty { _1 : a, _2 : b }) → + { _1 = + NonEmpty/map + { _1 : a, _2 : b } + a + (λ(x : { _1 : a, _2 : b }) → x._1) + xs + , _2 = + NonEmpty/map + { _1 : a, _2 : b } + b + (λ(x : { _1 : a, _2 : b }) → x._2) + xs + } + +let example0 = + assert + : unzip + Text + Bool + { head = { _1 = "ABC", _2 = True } + , tail = [ { _1 = "DEF", _2 = False }, { _1 = "GHI", _2 = True } ] + } + ≡ { _1 = { head = "ABC", tail = [ "DEF", "GHI" ] } + , _2 = { head = True, tail = [ False, True ] } + } + +let example1 = + assert + : unzip + Text + Bool + { head = { _1 = "ABC", _2 = True } + , tail = [] : List { _1 : Text, _2 : Bool } + } + ≡ { _1 = { head = "ABC", tail = [] : List Text } + , _2 = { head = True, tail = [] : List Bool } + } + +in unzip diff --git a/NonEmpty/zip.dhall b/NonEmpty/zip.dhall new file mode 100644 index 0000000..e8c587d --- /dev/null +++ b/NonEmpty/zip.dhall @@ -0,0 +1,20 @@ +λ(nix : ../NixPrelude.dhall) → + let NonEmpty = ./Type.dhall + + let List/zip = ../List/zip.dhall nix + + let zip + : ∀(a : Type) → + NonEmpty a → + ∀(b : Type) → + NonEmpty b → + NonEmpty { _1 : a, _2 : b } + = λ(a : Type) → + λ(xs : NonEmpty a) → + λ(b : Type) → + λ(ys : NonEmpty b) → + { head = { _1 = xs.head, _2 = ys.head } + , tail = List/zip a xs.tail b ys.tail + } + + in zip diff --git a/package.dhall b/package.dhall index 575f3c6..06bd62e 100644 --- a/package.dhall +++ b/package.dhall @@ -9,6 +9,7 @@ , Map = ./Map/package.dhall nix , Misc = ./Misc/package.dhall nix , Monoid = ./Monoid.dhall + , NonNull = ./NonEmpty/package.dhall nix , Natural = ./Natural/package.dhall nix , Number = ./Number/package.dhall nix , Path = ./Path/package.dhall nix