blob: fb97ba6070ef88a68de36545ca9d9a6be9b91467 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
let List/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
--| Concatenate a `List` of `List`s into a single `List`
List/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
-- Transform a list by applying a function to each element and flattening the results
List/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 Status = < Empty | NonEmpty : Text >
let
{-|
Transform each value in a `List` to `Text` and then concatenate them with a
separator in between each value
-}
Text/concatMapSep
: ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text
= λ(separator : Text) →
λ(a : Type) →
λ(f : a → Text) →
λ(elements : List a) →
let status =
List/fold
a
elements
Status
( λ(x : a) →
λ(status : Status) →
merge
{ Empty = Status.NonEmpty (f x)
, NonEmpty =
λ(result : Text) →
Status.NonEmpty (f x ++ separator ++ result)
}
status
)
Status.Empty
in merge { Empty = "", NonEmpty = λ(result : Text) → result } status
in { List/map, List/concat, List/concatMap, Text/concatMapSep }
|
