2018-08-09 23:08:51 +03:00
|
|
|
--map/traverse
|
|
|
|
effect Noop where
|
|
|
|
noop : ∀ a . a -> {Noop} a
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
effect Noop2 where
|
|
|
|
noop2 : ∀ a . a -> a -> {Noop2} a
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
type List a = Nil | Cons a (List a)
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
map : ∀ a b e . (a -> {e} b) -> List a -> {e} (List b)
|
|
|
|
map f as = case as of
|
|
|
|
List.Nil -> List.Nil
|
|
|
|
List.Cons h t -> List.Cons (f h) (map f t)
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
c = List.Cons
|
|
|
|
z : ∀ a . List a
|
|
|
|
z = List.Nil
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
ex = (c 1 (c 2 (c 3 z)))
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
pure-map : List Text
|
|
|
|
pure-map = map (a -> "hello") ex
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
-- `map` is effect polymorphic
|
2018-09-24 20:15:40 +03:00
|
|
|
zappy : () -> {Noop} (List Nat)
|
|
|
|
zappy u = map (zap -> (Noop.noop (zap Nat.+ 1))) ex
|
2018-08-14 23:13:50 +03:00
|
|
|
|
2018-08-09 23:08:51 +03:00
|
|
|
-- mixing multiple effects in a call to `map` works fine
|
2018-09-24 20:15:40 +03:00
|
|
|
zappy2 : () -> {Noop, Noop2} (List Nat)
|
|
|
|
zappy2 u = map (zap -> Noop.noop (zap Nat.+ Noop2.noop2 2 7)) ex
|
2018-08-09 23:08:51 +03:00
|
|
|
|
2018-08-14 23:13:50 +03:00
|
|
|
()
|