git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/effects/Effect/Select.idr
23 lines 585 B history raw
1module Effect.Select
3import Effects
5data Selection : Effect where
6 Select : List a -> { () } Selection a
8instance Handler Selection Maybe where
9 handle _ (Select xs) k = tryAll xs where
10 tryAll [] = Nothing
11 tryAll (x :: xs) = case k x () of
12 Nothing => tryAll xs
13 Just v => Just v
15instance Handler Selection List where
16 handle r (Select xs) k = concatMap (\x => k x r) xs
18SELECT : EFFECT
19SELECT = MkEff () Selection
21select : List a -> { [SELECT] } Eff a
22select xs = call $ Select xs