2018-08-30 20:30:49 +03:00
|
|
|
--map/traverse
|
|
|
|
effect Noop where
|
|
|
|
noop : a -> {Noop} a
|
|
|
|
|
|
|
|
type List a = Nil | Cons a (List a)
|
|
|
|
|
|
|
|
map : (a ->{} b) -> List a -> List b
|
|
|
|
map f as = case as of
|
|
|
|
List.Nil -> List.Nil
|
|
|
|
List.Cons h t -> List.Cons (f h) (map f t)
|
|
|
|
|
|
|
|
c = List.Cons
|
|
|
|
|
|
|
|
z : ∀ a . List a
|
|
|
|
z = List.Nil
|
|
|
|
|
|
|
|
ex = c 1 (c 2 (c 3 z))
|
|
|
|
|
|
|
|
pure-map : List Text
|
|
|
|
pure-map = map (a -> "hello") ex
|
|
|
|
|
|
|
|
-- this should not typecheck because map is annotated to take a pure function
|
2018-09-24 20:15:40 +03:00
|
|
|
zappy : '{Noop} (List Nat)
|
|
|
|
zappy = 'let map (zap -> Noop.noop (zap Nat.+ 1)) ex
|
2018-08-30 20:30:49 +03:00
|
|
|
|
|
|
|
pure-map
|