PostconditionT m α
represents an operation in the monad m
together with a
intrinsic proof that some postcondition holds for the α
valued monadic result.
It consists of a predicate P
about α
and an element of m ({ a // P a })
and is a helpful tool
for intrinsic verification, notably termination proofs, in the context of iterators.
PostconditionT m
is a monad if m
is. However, note that PostconditionT m α
is a structure,
so that the compiler will generate inefficient code from recursive functions returning
PostconditionT m α
. Optimizations for ReaderT
, StateT
etc. aren't applicable for structures.
Moreover, PostconditionT m α
is not a well-behaved monad transformer because PostconditionT.lift
neither commutes with pure
nor with bind
.
- Property : α → Prop
A predicate that holds for the return value(s) of the
m
-monadic operation. The actual monadic operation. Its return value is bundled together with a proof that it satisfies
Property
.
Instances For
Lifts an operation from m
to PostconditionT m
without asserting any nontrivial postcondition.
Caution: lift
is not a lawful lift function.
For example, pure a : PostconditionT m α
is not the same as
PostconditionT.lift (pure a : m α)
.
Equations
Instances For
Lifts a monadic value from m { a : α // P a }
to a value PostconditionT m α
.
Equations
Instances For
Given a function f : α → β
, returns a a function PostconditionT m α → PostconditionT m β
,
turning PostconditionT m
into a functor.
The postcondition of the x.map f
states that the return value is the image under f
of some
a : α
satisfying the x.Property
.
Equations
Instances For
Given a function α → PostconditionT m β
, returns a a function
PostconditionT m α → PostconditionT m β
, turning PostconditionT m
into a monad.
Equations
Instances For
A version of bind
that provides a proof of the previous postcondition to the mapping function.
Equations
Instances For
Lifts an operation from m
to PostConditionT m
and then applies PostconditionT.map
.
Equations
Instances For
Converts an operation from PostConditionT m
to m
, discarding the postcondition.