Select.idr

module Effect.Select

import Effects

data Selection : Effect where
     Select : List a -> { () } Selection a 

implementation Handler Selection Maybe where
     handle _ (Select xs) k = tryAll xs where
         tryAll [] = Nothing
         tryAll (x :: xs) = case k x () of
                                 Nothing => tryAll xs
                                 Just v => Just v

implementation Handler Selection List where
     handle r (Select xs) k = concatMap (\x => k x r) xs

SELECT : EFFECT
SELECT = MkEff () Selection

select : List a -> { [SELECT] } Eff m a 
select xs = call $ Select xs