Use new Some and None constructors (#9)

This also removes `./Optional/{Some,None}` since they are now obsolete
dhall-lang · Sep 10, 2018 · 0c83aed · 0c83aed
1 parent 302881a
commit 0c83aed
Show file tree

Hide file tree

Showing 30 changed files with 149 additions and 209 deletions.
diff --git 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
@@ -1 +1 @@
-{ show = ./show  }
+{ show = ./show }
diff --git a/Integer/package.dhall b/Integer/package.dhall
@@ -1 +1 @@
-{ show = ./show  }
+{ show = ./show }
diff --git 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
@@ -1,3 +1 @@
-{ keyText = ./keyText
-, keyValue = ./keyValue
-}
+{ keyText = ./keyText, keyValue = ./keyValue }
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/Optional/Some b/Optional/Some
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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