Proved bijection between monads and monoids in the category of endofunctors

Changes

1 changed files (+218/-24)

• Category.lean
  • @@ -44,7 +44,7 @@ https://math.andrej.com/2016/08/06/hask-is-not-a-category/
    Endofunctors in Lean! f maps objects - f.map maps morphisms + f.map or `<$>` maps morphisms `(α → β) → f α → f β` is the same thing as `(α → β) → (f α → f β)` -/ #check Functor
  • @@ -65,9 +65,7 @@ instance : LawfulFunctor List where
    /-- - Contravariant (endo)functors (normal functors are "covariant" functors) - - Also, contravariant functors are covariant functors in the opposite category + Contravariant functors (normal functors are "covariant" functors) are functors from Colean to Lean `map` turns a "producer of α" into a "producer of β" `comap` turns a "consumer of α" into a "consumer of β"
  • @@ -119,7 +117,7 @@ and so on
    /-- Composition of two functors of same variance is a functor -/ @[simp] - instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : Functor (f ∘ g) where + instance [Functor f] [Functor g] : Functor (f ∘ g) where map h x := Functor.map (f := f) (h <$> ·) x instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : LawfulFunctor (f ∘ g) where
  • @@ -166,6 +164,11 @@ instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
    #synth LawfulBifunctor Prod + -- Multivariate functors + #check MvFunctor + #check LawfulMvFunctor + + /-- Profunctors are useful for lenses -/ class Profunctor (p : Type u → Type v → Type*) where dimap : (s → a) → (b → t) → (p a b → p s t)
  • @@ -227,17 +230,15 @@ abbrev NaturalType.{u} (f : Type u → Type v) (g : Type u → Type v) :=
    class Natural f [Functor f] [LawfulFunctor f] g [Functor g] [LawfulFunctor g] (η : NaturalType f g) where naturality (h : α → β) (x : f α) : h <$> (η x) = η (h <$> x) - instance : Natural List Option List.head? where - naturality := by simp + instance : Natural List Option List.head? := + ⟨by simp⟩ def OptionToList : Option α → List α | some a => [a] | none => [] - instance : Natural Option List OptionToList where - naturality := by - simp [OptionToList] - grind + instance : Natural Option List OptionToList := + ⟨by simp [OptionToList]; grind⟩ class Conatural f [Cofunctor f] g [Cofunctor g] (η : NaturalType f g) where naturality (h : β → α) (x : f α) : h <¥> (η x) = η (h <¥> x)
  • @@ -248,8 +249,8 @@ Vertical composition of natural transformations
    Intuitively this is like doing two data moves. -/ instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] [Functor h] [LawfulFunctor h] [M : Natural f g η] [N : Natural g h μ] : - Natural f h (fun {α : Type u} ↦ @μ α ∘ @η α) where - naturality := by simp [N.naturality, M.naturality] + Natural f h (fun {α : Type u} ↦ @μ α ∘ @η α) := + ⟨by simp [N.naturality, M.naturality]⟩ /-- Horizontal composition of natural transformations
  • @@ -257,17 +258,17 @@ Horizontal composition of natural transformations
    Intuitively this is like repackaging data in nested "containers" -/ instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] : - Natural (g ∘ f) (g' ∘ f') (μ ∘ (Functor.map (f := g) η ·)) where - naturality := by simp [N.naturality, M.naturality] + Natural (g ∘ f) (g' ∘ f') (μ ∘ (Functor.map (f := g) η ·)) := + ⟨by simp [N.naturality, M.naturality]⟩ /-- Alternatively we do `μ` first and then the map second -/ instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] : - Natural (g ∘ f) (g' ∘ f') ((Functor.map (f := g') η ·) ∘ μ) where - naturality := by simp [N.naturality, M.naturality] + Natural (g ∘ f) (g' ∘ f') ((Functor.map (f := g') η ·) ∘ μ) := + ⟨by simp [N.naturality, M.naturality]⟩ /-- The two orderings are equivalent, which only requires the outer transformation to be natural -/ lemma horizontal_comp_equiv (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [N : Natural g g' μ] : - (μ ∘ (Functor.map (f := g) η ·)) x = ((Functor.map (f := g') η ·) ∘ μ) x:= by + (μ ∘ (Functor.map (f := g) η ·)) x = ((Functor.map (f := g') η ·) ∘ μ) x := by simp [N.naturality]
  • @@ -278,8 +279,8 @@ def yoneda (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] : f α
    def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : NaturalType (α → ·) f := (· <$> y) /-- Reverse map always produces a natural transformation -/ - instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where - naturality h x := by simp [yoneda']; rfl + instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) := + ⟨fun h x ↦ by simp [yoneda']; rfl⟩ /-- Mapping and unmapping a natural transformation returns the itself
  • @@ -300,8 +301,8 @@ def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := g id
    def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := (· <¥> y) /-- Reverse map always produces a natural transformation -/ - instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) where - naturality h x := by simp [coyoneda', Cofunctor.comp_comap] + instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) := + ⟨fun h x ↦ by simp [coyoneda', Cofunctor.comp_comap]⟩ /-- Same but for Coyoneda -/ theorem coyoneda_lemma (g : NaturalType (· → α) f) [Cofunctor f] [N : Conatural (· → α) f g] : coyoneda' (coyoneda g) x = g x := by
  • @@ -316,6 +317,10 @@ theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y :=
    #check Applicative #check LawfulApplicative + -- Motivation: mapping multi-arg functions + #simp (some 3).map (· * ·) + #eval (· * ·) <$> (some 3) <*> (some 4) + /-- Composition of two applicatives is an applicative -/ @[simp] instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicative g] : Applicative (f ∘ g) where
  • @@ -334,11 +339,94 @@ instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicativ
    ext simp [seq_assoc] + -- TODO: Lax monoidal functors - -- TODO: Monads + + -- Monads, "warm fuzzy things" #check Monad #check LawfulMonad + /- + Functors let us apply `α → β` to `f α` + Applicatives let us apply `f (a → β)` to `f α` + But what about applying an "effectful function" `α → f β` to `f α`? + Another use case is to compose `α → f β` and `β → f γ`. + + Kleisli category: Any monad `m` creates a category where the objects are still types but the morphisms are `α → β` for every `α → f β` in Lean. Then composition of effectful functions becomes composition of morphisms. + + This construction also motivates the monad laws. + + In fact, using `>>=` and `pure` we can implement `<$>` and `<*>` so every monad is also a functor and applicative. + + Exercise: Find an example of a functor which is not applicative and an applicative which is not a monad. + -/ + + #synth Monad Option + + #synth Monad IO + + #synth Monad (StateM ℕ) + + #synth Monad (Writer ℕ) + + #synth Monad (ST ℕ) + + #synth Monad (Except String) + + #synth Monad (Sum ℕ) + + instance : LawfulMonad Option := + LawfulMonad.mk' Option + (id_map := by simp) + (pure_bind := by simp [Option.bind]) + (bind_assoc := by simp; grind) + (bind_pure_comp := by simp [Option.map]; grind) + + #synth Monad List + + #synth LawfulMonad List + + + /-- + This function looks ugly, but we can simplify it with `do` notation, which is syntactic sugar that lets us unwrap monadic values and automatically inserts `>>=` when we use the unwrapped values + + https://slightknack.dev/blog/do-notation/ + -/ + def option_div (x_wrapped : Option ℕ) (y_wrapped : Option ℕ) : Option ℚ := + y_wrapped >>= fun y ↦ + if y = 0 then + none + else + x_wrapped >>= fun x ↦ some <| x / y + + #eval option_div (some 3) (some 0) + + def option_div' (x_wrapped : Option ℕ) (y_wrapped : Option ℕ) : Option ℚ := do + let x ← x_wrapped + let y ← y_wrapped + if y = 0 then none else some <| x / y + + /-- Even the identity monad is powerful! -/ + def Array.insSort [LinearOrder α] (A : Array α) := Id.run do + let N := A.size + let mut A := A.toVector + for hi : i in [:N] do + for hj : j in [:i] do + have := Membership.get_elem_helper hi rfl + if A[i - j] < A[i - j - 1] then + A := A.swap (i - j - 1) (i - j) + else + break + return A.toArray + + /-- List monad demo -/ + def UpToN (xs : List ℕ) : List ℕ := do + let x ← xs + let y ← List.range x + return y + + #eval UpToN [1, 2, 3] + /- Sadly, in general monads do not compose 😿 https://carlo-hamalainen.net/2014/01/02/applicatives-compose-monads-do-not/
  • @@ -346,4 +434,110 @@ https://carlo-hamalainen.net/2014/01/02/applicatives-compose-monads-do-not/
    However, in some cases we can use monad transformers to compose them. -/ - -- TODO: Kleisi categories + + -- Equivalent definition using "fish" + #check Bind.kleisliRight + -- Equivalent definition using "join" + #check joinM + -- Exercise: Implement bind using fish + + /- + "A monad is just a monoid in the category of endofunctors" + + https://old.reddit.com/r/math/comments/ap25mr/a_monad_is_a_monoid_in_the_category_of/ + + The category of Lean endofunctors + Objects: Endofunctors + Morphisms: Natural transformations + -/ + + /-- Vertical composition is associative -/ + lemma nat_trans_comp_assoc (η : NaturalType f g) (μ : NaturalType g h) (ν : NaturalType h i) [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] [Functor h] [LawfulFunctor h] [Functor i] [LawfulFunctor i] : + ((ν ∘ μ) ∘ η) x = (ν ∘ μ ∘ η) x := by + simp only [Function.comp_assoc] + + #check Monoid + + /- + A monoidal category is a category C equipped with a tensor product ⨂ from C × C to C and an identity object I with certain properties. + + For the category of Lean endofunctors, let ⨂ be functor composition and I be the identity functor `Id`. + -/ + + /-- ⨂ is obviously associative -/ + lemma functor_comp_assoc [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] [Functor h] [LawfulFunctor h] : (f ∘ g) ∘ h = f ∘ g ∘ h := by + apply Function.comp_assoc + + /-- `Id` is an identity for ⨂ -/ + lemma functor_left_id [Functor f] [LawfulFunctor f] : id ∘ f = f := by + simp + + /-- `Id` is an identity for ⨂ -/ + lemma functor_right_id [Functor f] [LawfulFunctor f] : f ∘ id = f := by + simp + + -- The coherence conditions (insert scary pentagon diagram here) are automatically satisfied because the associator and unitor natural isomorphisms are equalities. + + /- + A monoidal object is an object M in (C, ⨂, I) with an arrow μ from M ⨂ M to M and η from I to M such that μ is associative and η is an identity with respect to μ. + + A monoidal object in the category of Lean endofunctors is a functor with natural transformations `join` (corresponding to μ) and `pure` (η) with the following properties: + -/ + + class EndofunctorMonoid m extends Functor m, LawfulFunctor m where + join : NaturalType (m ∘ m) m + pure : NaturalType Id m + join_pure : (join ∘ pure) x = x + join_map_pure : (join ∘ (Functor.map (f := m) pure ·)) x = x + join_join : (join ∘ (Functor.map (f := m) join ·)) x = (join ∘ join) x + + @[simp] + def bindFromJoin [EndofunctorMonoid m] (join : NaturalType (m ∘ m) m) (x : m α) (f : α → m β) := + join (Functor.map (f := m) f x) + + @[simp] + instance [EndofunctorMonoid m] : Monad m where + pure := EndofunctorMonoid.pure + bind := bindFromJoin EndofunctorMonoid.join + + /-- A monoid in the category of endofunctors is a monad -/ + instance [EndofunctorMonoid m] [J : Natural (m ∘ m) m EndofunctorMonoid.join] [P : Natural Id m EndofunctorMonoid.pure] : LawfulMonad m := + LawfulMonad.mk' m id_map + (pure_bind := fun x f ↦ by + simp [P.naturality, Functor.map] + exact EndofunctorMonoid.join_pure) + (bind_assoc := fun x f g ↦ by + have := EndofunctorMonoid.join_join (x := (fun a ↦ Functor.map (f := m) g (f a)) <$> x) + simp at this + simp [J.naturality, ← this]) + (map_const := by simp [map_const]) + (bind_pure_comp := fun f x ↦ by + have := EndofunctorMonoid.join_map_pure (x := f <$> x) + simp at this + exact this) + + @[simp] + def joinFromBind [Monad m] (bind : {α β : Type u} → m α → (α → m β) → m β) (x : m (m α)) := + bind x id + + /-- A monad is a monoid in the category of endofunctors -/ + @[simp] + instance [Monad m] [LawfulMonad m] : EndofunctorMonoid m where + pure := pure + join := joinFromBind bind + join_pure := by simp + join_map_pure := by simp + join_join := by simp + + instance [Monad m] [LawfulMonad m] : Natural (m ∘ m) m EndofunctorMonoid.join := + ⟨by simp⟩ + + instance [Monad m] [LawfulMonad m] : Natural Id m EndofunctorMonoid.pure := + ⟨by simp [Functor.map]⟩ + + /-- `bindFromJoin` and `joinFromBind` form a bijection -/ + theorem bind_join_equiv [Monad m] [LawfulMonad m] : (bindFromJoin (m := m) (joinFromBind bind)) x f = bind x f := by + simp + + theorem bind_join_equiv' [E : EndofunctorMonoid m] : joinFromBind (bindFromJoin E.join) x = E.join x := by + simp