Permalink
Browse files

Update Prelude to reflect changes to `Natural` literals (#1)

The Prelude examples and code now reflect the fact that `Natural`
numbers don't require a leading `+`

Most of the examples change to use `Natural` literals since they are now
the more visually pleasing literal
  • Loading branch information...
Gabriel439 committed May 19, 2018
1 parent d48dc51 commit e44284bc37a5808861dacd4c8bd13d18411cb961
Showing with 149 additions and 148 deletions.
  1. +2 −2 Bool/fold
  2. +3 −2 Integer/show
  3. +1 −1 List/all
  4. +1 −1 List/any
  5. +7 −7 List/concat
  6. +2 −2 List/concatMap
  7. +4 −4 List/filter
  8. +7 −7 List/fold
  9. +3 −3 List/generate
  10. +2 −2 List/head
  11. +3 −3 List/indexed
  12. +3 −3 List/iterate
  13. +2 −2 List/last
  14. +2 −2 List/length
  15. +1 −1 List/map
  16. +2 −2 List/null
  17. +2 −2 List/replicate
  18. +2 −2 List/reverse
  19. +20 −20 List/shifted
  20. +2 −2 Natural/build
  21. +3 −3 Natural/enumerate
  22. +2 −2 Natural/even
  23. +5 −5 Natural/fold
  24. +3 −3 Natural/isZero
  25. +2 −2 Natural/odd
  26. +3 −3 Natural/product
  27. +3 −3 Natural/show
  28. +3 −3 Natural/sum
  29. +2 −2 Natural/toInteger
  30. +1 −1 Optional/all
  31. +1 −1 Optional/any
  32. +6 −6 Optional/build
  33. +6 −6 Optional/concat
  34. +3 −3 Optional/filter
  35. +2 −2 Optional/fold
  36. +10 −10 Optional/head
  37. +10 −10 Optional/last
  38. +4 −4 Optional/length
  39. +1 −1 Optional/map
  40. +2 −2 Optional/null
  41. +2 −2 Optional/toList
  42. +2 −2 Text/concatMap
  43. +2 −2 Text/concatMapSep
View
@@ -4,9 +4,9 @@
Examples:
```
./fold True Integer 0 1 = 0
./fold True Natural 0 1 = 0
./fold False Integer 0 1 = 1
./fold False Natural 0 1 = 1
```
-}
let fold
View
@@ -1,13 +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)
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"
./show +0 = "+0"
```
-}
let show : Integer → Text = Integer/show in show
View
@@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for all elements in the
Examples:
```
./all Natural Natural/even [ +2, +3, +5 ] = False
./all Natural Natural/even [ 2, 3, 5 ] = False
./all Natural Natural/even ([] : List Natural) = True
```
View
@@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for any element in the
Examples:
```
./any Natural Natural/even [ +2, +3, +5 ] = True
./any Natural Natural/even [ 2, 3, 5 ] = True
./any Natural Natural/even ([] : List Natural) = False
```
View
@@ -4,22 +4,22 @@ Concatenate a `List` of `List`s into a single `List`
Examples:
```
./concat Integer
./concat Natural
[ [0, 1, 2]
, [3, 4]
, [5, 6, 7, 8]
]
= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
./concat Integer
( [ [] : List Integer
, [] : List Integer
, [] : List Integer
./concat Natural
( [ [] : List Natural
, [] : List Natural
, [] : List Natural
]
)
= [] : List Integer
= [] : List Natural
./concat Integer ([] : List (List Integer)) = [] : List Integer
./concat Natural ([] : List (List Natural)) = [] : List Natural
```
-}
let concat
View
@@ -5,8 +5,8 @@ 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]) [2, 3, 5]
= [ 2, 2, 3, 3, 5, 5 ]
./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural)
= [] : List Natural
View
@@ -4,11 +4,11 @@ Only keep elements of the list where the supplied function returns `True`
Examples:
```
./filter Natural Natural/even [+2, +3, +5]
= [ +2 ]
./filter Natural Natural/even [ 2, 3, 5 ]
= [ 2 ]
./filter Natural Natural/odd [+2, +3, +5]
= [ +3, +5 ]
./filter Natural Natural/odd [ 2, 3, 5 ]
= [ 3, 5 ]
```
-}
let filter
View
@@ -9,29 +9,29 @@ Examples:
```
./fold
Natural
[ +2, +3, +5 ]
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
+0
= +10
0
= 10
λ(nil : Natural)
→ ./fold
Natural
[ +2, +3, +5 ]
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
nil
= λ(nil : Natural) → +2 + +3 + +5 + nil
= λ(nil : Natural) → 2 + 3 + 5 + nil
λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)
→ ./fold Natural [ +2, +3, +5 ] list cons nil
→ ./fold Natural [ 2, 3, 5 ] list cons nil
= λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)
→ cons +2 (cons +3 (cons +5 nil))
→ cons 2 (cons 3 (cons 5 nil))
```
-}
let fold
View
@@ -1,13 +1,13 @@
{-
Build a list by calling the supplied function on all `Natural` numbers from `+0`
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 5 Bool Natural/even = [ True, False, True, False, True ]
./generate +0 Bool Natural/even = [] : List Bool
./generate 0 Bool Natural/even = [] : List Bool
```
-}
let generate
View
@@ -4,9 +4,9 @@ Retrieve the first element of the list
Examples:
```
./head Integer [ 0, 1, 2 ] = [ 0 ] : Optional Integer
./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural
./head Integer ([] : List Integer) = [] : Optional Integer
./head Natural ([] : List Natural) = [] : Optional Natural
```
-}
let head : ∀(a : Type) → List a → Optional a = List/head in head
View
@@ -5,9 +5,9 @@ Examples:
```
./indexed Bool [ True, False, True ]
= [ { index = +0, value = True }
, { index = +1, value = False }
, { index = +2, value = True }
= [ { index = 0, value = True }
, { index = 1, value = False }
, { index = 2, value = True }
] : List { index : Natural, value : Bool }
./indexed Bool ([] : List Bool)
View
@@ -5,10 +5,10 @@ function
Examples:
```
./iterate +10 Natural (λ(x : Natural) → x * +2) +1
= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]
./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
./iterate 0 Natural (λ(x : Natural) → x * 2) 1
= [] : List Natural
```
-}
View
@@ -4,9 +4,9 @@ Retrieve the last element of the list
Examples:
```
./last Integer [ 0, 1, 2 ] = [ 2 ] : Optional Integer
./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural
./last Integer ([] : List Integer) = [] : Optional Integer
./last Natural ([] : List Natural) = [] : Optional Natural
```
-}
let last : ∀(a : Type) → List a → Optional a = List/last in last
View
@@ -4,9 +4,9 @@ Returns the number of elements in a list
Examples:
```
./length Integer [ 0, 1, 2 ] = +3
./length Natural [ 0, 1, 2 ] = 3
./length Integer ([] : List Integer) = +0
./length Natural ([] : List Natural) = 0
```
-}
let length : ∀(a : Type) → List a → Natural = List/length in length
View
@@ -4,7 +4,7 @@ Transform a list by applying a function to each element
Examples:
```
./map Natural Bool Natural/even [ +2, +3, +5 ]
./map Natural Bool Natural/even [ 2, 3, 5 ]
= [ True, False, False ]
./map Natural Bool Natural/even ([] : List Natural)
View
@@ -4,9 +4,9 @@ Returns `True` if the `List` is empty and `False` otherwise
Examples:
```
./null Integer [ 0, 1, 2 ] = False
./null Natural [ 0, 1, 2 ] = False
./null Integer ([] : List Integer) = True
./null Natural ([] : List Natural) = True
```
-}
let null
View
@@ -4,9 +4,9 @@ Build a list by copying the given element the specified number of times
Examples:
```
./replicate +9 Integer 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
./replicate 9 Natural 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
./replicate +0 Integer 1 = [] : List Integer
./replicate 0 Natural 1 = [] : List Natural
```
-}
let replicate
View
@@ -4,9 +4,9 @@ Reverse a list
Examples:
```
./reverse Integer [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Integer
./reverse Natural [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Natural
./reverse Integer ([] : List Integer) = [] : List Integer
./reverse Natural ([] : List Natural) = [] : List Natural
```
-}
let reverse : ∀(a : Type) → List a → List a = List/reverse in reverse
View
@@ -7,28 +7,28 @@ Examples:
```
./shifted
Bool
[ [ { index = +0, value = True }
, { index = +1, value = True }
, { index = +2, value = True }
[ [ { index = 0, value = True }
, { index = 1, value = True }
, { index = 2, value = True }
]
, [ { index = +0, value = False }
, { index = +1, value = False }
, [ { 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 = 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 }
= [ { 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 }))
@@ -79,9 +79,9 @@ Bool
(y.diff (n + length))
}
)
{ count = +0, diff = λ(_ : Natural) → nil }
{ count = 0, diff = λ(_ : Natural) → nil }
in result.diff +0
in result.diff 0
)
in shifted
View
@@ -10,15 +10,15 @@ Examples:
→ λ(zero : natural)
→ succ (succ (succ zero))
)
= +3
= 3
./build
( λ(natural : Type)
→ λ(succ : natural → natural)
→ λ(zero : natural)
→ zero
)
= +0
= 0
```
-}
let build
View
@@ -1,13 +1,13 @@
{-
Generate a list of numbers from `+0` up to but not including the specified
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 10 = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]
./enumerate +0 = [] : List Natural
./enumerate 0 = [] : List Natural
```
-}
let enumerate
View
@@ -4,9 +4,9 @@ Returns `True` if a number if even and returns `False` otherwise
Examples:
```
./even +3 = False
./even 3 = False
./even +0 = True
./even 0 = True
```
-}
let even : Natural → Bool = Natural/even in even
View
@@ -1,21 +1,21 @@
{-
`fold` is the primitive function for consuming `Natural` numbers
If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just
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
./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
λ(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
→ ./fold 3 natural succ zero
= λ(natural : Type)
→ λ(succ : natural → natural)
→ λ(zero : natural)
Oops, something went wrong.

0 comments on commit e44284b

Please sign in to comment.