git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/libs/effects/Effect/Select.idr
25 lines 614 B history raw
1module Effect.Select
3import Effects
5%access public export
7data Selection : Effect where
8 Select : List a -> sig Selection a ()
10implementation Handler Selection Maybe where
11 handle _ (Select xs) k = tryAll xs where
12 tryAll [] = Nothing
13 tryAll (x :: xs) = case k x () of
14 Nothing => tryAll xs
15 Just v => Just v
17implementation Handler Selection List where
18 handle r (Select xs) k = concatMap (\x => k x r) xs
20SELECT : EFFECT
21SELECT = MkEff () Selection
23select : List a -> Eff a [SELECT]
24select xs = call $ Select xs