From 8bc34b1277a4bc17216c7d225e108aadd1b54070 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Mon, 5 Oct 2026 17:33:09 -0500 Subject: [PATCH] feat(FreeM): relate indexed and polynomial free monads MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `PFunctor.ofFamily F`, whose shapes package an operation `F ι` with its answer type `ι`, and the equivalence `Cslib.FreeM F α ≃ (PFunctor.ofFamily F).FreeM α`. Both conversions are monad morphisms and commute with `foldFreeM` and `liftM`. Co-Authored-By: Claude Opus 5.5 --- Cslib.lean | 1 + Cslib/Foundations/Control/Monad/Free.lean | 3 +- .../Control/Monad/Free/PFunctor.lean | 172 ++++++++++++++++++ Cslib/Foundations/Data/PFunctor/Basic.lean | 9 +- Cslib/Foundations/Data/PFunctor/Free.lean | 3 + CslibTests/PFunctorFree.lean | 15 ++ 6 files changed, 201 insertions(+), 2 deletions(-) create mode 100644 Cslib/Foundations/Control/Monad/Free/PFunctor.lean diff --git a/Cslib.lean b/Cslib.lean index 5cfc781da..2a02ed39b 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -117,6 +117,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects public import Cslib.Foundations.Control.Monad.Free.Fold +public import Cslib.Foundations.Control.Monad.Free.PFunctor public import Cslib.Foundations.Control.Monad.IsMonadHom public import Cslib.Foundations.Control.Monad.IsMonadHom.List public import Cslib.Foundations.Data.BiTape diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean index f828eae5e..0ae1ac003 100644 --- a/Cslib/Foundations/Control/Monad/Free.lean +++ b/Cslib/Foundations/Control/Monad/Free.lean @@ -41,7 +41,8 @@ This unique interpreter is `FreeM.liftM f` For elimination and interpretation theory, see `Free/Fold.lean`. For polynomial effect signatures with explicit operation shapes and positions, see -`Cslib.Foundations.Data.PFunctor.Free`. +`Cslib.Foundations.Data.PFunctor.Free`; `Cslib.Foundations.Control.Monad.Free.PFunctor` relates +the two free monads. See the Haskell [freer-simple](https://hackage.haskell.org/package/freer-simple) library for the Haskell implementation that inspired this approach. diff --git a/Cslib/Foundations/Control/Monad/Free/PFunctor.lean b/Cslib/Foundations/Control/Monad/Free/PFunctor.lean new file mode 100644 index 000000000..dd7be20ce --- /dev/null +++ b/Cslib/Foundations/Control/Monad/Free/PFunctor.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2026 Devon Tuma. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +public import Cslib.Foundations.Control.Monad.Free.Fold +public import Cslib.Foundations.Data.PFunctor.Basic +public import Cslib.Foundations.Data.PFunctor.Free.Fold + +/-! +# Indexed effects as polynomial effects + +An operation `op : F ι` of a type-indexed effect family `F` is a shape of the polynomial functor +`PFunctor.ofFamily F`, whose directions are the answers `ι`. This file shows that the free monads +`Cslib.FreeM F` and `(PFunctor.ofFamily F).FreeM` are isomorphic, compatibly with folds and +monadic interpretation, so programs over indexed effects can use the `PFunctor.FreeM` API. +The price is the shape universe `max (u + 1) v` of `PFunctor.ofFamily F`. + +## Main definitions + +- `Cslib.FreeM.toPFunctorFreeM`, `Cslib.FreeM.ofPFunctorFreeM`: the conversions. +- `Cslib.FreeM.equivPFunctorFreeM`: the conversions as an equivalence. + +## Main statements + +- `Cslib.FreeM.isMonadHom_toPFunctorFreeM`, `Cslib.FreeM.isMonadHom_ofPFunctorFreeM`: both + conversions are monad morphisms. +- `Cslib.FreeM.foldFreeM_toPFunctorFreeM`, `Cslib.FreeM.liftM_toPFunctorFreeM`: folds and + interpretations agree on both presentations. +-/ + +@[expose] public section + +universe u v w w' z + +namespace Cslib.FreeM + +variable {F : Type u → Type v} {α : Type w} {β : Type w'} + +/-- Regard a program over the effect family `F` as a program over `PFunctor.ofFamily F`. -/ +def toPFunctorFreeM : FreeM F α → (PFunctor.ofFamily F).FreeM α + | .pure a => .pure a + | .liftBind (ι := ι) op cont => .liftBind ⟨ι, op⟩ fun b => toPFunctorFreeM (cont b) + +/-- Regard a program over `PFunctor.ofFamily F` as a program over the effect family `F`. -/ +def ofPFunctorFreeM : (PFunctor.ofFamily F).FreeM α → FreeM F α + | .pure a => .pure a + | .liftBind op cont => .liftBind op.2 fun b => ofPFunctorFreeM (cont b) + +@[simp] +theorem toPFunctorFreeM_pure (a : α) : toPFunctorFreeM (pure a : FreeM F α) = pure a := rfl + +@[simp] +theorem toPFunctorFreeM_lift {ι : Type u} (op : F ι) : + toPFunctorFreeM (lift op) = PFunctor.FreeM.lift (P := .ofFamily F) ⟨ι, op⟩ := rfl + +@[simp] +theorem toPFunctorFreeM_bind (x : FreeM F α) (f : α → FreeM F β) : + toPFunctorFreeM (x.bind f) = (toPFunctorFreeM x).bind fun a => toPFunctorFreeM (f a) := by + induction x with + | pure a => rfl + | lift_bind op cont ih => + exact congrArg (PFunctor.FreeM.liftBind (P := .ofFamily F) ⟨_, op⟩) (funext ih) + +@[simp] +theorem toPFunctorFreeM_map (f : α → β) (x : FreeM F α) : + toPFunctorFreeM (x.map f) = (toPFunctorFreeM x).map f := by + induction x with + | pure a => rfl + | lift_bind op cont ih => + exact congrArg (PFunctor.FreeM.liftBind (P := .ofFamily F) ⟨_, op⟩) (funext ih) + +@[simp] +theorem toPFunctorFreeM_bind' {α β : Type w} (x : FreeM F α) (f : α → FreeM F β) : + toPFunctorFreeM (x >>= f) = toPFunctorFreeM x >>= fun a => toPFunctorFreeM (f a) := + toPFunctorFreeM_bind x f + +@[simp] +theorem toPFunctorFreeM_map' {α β : Type w} (f : α → β) (x : FreeM F α) : + toPFunctorFreeM (f <$> x) = f <$> toPFunctorFreeM x := + toPFunctorFreeM_map f x + +@[simp] +theorem ofPFunctorFreeM_pure (a : α) : + ofPFunctorFreeM (pure a : (PFunctor.ofFamily F).FreeM α) = pure a := rfl + +@[simp] +theorem ofPFunctorFreeM_lift (op : (PFunctor.ofFamily F).A) : + ofPFunctorFreeM (PFunctor.FreeM.lift op) = lift op.2 := rfl + +@[simp] +theorem ofPFunctorFreeM_bind (x : (PFunctor.ofFamily F).FreeM α) + (f : α → (PFunctor.ofFamily F).FreeM β) : + ofPFunctorFreeM (x.bind f) = (ofPFunctorFreeM x).bind fun a => ofPFunctorFreeM (f a) := by + induction x with + | pure a => rfl + | lift_bind op cont ih => exact congrArg (liftBind op.2) (funext ih) + +@[simp] +theorem ofPFunctorFreeM_map (f : α → β) (x : (PFunctor.ofFamily F).FreeM α) : + ofPFunctorFreeM (x.map f) = (ofPFunctorFreeM x).map f := by + induction x with + | pure a => rfl + | lift_bind op cont ih => exact congrArg (liftBind op.2) (funext ih) + +@[simp] +theorem ofPFunctorFreeM_bind' {α β : Type w} (x : (PFunctor.ofFamily F).FreeM α) + (f : α → (PFunctor.ofFamily F).FreeM β) : + ofPFunctorFreeM (x >>= f) = ofPFunctorFreeM x >>= fun a => ofPFunctorFreeM (f a) := + ofPFunctorFreeM_bind x f + +@[simp] +theorem ofPFunctorFreeM_map' {α β : Type w} (f : α → β) (x : (PFunctor.ofFamily F).FreeM α) : + ofPFunctorFreeM (f <$> x) = f <$> ofPFunctorFreeM x := + ofPFunctorFreeM_map f x + +@[simp] +theorem ofPFunctorFreeM_toPFunctorFreeM (x : FreeM F α) : + ofPFunctorFreeM (toPFunctorFreeM x) = x := by + induction x with + | pure a => rfl + | lift_bind op cont ih => exact congrArg (liftBind op) (funext ih) + +@[simp] +theorem toPFunctorFreeM_ofPFunctorFreeM (x : (PFunctor.ofFamily F).FreeM α) : + toPFunctorFreeM (ofPFunctorFreeM x) = x := by + induction x with + | pure a => rfl + | lift_bind op cont ih => exact congrArg (PFunctor.FreeM.liftBind op) (funext ih) + +/-- Programs over an effect family are equivalent to programs over its polynomial functor. -/ +@[simps] +def equivPFunctorFreeM : FreeM F α ≃ (PFunctor.ofFamily F).FreeM α where + toFun := toPFunctorFreeM + invFun := ofPFunctorFreeM + left_inv := ofPFunctorFreeM_toPFunctorFreeM + right_inv := toPFunctorFreeM_ofPFunctorFreeM + +theorem isMonadHom_toPFunctorFreeM : + IsMonadHom (FreeM F) (PFunctor.ofFamily F).FreeM toPFunctorFreeM := + .mk' toPFunctorFreeM_pure toPFunctorFreeM_bind + +theorem isMonadHom_ofPFunctorFreeM : + IsMonadHom (PFunctor.ofFamily F).FreeM (FreeM F) ofPFunctorFreeM := + .mk' ofPFunctorFreeM_pure ofPFunctorFreeM_bind + +/-- Folding a program agrees with folding its polynomial presentation. -/ +theorem foldFreeM_toPFunctorFreeM {γ : Type z} (onValue : α → γ) + (onEffect : {ι : Type u} → F ι → (ι → γ) → γ) (x : FreeM F α) : + (toPFunctorFreeM x).foldFreeM onValue (fun op : (PFunctor.ofFamily F).A => onEffect op.2) = + x.foldFreeM onValue onEffect := by + induction x with + | pure a => rfl + | lift_bind op cont ih => exact congrArg (onEffect op) (funext ih) + +/-- Interpreting a program agrees with interpreting its polynomial presentation. -/ +theorem liftM_toPFunctorFreeM {m : Type u → Type z} [Monad m] {α : Type u} + (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) : + (toPFunctorFreeM x).liftM (fun op : (PFunctor.ofFamily F).A => interp op.2) = + x.liftM interp := by + rw [PFunctor.FreeM.liftM_eq_foldFreeM, liftM_eq_foldFreeM, ← foldFreeM_toPFunctorFreeM] + +theorem liftM_ofPFunctorFreeM {m : Type u → Type z} [Monad m] {α : Type u} + (interp : {ι : Type u} → F ι → m ι) (x : (PFunctor.ofFamily F).FreeM α) : + (ofPFunctorFreeM x).liftM interp = + x.liftM (fun op : (PFunctor.ofFamily F).A => interp op.2) := by + rw [← liftM_toPFunctorFreeM, toPFunctorFreeM_ofPFunctorFreeM] + +end Cslib.FreeM diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean index b6418d909..e766170d8 100644 --- a/Cslib/Foundations/Data/PFunctor/Basic.lean +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -16,6 +16,7 @@ Definitions of common `PFunctor` constructions: - `monomial A B`: constant direction `B` for any shape `a : A` - `P + Q`: shapes are a disjoint sum, directions are defined by sum elimination on `a : P.A ⊕ Q.A` - `P * Q`: shapes are pairs of underlying shapes, directions are a disjoint sum over both shapes. +- `ofFamily F`: shapes are operations `F ι` paired with their answer type `ι`, the directions. Special cases `C`, `linear`, `selfMonomial`, `purePower`, the indeterminate `y`, and canonical choices of `0` and `1` are defined as abbreviations or instances over `monomial`. @@ -26,7 +27,7 @@ The child-map API includes `const`, `Unary`, and `DecidableEqChildren`. @[expose] public section -universe uA uB uA₁ uA₂ uB₁ uB₂ +universe u v uA uB uA₁ uA₂ uB₁ uB₂ namespace PFunctor @@ -155,6 +156,12 @@ defined as the product of the head types and the sum of the child types. -/ end prod +/-- The polynomial functor of a type-indexed family of operations: a shape packages an operation +`op : F ι` with its answer type `ι`, which is also its type of directions. +Its free monad presents the same programs as `Cslib.FreeM F`. -/ +@[implicit_reducible] def ofFamily (F : Type u → Type v) : PFunctor.{max (u + 1) v, u} := + ⟨Σ ι, F ι, Sigma.fst⟩ + section Unary /-- A polynomial functor is unary if all child types have exactly one element. -/ diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index a26e39a02..17e1c6f36 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -54,6 +54,9 @@ With the abstract `ι`, the analogous program lives in `Type 1`, so an effect `T cannot return it; bumping the effect to `Type 1 → Type 1` pushes its programs to `Type 2`, and so on without bound. +Conversely, every `Cslib.FreeM F` is a polynomial free monad: `Cslib.FreeM.equivPFunctorFreeM` +identifies it with `(PFunctor.ofFamily F).FreeM`, whose shapes package the abstract `ι`. + This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io) library. ## Main Definitions diff --git a/CslibTests/PFunctorFree.lean b/CslibTests/PFunctorFree.lean index 9a975ffb9..6750c98a6 100644 --- a/CslibTests/PFunctorFree.lean +++ b/CslibTests/PFunctorFree.lean @@ -5,6 +5,7 @@ Authors: Devon Tuma -/ import Cslib.Foundations.Control.Monad.Free.Fold +import Cslib.Foundations.Control.Monad.Free.PFunctor import Cslib.Foundations.Data.PFunctor.Free.Fold import Cslib.Foundations.Data.PFunctor.Free.W @@ -78,6 +79,20 @@ example {F : Type u → Type v} {G : Type u → Type w} Cslib.FreeM.foldFreeM pure (fun op k => (first op).liftM second >>= k) x := by rw [Cslib.FreeM.liftM_comp, Cslib.FreeM.liftM_eq_foldFreeM] +-- Converting between the two free monads must push through `do` blocks, which use `>>=` and +-- `<$>` rather than the universe-polymorphic `bind` and `map`. +example {F : Type u → Type v} {δ ε : Type u} (x : Cslib.FreeM F δ) (f : δ → Cslib.FreeM F ε) + (g : ε → δ) : + Cslib.FreeM.toPFunctorFreeM (do let a ← x; let b ← f a; pure (g b)) = + (do let a ← x.toPFunctorFreeM; let b ← (f a).toPFunctorFreeM; pure (g b)) := by + simp + +example {F : Type u → Type v} {δ ε : Type u} (x : Cslib.FreeM F δ) + (p : δ → (PFunctor.ofFamily F).FreeM ε) (g : ε → δ) : + Cslib.FreeM.ofPFunctorFreeM (do let a ← x.toPFunctorFreeM; let b ← p a; pure (g b)) = + (do let a ← x; let b ← Cslib.FreeM.ofPFunctorFreeM (p a); pure (g b)) := by + simp + -- A nullary operation makes these W-type checks nonvacuous. private abbrev arity : PFunctor := ⟨Nat, Fin⟩