Serene.Core.Result

Definitions

record Identity : Type -> Type

Totality: total
Visibility: public export
Constructor: 

Id : a -> Identity a

Projection: 

.runIdentity : Identity a -> a

Hints:

Applicative Identity

Functor Identity

Monad Identity

TransformResult Identity IO

.runIdentity : Identity a -> a

Totality: total
Visibility: public export

runIdentity : Identity a -> a

Totality: total
Visibility: public export

interface MonadResult : ((Type -> Type) -> Type -> Type) -> (Type -> Type) -> Type

  Abstraction over monad transformers that can express pure failure
  or success.
  
  The functional dependency `| m` records that the choice of inner
  monad `m` uniquely determines the transformer `r`. Note: Like `| m -> r` in
  haskell.

Parameters: r, m
Constraints: Monad m
Methods:

failure : HasMetadata md => md -> ErrorType -> String -> r m a

ok : a -> r m a

Implementation: 

Monad m => MonadResult ResultT m

failure : MonadResult r m => HasMetadata md => md -> ErrorType -> String -> r m a

Totality: total
Visibility: public export

ok : MonadResult r m => a -> r m a

Totality: total
Visibility: public export

record ResultT : (Type -> Type) -> Type -> Type

  A monad transformer whose inner computation may fail with a
  non-empty list of errors.

Totality: total
Visibility: public export
Constructor: 

MkResultT : m (Either ErrorList a) -> ResultT m a

Projection: 

.runResultT : ResultT m a -> m (Either ErrorList a)

Hints:

Monad m => Applicative (ResultT m)

Functor m => Functor (ResultT m)

HasIO m => HasIO (ResultT m)

Monad m => Monad (ResultT m)

Monad m => MonadResult ResultT m

.runResultT : ResultT m a -> m (Either ErrorList a)

Totality: total
Visibility: public export

runResultT : ResultT m a -> m (Either ErrorList a)

Totality: total
Visibility: public export

lift : Monad m => m a -> ResultT m a

  Lift a computation from the inner monad into 'ResultT'.

Totality: total
Visibility: public export

Result : Type -> Type

  A pure result computation backed by the 'Identity' monad.
  Equivalent to `Either ErrorList a`, but with a uniform interface.

Totality: total
Visibility: public export

ResultIO : Type -> Type

  A result computation that may also perform 'IO'.

Totality: total
Visibility: public export

runResult : Result a -> Either ErrorList a

  Unwrap a pure 'Result', yielding `Either ErrorList a`.

Totality: total
Visibility: public export

runResultIO : ResultIO a -> IO (Either ErrorList a)

  Run a 'ResultIO' computation, returning the result inside 'IO'.

Totality: total
Visibility: public export

absurdResult : HasMetadata md => Monad m => md -> ResultT m a

  Produce an 'Absurd' error annotated with a source file and line.

Totality: total
Visibility: public export

todo : HasMetadata md => Monad m => md -> String -> ResultT m a

  Mark an unimplemented branch with a 'TODO' error.

Totality: total
Visibility: public export

interface TransformResult : (Type -> Type) -> (Type -> Type) -> Type

  Transform the inner monad of a 'ResultT' from `m` to `n`.
  
  Instantiate this interface for each pair of monads you need to
  convert between.  The built-in instance handles the common
  `Result` → `ResultIO` case.
  
  ```idris
  liftToIO : Result a -> ResultIO a
  liftToIO = transform
  ```

Parameters: m, n
Constraints: Monad m, Monad n
Methods:

transform : ResultT m a -> ResultT n a

Implementation: 

TransformResult Identity IO

transform : TransformResult m n => ResultT m a -> ResultT n a

Totality: total
Visibility: public export