Control.Monad.Partial

Definitions

data Partial : Type -> Type

  Delay/partiality monad. Represents partial computations which may not
  terminate or cover all inputs. This can be preferable to defining a partial
  Idris function as it allows termination to be proven as an external proof.

Totality: total
Visibility: public export
Constructors:

Now : a -> Partial a

Later : Inf (Partial a) -> Partial a

Hints:

Applicative Partial

Functor Partial

Monad Partial

never : Partial a

  A partial computation which never terminates (aka. undefined/bottom).

Totality: total
Visibility: public export

data Total : Partial a -> Type

Totality: total
Visibility: public export
Constructors:

TNow : (x : a) -> Total (Now x)

TLater : Total (Force x) -> Total (Later x)

runPartial : (0 _ : Total x) -> a

  Extract the value from a partial computation if you have a proof it is
  actually total.

Totality: total
Visibility: public export