SupportMonadMorphism.lean

View source on GitHub

Reach

The reachability monad: predicates on a type. Reach a is a → Prop — the powerset monad. pure is the singleton set, bind is relational composition (existential quantification over an intermediate).

def Reach (α : Type) := α → Prop

instance : Monad Reach where
  pure := fun a x => x = a
  bind := fun s f y => &exists; x, s x ∧ f x y

MonadMorphism

A monad morphism from M to N: a natural transformation that preserves pure and bind. In software terms: a map that commutes with wrapping values and with sequencing computations. The framework lexicon maps how different communities name these same structures.

class MonadMorphism (M N : Type → Type) [Monad M] [Monad N] where
  morph : {α : Type} → M α → N α
  morph_pure : ∀ {α} (a : α), morph (pure a : M α) = (pure a : N α)
  morph_bind : ∀ {α β} (m : M α) (f : α → M β),
    morph (m >>= f) = (morph m >>= fun x => morph (f x))

instance supportMonadMorphism

Support is a monad morphism from M to Reach. The unit law (support(pure a) = {a}) follows from support_pure. The bind law (support(m >>= f) = union of support(f x) for x in support(m)) follows from support_bind.

instance supportMonadMorphism (M : Type → Type) [Monad M] [Support M] :
    MonadMorphism M Reach where
  morph := fun m => Support.support m
  morph_pure := by
    intro α a; funext x
    exact propext (Support.support_pure a x)
  morph_bind := by
    intro α β m f; funext y
    exact propext (Support.support_bind m f y)

Both laws reduce to propositional extensionality applied to the Support axioms. The proofs are one line each.

Connections

• Support.lean — imported; the Support typeclass whose laws are the monad morphism laws
• Kleisli.lean — kernels compose in M; this shows support maps them to Reach coherently