class MonadAttach (m : Type u → Type v) : Type (max (u + 1) v)

For every x : m α, this type class provides a predicate MonadAttach.CanReturn x and a way to attach a proof of this predicate to the return values of x by providing an element MonadAttach.attach x of m { a : α // MonadAttach.CanReturn x a }.

Instances should abide the law Subtype.val <$> MonadAttach.attach x = x, which is encoded by the WeaklyLawfulMonadAttach type class. The stronger type class LawfulMonadAttach ensures that MonadAttach.CanReturn x is the unique strongest possible predicate.

Similarly to List.attach, the purpose of MonadAttach is to attach proof terms necessary for well-founded termination proofs. The iterator library relies on MonadAttach for combinators such as Std.Iter.filterM in order to automatically attach information about the monadic predicate's behavior that could be relevant for the termination behavior of the iterator.

Limitations:

For many monads, there is a strongly lawful MonadAttach instance, but there are exceptions. For example, there is no way to provide a computable MonadAttach instance for the CPS monad transformers StateCpsT and ExceptCpsT with a predicate that is not always True. Therefore, such CPS monads only provide the trivial MonadAttach instance MonadAttach.trivial together with WeaklyLawfulMonadAttach, but without LawfulMonadAttach.

For most monads with side effects, MonadAttach is too weak to fully capture the behavior of computations because the postcondition represented by MonadAttach.CanReturn neither depends on the prior internal state of the monad, nor does it contain information about how the state of the monad changes with the computation.

• CanReturn {α : Type u} (x : m α) (a : α) : Prop

  A predicate that can be assumed to be true for all return values a of actions x in m, in all situations.

• attach {α : Type u} (x : m α) : m (Subtype (CanReturn x))

  Attaches a proof of MonadAttach.CanReturn to the return value of x. This proof can be used to prove the termination of well-founded recursive functions.

class WeaklyLawfulMonadAttach (m : Type u → Type v) [Monad m] [MonadAttach m] : Prop

This type class ensures that every monadic action x : m α can be recovered by stripping the proof component from the subtypes returned by (MonadAttach.attach x) : m { a : α // MonadAttach.CanReturn x a } . In other words, the type class ensures that Subtype.val <$> MonadAttach.attach x = x.

• map_attach {α : Type u} {x : m α} : Subtype.val <$> MonadAttach.attach x = x

class LawfulMonadAttach (m : Type u → Type v) [Monad m] [MonadAttach m] extends WeaklyLawfulMonadAttach m : Prop

This type class ensures that MonadAttach.CanReturn is the unique strongest possible postcondition.

• map_attach {α : Type u} {x : m α} : Subtype.val <$> MonadAttach.attach x = x
• canReturn_map_imp {α : Type u} {P : α → Prop} {x : m (Subtype P)} {a : α} : MonadAttach.CanReturn (Subtype.val <$> x) a → P a

def MonadAttach.pbind {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [MonadAttach m] (x : m α) (f : (a : α) → CanReturn x a → m β) : m β

Like Bind.bind, pbind sequences two computations x : m α and f, allowing the second to depend on the value computed by the first. But other than with Bind.bind, the second computation can also depend on a proof that the return value a of x satisfies MonadAttach.CanReturn x a.

Equations

• MonadAttach.pbind x f = do let x_1 ← MonadAttach.attach x match x_1 with | ⟨a, ha⟩ => f a ha

def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m

A MonadAttach instance where all return values are possible and attach adds no information to the return value, except a trivial proof of True.

This instance is used whenever no more useful MonadAttach instance can be implemented. It always has a WeaklyLawfulMonadAttach, but usually no LawfulMonadAttach instance.

Equations

• MonadAttach.trivial = { CanReturn := fun {α : Type ?u.19} (x : m α) (x_1 : α) => True, attach := fun {α : Type ?u.19} (x : m α) => (fun (x : α) => ⟨x, True.intro⟩) <$> x }