From 14014aa4111c9a5884e7a8eecc17f787a2cb276f Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Fri, 7 Sep 2018 09:05:57 -0700 Subject: [PATCH] Use new `Some` and `None` constructors This also removes `./Optional/{Some,None}` since they are now obsolete --- Bool/package.dhall | 16 ++++++++-------- Double/package.dhall | 2 +- Integer/package.dhall | 2 +- JSON/Tagged | 2 +- JSON/package.dhall | 4 +--- List/head | 4 ++-- List/last | 4 ++-- List/package.dhall | 38 +++++++++++++++++++------------------- List/shifted | 11 +++++++---- Natural/package.dhall | 20 ++++++++++---------- Optional/None | 13 ------------- Optional/Some | 13 ------------- Optional/all | 4 ++-- Optional/any | 4 ++-- Optional/build | 20 ++++++++++---------- Optional/concat | 14 +++++++------- Optional/filter | 16 ++++++++-------- Optional/fold | 8 ++++---- Optional/head | 20 +++++--------------- Optional/last | 20 +++++--------------- Optional/length | 4 ++-- Optional/map | 13 +++---------- Optional/null | 4 ++-- Optional/package.dhall | 30 +++++++++++++----------------- Optional/toList | 11 +++-------- Optional/unzip | 19 ++++++++----------- Text/concatMapSep | 8 +++++--- Text/concatSep | 8 +++++--- Text/package.dhall | 8 ++++---- package.dhall | 18 +++++++++--------- 30 files changed, 149 insertions(+), 209 deletions(-) delete mode 100644 Optional/None delete mode 100644 Optional/Some diff --git a/Bool/package.dhall b/Bool/package.dhall index c004339..c776940 100644 --- a/Bool/package.dhall +++ b/Bool/package.dhall @@ -1,17 +1,17 @@ { and = - ./and + ./and , build = - ./build + ./build , even = - ./even + ./even , fold = - ./fold + ./fold , not = - ./not + ./not , odd = - ./odd + ./odd , or = - ./or + ./or , show = - ./show + ./show } diff --git a/Double/package.dhall b/Double/package.dhall index 0acd0bf..46f0272 100644 --- a/Double/package.dhall +++ b/Double/package.dhall @@ -1 +1 @@ -{ show = ./show } +{ show = ./show } diff --git a/Integer/package.dhall b/Integer/package.dhall index 0acd0bf..46f0272 100644 --- a/Integer/package.dhall +++ b/Integer/package.dhall @@ -1 +1 @@ -{ show = ./show } +{ show = ./show } diff --git a/JSON/Tagged b/JSON/Tagged index 33e8aef..9b731d6 100644 --- a/JSON/Tagged +++ b/JSON/Tagged @@ -64,6 +64,6 @@ in { provisioners = -} let Tagged : Type → Type - = λ(a : Type) → { field : Text, nesting : ./Nesting , contents : a } + = λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a } in Tagged diff --git a/JSON/package.dhall b/JSON/package.dhall index 3ee10c8..9c4b605 100644 --- a/JSON/package.dhall +++ b/JSON/package.dhall @@ -1,3 +1 @@ -{ keyText = ./keyText -, keyValue = ./keyValue -} +{ keyText = ./keyText, keyValue = ./keyValue } diff --git a/List/head b/List/head index 3bc895f..0e2186e 100644 --- a/List/head +++ b/List/head @@ -4,9 +4,9 @@ Retrieve the first element of the list Examples: ``` -./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural +./head Natural [ 0, 1, 2 ] = Some 0 -./head Natural ([] : List Natural) = [] : Optional Natural +./head Natural ([] : List Natural) = None Natural ``` -} let head : ∀(a : Type) → List a → Optional a = List/head in head diff --git a/List/last b/List/last index b6fe099..ca0cf7b 100644 --- a/List/last +++ b/List/last @@ -4,9 +4,9 @@ Retrieve the last element of the list Examples: ``` -./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural +./last Natural [ 0, 1, 2 ] = Some 2 -./last Natural ([] : List Natural) = [] : Optional Natural +./last Natural ([] : List Natural) = None Natural ``` -} let last : ∀(a : Type) → List a → Optional a = List/last in last diff --git a/List/package.dhall b/List/package.dhall index cdf0fa8..9555bbb 100644 --- a/List/package.dhall +++ b/List/package.dhall @@ -1,39 +1,39 @@ { all = - ./all + ./all , any = - ./any + ./any , build = - ./build + ./build , concat = - ./concat + ./concat , concatMap = - ./concatMap + ./concatMap , filter = - ./filter + ./filter , fold = - ./fold + ./fold , generate = - ./generate + ./generate , head = - ./head + ./head , indexed = - ./indexed + ./indexed , iterate = - ./iterate + ./iterate , last = - ./last + ./last , length = - ./length + ./length , map = - ./map + ./map , null = - ./null + ./null , replicate = - ./replicate + ./replicate , reverse = - ./reverse + ./reverse , shifted = - ./shifted + ./shifted , unzip = - ./unzip + ./unzip } diff --git a/List/shifted b/List/shifted index ebf505c..80551dc 100644 --- a/List/shifted +++ b/List/shifted @@ -58,8 +58,9 @@ Bool { index : Natural, value : a } kvs - in { count = y.count + length - , diff = + in { count = + y.count + length + , diff = λ(n : Natural) → List/fold { index : Natural, value : a } @@ -70,8 +71,10 @@ Bool ) → λ(z : list) → let kvNew = - { index = kvOld.index + n - , value = kvOld.value + { index = + kvOld.index + n + , value = + kvOld.value } in cons kvNew z diff --git a/Natural/package.dhall b/Natural/package.dhall index 41ee0b2..513cb97 100644 --- a/Natural/package.dhall +++ b/Natural/package.dhall @@ -1,21 +1,21 @@ { build = - ./build + ./build , enumerate = - ./enumerate + ./enumerate , even = - ./even + ./even , fold = - ./fold + ./fold , isZero = - ./isZero + ./isZero , odd = - ./odd + ./odd , product = - ./product + ./product , sum = - ./sum + ./sum , show = - ./show + ./show , toInteger = - ./toInteger + ./toInteger } diff --git a/Optional/None b/Optional/None deleted file mode 100644 index 0a6dc70..0000000 --- a/Optional/None +++ /dev/null @@ -1,13 +0,0 @@ -{- -Convenience function to construct empty Optional values. - -Examples: - -``` -./None Natural = [] : Optional Natural - -./None Text = [] : Optional Text -``` --} - -let None = λ(a : Type) → [] : Optional a in None diff --git a/Optional/Some b/Optional/Some deleted file mode 100644 index 1bac8c0..0000000 --- a/Optional/Some +++ /dev/null @@ -1,13 +0,0 @@ -{- -Convenience function to construct an Optional containing a value. - -Examples: - -``` -./Some Natural 42 = [ 42 ] : Optional Natural - -./Some Text "foo" = [ "foo" ] : Optional Text -``` --} - -let Some = λ(a : Type) → λ(v : a) → [ v ] : Optional a in Some diff --git a/Optional/all b/Optional/all index 76d8fcc..0db2c8f 100644 --- a/Optional/all +++ b/Optional/all @@ -5,9 +5,9 @@ and `True` otherwise: Examples: ``` -./all Natural Natural/even ([ 3 ] : Optional Natural) = False +./all Natural Natural/even (Some 3) = False -./all Natural Natural/even ([] : Optional Natural) = True +./all Natural Natural/even (None Natural) = True ``` -} let all diff --git a/Optional/any b/Optional/any index d172182..172cebc 100644 --- a/Optional/any +++ b/Optional/any @@ -5,9 +5,9 @@ Returns `True` if the supplied function returns `True` for a present element and Examples: ``` -./any Natural Natural/even ([ 2 ] : Optional Natural) = True +./any Natural Natural/even (Some 2) = True -./any Natural Natural/even ([] : Optional Natural) = False +./any Natural Natural/even (None Natural) = False ``` -} let any diff --git a/Optional/build b/Optional/build index 2636f7c..dde5fa6 100644 --- a/Optional/build +++ b/Optional/build @@ -7,27 +7,27 @@ Examples: ./build Natural ( λ(optional : Type) -→ λ(just : Natural → optional) -→ λ(nothing : optional) -→ just 1 +→ λ(some : Natural → optional) +→ λ(none : optional) +→ some 1 ) -= [ 1 ] : Optional Natural += Some 1 ./build Natural ( λ(optional : Type) -→ λ(just : Natural → optional) -→ λ(nothing : optional) -→ nothing +→ λ(some : Natural → optional) +→ λ(none : optional) +→ none ) -= [] : Optional Natural += None Natural ``` -} let build : ∀(a : Type) → ( ∀(optional : Type) - → ∀(just : a → optional) - → ∀(nothing : optional) + → ∀(some : a → optional) + → ∀(none : optional) → optional ) → Optional a diff --git a/Optional/concat b/Optional/concat index f915807..8bbd36f 100644 --- a/Optional/concat +++ b/Optional/concat @@ -4,14 +4,14 @@ Flatten two `Optional` layers into a single `Optional` layer Examples: ``` -./concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural)) -= [ 1 ] : Optional Natural +./concat Natural (Some (Some 1)) += Some 1 -./concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural)) -= [] : Optional Natural +./concat Natural (Some (None Natural)) += None Natural -./concat Natural ([] : Optional (Optional Natural)) -= [] : Optional Natural +./concat Natural (None (Optional Natural)) += None Natural ``` -} let concat @@ -23,6 +23,6 @@ Examples: x (Optional a) (λ(y : Optional a) → y) - ([] : Optional a) + (None a) in concat diff --git a/Optional/filter b/Optional/filter index e1b6d13..3c0d4eb 100644 --- a/Optional/filter +++ b/Optional/filter @@ -4,11 +4,11 @@ Only keep an `Optional` element if the supplied function returns `True` Examples: ``` -./filter Natural Natural/even ([ 2 ] : Optional Natural) -= [ 2 ] : Optional Natural +./filter Natural Natural/even (Some 2) += Some 2 -./filter Natural Natural/odd ([ 2 ] : Optional Natural) -= [] : Optional Natural +./filter Natural Natural/odd (Some 2) += None Natural ``` -} let filter @@ -19,14 +19,14 @@ Examples: → Optional/build a ( λ(optional : Type) - → λ(just : a → optional) - → λ(nil : optional) + → λ(some : a → optional) + → λ(none : optional) → Optional/fold a xs optional - (λ(x : a) → if f x then just x else nil) - nil + (λ(x : a) → if f x then some x else none) + none ) in filter diff --git a/Optional/fold b/Optional/fold index 3b8e39f..602fba2 100644 --- a/Optional/fold +++ b/Optional/fold @@ -4,17 +4,17 @@ Examples: ``` -./fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 2 +./fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 = 2 -./fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 0 +./fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 = 0 ``` -} let fold : ∀(a : Type) → Optional a → ∀(optional : Type) - → ∀(just : a → optional) - → ∀(nothing : optional) + → ∀(some : a → optional) + → ∀(none : optional) → optional = Optional/fold diff --git a/Optional/head b/Optional/head index ea0433d..9cbce3c 100644 --- a/Optional/head +++ b/Optional/head @@ -4,21 +4,11 @@ Returns the first non-empty `Optional` value in a `List` Examples: ``` -./head -Natural -[ [ ] : Optional Natural -, [ 1 ] : Optional Natural -, [ 2 ] : Optional Natural -] -= [ 1 ] : Optional Natural +./head Natural [ None Natural, Some 1, Some 2 ] = Some 1 -./head -Natural -[ [] : Optional Natural, [] : Optional Natural ] -= [] : Optional Natural +./head Natural [ None Natural, None Natural ] = None Natural -./head Natural ([] : List (Optional Natural)) -= [] : Optional Natural +./head Natural ([] : List (Optional Natural)) = None Natural ``` -} let head @@ -31,8 +21,8 @@ Natural (Optional a) ( λ(l : Optional a) → λ(r : Optional a) - → Optional/fold a l (Optional a) (λ(x : a) → [ x ] : Optional a) r + → Optional/fold a l (Optional a) (λ(x : a) → Some x) r ) - ([] : Optional a) + (None a) in head diff --git a/Optional/last b/Optional/last index 4af913d..8c70d9e 100644 --- a/Optional/last +++ b/Optional/last @@ -4,21 +4,11 @@ Returns the last non-empty `Optional` value in a `List` Examples: ``` -./last -Natural -[ [ ] : Optional Natural -, [ 1 ] : Optional Natural -, [ 2 ] : Optional Natural -] -= [ 2 ] : Optional Natural +./last Natural [ None Natural, Some 1, Some 2 ] = Some 2 -./last -Natural -[ [] : Optional Natural, [] : Optional Natural ] -= [] : Optional Natural +./last Natural [ None Natural, None Natural ] = None Natural -./last Natural ([] : List (Optional Natural)) -= [] : Optional Natural +./last Natural ([] : List (Optional Natural)) = None Natural ``` -} let last @@ -31,8 +21,8 @@ Natural (Optional a) ( λ(l : Optional a) → λ(r : Optional a) - → Optional/fold a r (Optional a) (λ(x : a) → [ x ] : Optional a) l + → Optional/fold a r (Optional a) (λ(x : a) → Some x) l ) - ([] : Optional a) + (None a) in last diff --git a/Optional/length b/Optional/length index 55ea87c..c8df433 100644 --- a/Optional/length +++ b/Optional/length @@ -4,9 +4,9 @@ Returns `1` if the `Optional` value is present and `0` if the value is absent Examples: ``` -./length Natural ([ 2 ] : Optional Natural) = 1 +./length Natural (Some 2) = 1 -./length Natural ([] : Optional Natural) = 0 +./length Natural (None Natural) = 0 ``` -} let length diff --git a/Optional/map b/Optional/map index f9e5ae4..d08329e 100644 --- a/Optional/map +++ b/Optional/map @@ -4,11 +4,9 @@ Transform an `Optional` value with a function Examples: ``` -./map Natural Bool Natural/even ([ 3 ] : Optional Natural) -= [ False ] : Optional Bool +./map Natural Bool Natural/even (Some 3) = Some False -./map Natural Bool Natural/even ([] : Optional Natural) -= [] : Optional Bool +./map Natural Bool Natural/even (None Natural) = None Bool ``` -} let map @@ -17,11 +15,6 @@ Examples: → λ(b : Type) → λ(f : a → b) → λ(o : Optional a) - → Optional/fold - a - o - (Optional b) - (λ(x : a) → [ f x ] : Optional b) - ([] : Optional b) + → Optional/fold a o (Optional b) (λ(x : a) → Some (f x)) (None b) in map diff --git a/Optional/null b/Optional/null index 0accfce..6854edb 100644 --- a/Optional/null +++ b/Optional/null @@ -4,9 +4,9 @@ Returns `True` if the `Optional` value is absent and `False` if present Examples: ``` -./null Natural ([ 2 ] : Optional Natural) = False +./null Natural (Some 2) = False -./null Natural ([] : Optional Natural) = True +./null Natural (None Natural) = True ``` -} let null diff --git a/Optional/package.dhall b/Optional/package.dhall index a0bb2e8..97a4d0c 100644 --- a/Optional/package.dhall +++ b/Optional/package.dhall @@ -1,31 +1,27 @@ { all = - ./all + ./all , any = - ./any + ./any , build = - ./build + ./build , concat = - ./concat + ./concat , filter = - ./filter + ./filter , fold = - ./fold + ./fold , head = - ./head + ./head , last = - ./last + ./last , length = - ./length + ./length , map = - ./map + ./map , null = - ./null + ./null , toList = - ./toList + ./toList , unzip = - ./unzip -, None = - ./None -, Some = - ./Some + ./unzip } diff --git a/Optional/toList b/Optional/toList index dcaa6c7..6dc7ccb 100644 --- a/Optional/toList +++ b/Optional/toList @@ -4,20 +4,15 @@ Convert an `Optional` value into the equivalent `List` Examples: ``` -./toList Natural ([ 1 ] : Optional Natural) = [ 1 ] +./toList Natural (Some 1) = [ 1 ] -./toList Natural ([] : Optional Natural) = [] : List Natural +./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) + → Optional/fold a o (List a) (λ(x : a) → [ x ] : List a) ([] : List a) in toList diff --git a/Optional/unzip b/Optional/unzip index a5a3178..af4b99f 100644 --- a/Optional/unzip +++ b/Optional/unzip @@ -4,14 +4,11 @@ Unzip an `Optional` value into two separate `Optional` values Examples: ``` -./unzip -Text -Bool -([ { _1 = "ABC", _2 = True } ] : Optional { _1 : Text, _2 : Bool }) -= { _1 = [ "ABC" ] : Optional Text, _2 = [ True ] : Optional Bool } +./unzip Text Bool (Some { _1 = "ABC", _2 = True }) += { _1 = Some "ABC", _2 = Some True } -./unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool }) -= { _1 = [] : Optional Text, _2 = [] : Optional Bool } +./unzip Text Bool (None { _1 : Text, _2 : Bool }) += { _1 = None Text, _2 = None Bool } ``` -} let unzip @@ -27,15 +24,15 @@ Bool { _1 : a, _2 : b } xs (Optional a) - (λ(x : { _1 : a, _2 : b }) → [ x._1 ] : Optional a) - ([] : 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 }) → [ x._2 ] : Optional b) - ([] : Optional b) + (λ(x : { _1 : a, _2 : b }) → Some x._2) + (None b) } in unzip diff --git a/Text/concatMapSep b/Text/concatMapSep index 5a0b576..5d5b0be 100644 --- a/Text/concatMapSep +++ b/Text/concatMapSep @@ -24,12 +24,14 @@ Examples: ( λ(element : a) → λ(status : < Empty : {} | NonEmpty : Text >) → merge - { Empty = + { Empty = λ(_ : {}) → < NonEmpty = f element | Empty : {} > , NonEmpty = λ(result : Text) - → < NonEmpty = f element ++ separator ++ result - | Empty : {} + → < NonEmpty = + f element ++ separator ++ result + | Empty : + {} > } status diff --git a/Text/concatSep b/Text/concatSep index 709a4a8..d25df38 100644 --- a/Text/concatSep +++ b/Text/concatSep @@ -21,12 +21,14 @@ Examples: ( λ(element : Text) → λ(status : < Empty : {} | NonEmpty : Text >) → merge - { Empty = + { Empty = λ(_ : {}) → < NonEmpty = element | Empty : {} > , NonEmpty = λ(result : Text) - → < NonEmpty = element ++ separator ++ result - | Empty : {} + → < NonEmpty = + element ++ separator ++ result + | Empty : + {} > } status diff --git a/Text/package.dhall b/Text/package.dhall index 7b8a2ed..863d06c 100644 --- a/Text/package.dhall +++ b/Text/package.dhall @@ -1,9 +1,9 @@ { concat = - ./concat + ./concat , concatMap = - ./concatMap + ./concatMap , concatMapSep = - ./concatMapSep + ./concatMapSep , concatSep = - ./concatSep + ./concatSep } diff --git a/package.dhall b/package.dhall index 81875d3..7b88b79 100644 --- a/package.dhall +++ b/package.dhall @@ -1,19 +1,19 @@ { `Bool` = - ./Bool/package.dhall + ./Bool/package.dhall , `Double` = - ./Double/package.dhall + ./Double/package.dhall , Function = - ./Function/package.dhall + ./Function/package.dhall , `Integer` = - ./Integer/package.dhall + ./Integer/package.dhall , `List` = - ./List/package.dhall + ./List/package.dhall , `Natural` = - ./Natural/package.dhall + ./Natural/package.dhall , `Optional` = - ./Optional/package.dhall -, `JSON` = + ./Optional/package.dhall +, JSON = ./JSON/package.dhall , `Text` = - ./Text/package.dhall + ./Text/package.dhall }