
  0 | module IO.Async.Outcome
  1 | 
  2 | import public Data.List.Quantifiers.Extra
  3 | 
  4 | %default total
  5 | 
  6 | ||| Alias for `Either (HSum es) a`: A computation that either
  7 | ||| succeeds with a result of type `a` or fails with an error
  8 | ||| of one of the types given in list `es`.
  9 | |||
 10 | ||| Note: If `es` is the empty list, the computation cannot fail,
 11 | ||| because `HSum []` is uninhabited.
 12 | public export
 13 | 0 Result : List Type -> Type -> Type
 14 | Result es a = Either (HSum es) a
 15 | 
 16 | public export
 17 | data Outcome : List Type -> Type -> Type where
 18 |   Succeeded : (res : a) -> Outcome es a
 19 |   Error     : (err : HSum es) -> Outcome es a
 20 |   Canceled  : Outcome es a
 21 | 
 22 | export
 23 | toOutcome : Result es a -> Outcome es a
 24 | toOutcome (Right v)   = Succeeded v
 25 | toOutcome (Left errs) = Error errs
 26 | 
 27 | export
 28 | Functor (Outcome es) where
 29 |   map f (Succeeded v) = Succeeded (f v)
 30 |   map _ (Error v)     = Error v
 31 |   map _ Canceled      = Canceled
 32 | 
 33 | export
 34 | Foldable (Outcome es) where
 35 |   foldr f x (Succeeded v) = f v x
 36 |   foldr f x _             = x
 37 | 
 38 |   foldl f x (Succeeded v) = f x v
 39 |   foldl f x _             = x
 40 | 
 41 |   foldMap f (Succeeded v) = f v
 42 |   foldMap f _             = neutral
 43 | 
 44 |   toList (Succeeded v) = [v]
 45 |   toList _             = []
 46 | 
 47 |   null (Succeeded v) = False
 48 |   null _             = True
 49 | 
 50 | export
 51 | Traversable (Outcome es) where
 52 |   traverse f (Succeeded v) = Succeeded <$> f v
 53 |   traverse _ (Error v)     = pure $ Error v
 54 |   traverse _ Canceled      = pure Canceled
 55 |