/Prelude-v23.0.0/Map/mapMaybe.dhall

Copy path to clipboard

Examples

  mapMaybe
Text
Natural
Text
( λ(n : Natural) →
if Natural/isZero n then None Text else Some (Natural/show n)
)
(toMap { foo = 2, bar = 0 })
≡ toMap { foo = "2" }

Source

--| Apply a function across the values of a `Map k v`, dropping
-- entries whose values return `None`.
let Map/empty =
missing sha256:4c612558b8bbe8f955550ed3fb295d57b1b864c85cd52615b52d0ee0e9682e52
? ./empty.dhall

let Map/unpackOptionals =
missing sha256:66c3e6f6f81418cf99342e1dba739617c01af4b27c1ca5e2e1d7bce64a522e22
? ./unpackOptionals.dhall

let Map/map =
missing sha256:23e09b0b9f08649797dfe1ca39755d5e1c7cad2d0944bdd36c7a0bf804bde8d0
? ./map.dhall

let Map/Type =
missing sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed
? ./Type.dhall

let mapMaybe
: ∀(k : Type) →
∀(a : Type) →
∀(b : Type) →
(a → Optional b) →
Map/Type k a →
Map/Type k b
= λ(k : Type) →
λ(a : Type) →
λ(b : Type) →
λ(f : a → Optional b) →
λ(m : Map/Type k a) →
Map/unpackOptionals k b (Map/map k a (Optional b) f m)

let property =
λ(k : Type) →
λ(a : Type) →
λ(b : Type) →
λ(f : a → Optional b) →
assert : mapMaybe k a b f (Map/empty k a) ≡ Map/empty k b

let example0 =
assert
: mapMaybe
Text
Natural
Text
( λ(n : Natural) →
if Natural/isZero n then None Text else Some (Natural/show n)
)
(toMap { foo = 2, bar = 0 })
≡ toMap { foo = "2" }

in mapMaybe