1.1. Repository

The code for the «freely» (Lean 4) library is hosted on GitHub at:

• https://github.com/liminalisht/freely

For information on license, citation, and use of «freely», take a look at this section.

1.2. Language

«freely» is written in Lean 4, a functional language built for formal verification.

Those new to Lean should carve out some time to take a look at our Lean 4 resources.

1.3. Dependencies

«freely» has minimal dependencies. Specifically, «freely» does not depend on mathlib.

Additionally, we should note that «freely» does not depend upon «freely-docs», «freely-log», or «freely-tests». Instead, those libraries depend upon «freely». This means that «freely» does not depend upon verso (only subverso).

1.4. Purpose of «freely»

As a library, «freely» attempts to realize the slogan "free(r) syntax, modular semantics". It attempts to achieve this by equipping signatures / protocols written in continuation-passing style (CPS) with their initial interpreters, using the free(r) monad, so that meaning is stable (essentially unique), compositional (monadic), and portable (functorial).

The idea, roughly speaking, is that:

• programs should be written using free(r) monads (Freer «Σ» α, i.e. ℙ «Σ» α) over (DSL) signatures «Σ»)

• (DSL) signatures «Σ» should be functorial expressions of the syntax of a domain specific language (e.g. «Σ_Foo», «Σ_Bar»,«Σ_Foo⊕Bar» etc.), so that they admit of composition and combination via functor combinators

• handlers should be natural transformations (Handler «Σ» m, i.e «Σ» ⟹ᶠ m) mapping signature functors («Σ») to endofunctors / monads m : Type u → Type u

• interpretations should be realized as canonical folds/catamorphisms ∀ {α}, ℙ «Σ» α → m α that employ handlers «Σ» ⟹ᶠ m to interpret programs ℙ «Σ» α in monadic execution contexts.

Under such an arrangement, composing DSLs and optimizing interpretations of programs can be done using standard categorical constructions, rather than bespoke machinery, or mechanisms tightly bound to any specific domain.

1.5. «freely», at a glance (where to start)

When read in order (top-down), this document presents «freely» in a continuous narrative, starting with the motivation driving the creation of the library, the notation used in «freely» (and throughout this document), and «freely»'s relationship to prior art, before diving into its category theoretic grounding, and finally presenting a thorough, module-by-module presentation of its code.

But that is only one way to read this document. This document can be read in many different orders, depending upon pedogogical purposes, and personal interests. So please feel free to skip around!

If you're eager to just dive into the core code abstractions behind the library, you might begin with:

• Freely.Program.Monad.Freer for the free(r) monad and fold, or

• Freely.Handler.Interpret for interpret and handler typing

If you want to see basic examples of using «freely», you might take a look at:

• «freely-log», or

• «freely-tests»

«freely-log» establishes a logging DSL and handlers, while «freely-tests» reuses the logging DSL and handlers in the course of building a tests DSL and handlers, which it then uses to write tests for «freely» itself. Both «freely-log» and «freely-tests» give an initial flavor of what it's like to use the «freely» abstractions to build DSL, handlers, and interpreters, and to compose them into larger DSLs, etc.

If you're eager to see tests witnessing both usage of freely abstractions and laws governing (algebraic) reasoning, see:

• the test suite FreelyTests.Suites.Freely

Finally, we have attempted to link to nLab where appropriate when categorical notions are introduced. We encourage readers unfamiliar with such notions to follow these links to get a better appreciation of the generality and scope of the notions involved, understanding that any link to nLab is a link to a rabbit hole of potentially infinite depth.

1.6. Motivation behind «freely»

We understand our goal to be to enable "free(r) expression" by offering avenues for leveraging "freer syntax" and "modular semantics". This must entail (at a minimum) the ability:

• to author programs against many different (domain specific) languages

• to be able to compose these languages, permitting their extension, their embedding in larger languages, and the like

• to be able to reuse programs written in these languages, allowing interpretations of higher languages to delegate to interpretations of lower languages, etc., and

• to be able to defer the meaning of programs until interpretation (permitting freely replacing, substituting, and extending interpretations)

Free(r) expression must always contend with the fundamental obstacle to communication we always face: viz. that you don't already know what I mean. To communicate, I must send you (serialized) data, and you must interpret that (de-serialized) data in some way that you presume coheres with my intended meaning.

If we separate syntax (data) from semantics (interpretations of data) in a principled way that anticipates their structured recombination, then we can presumably express what it is that we mean in a way that supports advanced reasoning and optimization of programs and their interpretations.

The «freely» library models (domain-specific) languages by endofunctors «Σ» : Type u → Type u (effect signatures). When one builds programs as free objects over «Σ» (sequential programs via a free(r) monad, or - planned but not yet reified in code - parallel programs via a free(r) applicative), one can then give expression(s) in languages semantic meaning by defining handlers from the languages into monadic contexts, i.e. by defining natural transformations θ : «Σ» ⟹ᶠ m. The «freely» library supplies folds/catamorphisms, as well as various combinators, so that composition, extension, and rewriting follow from universal properties and naturality conditions.

1.7. Separating Syntax from Semantics

When using «freely», you will:

• write programs purely against Freer (a.k.a. ℙ «Σ») for sequential programs, or (planned, not yet implemented) FreeA «Σ» (for parallel programs)

• supply handlers θ : «Σ» ⟹ᶠ m to answer questions, i.e. to supply the semantic meaning of expressions employed in programs

Under this approach, programs involve elaborating expressions that you may think of as asking questions that are meant to be answered by handlers. Programs are entirely syntactic constructs, and are independent from their interpretation(s). Crucially, just as DSLs can be composed, handlers can be composed too. Interpretation provides a canonical way to "run" a handler, and because it is a catamorphism / fold, any algebra we put on handlers is preserved through this fold.

1.8. How is this "free(r)" expression?

In its fullest expression, a guiding goal of «freely» is to enable us to write programs once, and reuse them myriad times, to perform radically different effects. Separating the syntactic layer from the semantic layer allows us to manipulate both algebraically, and to share highly reusable programmatic logic, pushing (substitutable, algebraically manipulable) handlers to the boundaries of the program. Further, because DSLs can be composed, programs written in one language can be lifted / embedded into larger languages. A high level language's semantics can involve interpreting programs written in a lower level language, and the functorial combinatorics of how languages and handlers compose is available to us.

In sum, though there are a great many disparate goals that the «freely» library aims to support, most of them invariably revolve around freely using, reusing, composing, and substituting syntactic and semantic constructs to facilitate conveyance of meaning in a composable, reusable way.

1.9. Disclaimer

This is experimental software. «freely» is in its infancy. I am a (principal) software engineer with experience in Haskell, functional programming, and retail pricing, first and foremost - as well as a student of philosophy - but I am not a mathematician, nor a category theorist. Consider this work a modest submission in the vein of "applied" category theory, understanding that those of us (like me) who attempt such an application are sometimes in need of guidance and correction on mathematical topics that exceed our training. In other words: caveat emptor.

If you find errors in reasoning and the like, please notify me on Zulip, or create a Github issue in the «freely» repo.

For more information on the author, see this section at the bottom of this document.

3.1. Prior art around Free(r)

3.2. Prior art around Functor Combinators

In truth, the aim is to extend the idea even further than this, as far as we can take it:

• to take syntax / data structures, and lift to the functor level

• to unlock algebraic ways to combine expressions, embed expressions, rewrite expressions, and perform substitution on expressions, and

• to take the semantic handlers of languages and compose them, chain them, replace them, and so on.

In other words, we aim to utilize and structure the relationship between syntax and semantics so as to freely aid the conveyance of meaning, however articulated.

Dedication

Just what is one to do with extremely abstract concepts?

If nothing else, «freely» may be of use to those who wish somehow to ground the real, computable world, in the abstract world of categorical concepts and abstractions, and vice versa.

4.1. Universe levels and smallness

Lean has a cumulative hierarchy \mathbf{Type}_0 \;\subseteq\; \mathbf{Type}_1 \;\subseteq\; \mathbf{Type}_2 \;\subseteq\; \cdots \quad\text{with}\quad \mathbf{Type}_u : \mathbf{Type}_{u+1}

The bare identifier Type is syntactic sugar for Type 0.

Fixing 𝒞 = Type (i.e. Type 0) can sometimes prove to be too small. Generic constructions (free monads, handlers, etc.) may sometimes need to live at an arbitrary higher level.

Thus, we work universe-polymorphically with a parameter u and set 𝒞 := Type u.

4.2. Type u has a cartesian-closed core with finite coproducts

Equipped with functions as morphisms, the core of 𝒞 := Type u (a.k.a. \mathbf{Type}_u) has:

• Products (X × Y) with terminal object PUnit

• Coproducts (X ⊕ Y) with initial object PEmpty

• Exponentials (Y^X), i.e. the internal hom(X,Y)

In a cartesian closed category the canonical monoidal structure is the cartesian one, so the tensor is literally the categorical product: ((\mathcal C, \times, 1)) is symmetric monoidal. It is traditional to write × to signal “product” (with its projections and universal cone), reserving ⊗ for a generic monoidal tensor that need not be cartesian. We regard ((\mathbf{Type}_u, \times, \mathbf{1})) as a symmetric monoidal category (cartesian monoidal), so that the "tensor" coincides with cartesian product; but we keep the symbol × here to avoid confusion with the tensor ⊗ᶠ on signatures.

This will allow us to meet the hypotheses used in the rest of the abstract presentation of the library: viz. the presentation in terms of polynomial endofunctors, free monads, and strengths/distributivity laws.

4.3. Endofunctors, free monads, and handlers at universe level u

With 𝒞 := Type u fixed, a signature is an endofunctor «Σ» : Type u → Type u. Additionally, the free monad ℙ «Σ», handlers into semantic monads (M : \mathcal C \to \mathcal C), and interpreters are all also endomorphisms on \mathbf{Type}_u. No universe shifts are introduced by the core API.

4.4. Why not bare Type?

• Type means Type 0. Restricting ourselves in this way would needlessly forbid using signatures or semantic monads that live in a higher universe (e.g. when data mentions large indices). We would then be forced into ULift plumbing or ad-hoc casts.

• Using Type u makes every theorem and definition universe-polymorphic, so they instantiate uniformly at any desired level.

4.5. «freely» design contract

• We fix a universe u and set ( \mathcal C := \mathbf{Type}_u ).

• We work with DSL signatures that are endofunctors ( «Σ» : Type u → Type u ).

• We construct the free monad ( ℙ «Σ» ) on the same (\mathcal C).

• We construct handlers from «Σ» into M with M of type \mathcal C \to \mathcal C.

• We use the initiality of ((\mathbb T,\alpha)) in the category Mnd^(«Σ») of such pairs to obtain a unique interpreter.

All categorical claims in the «freely» manual (polynomials, sums, initiality, commuting squares) specialize to the concrete model ( \mathcal C = \mathbf{Type}_u ), while remaining universe-polymorphic.

5.1. An overview of the categorical picture pursued in «freely»

Let 𝒞 = Type u and let a signature be an endofunctor «Σ» : 𝒞 ⟶ 𝒞.

«freely» pursues the viewpoint that we can have:

• a Free monad ℙ «Σ» (our Freer «Σ») with unit ηᵀ : Id ⇒ ℙ and the universal transformation ↑ᵀ : «Σ» ⟹ᶠ ℙ «Σ»

  Our Freer is the continuation-passing style (CPS) free-monad encoding which is operationally the "freer monad" of Kiselyov & Ishii

  The core idea is that ℙ «Σ» is initial among monads m with a natural transformation «Σ» ⟹ᶠ m, and that our catamorphism / fold (cataFreer) should realize the unique monad morphism. This is what the Freer monad instance should encode operationally.

  🔗inductive type

  Freely.Freer.{u, v} (F : Type u → Type v) (α : Type u) :
    Type (max (u + 1) v)
  Freely.Freer.{u, v} (F : Type u → Type v)
    (α : Type u) : Type (max (u + 1) v)

  Freer F (notation: ℙ F) — the free monad on a mapping F : Type u → Type v.

  Mathematically, Freer F is the initial object among monads M equipped with a natural transformation F ⇒ M. Operationally it is the syntax of programs freely built from F-effects and pure.

  pure : α → ℙ F α injects a return value.

  freer : F β → (β → ℙ F α) → ℙ F α is the “one effect then continue” step.

  Universe: if F : Type u → Type v, then ℙ F : Type u → Type (max (u+1) v).

  Constructors

  pure.{u, v} {F : Type u → Type v} {α : Type u} : α → ℙ F α

  Monad unit of the CPS freer monad. Categorical reading. The unit ηᵀ : Id ⇒ T for T = Freer Σ, inserting a variable as a leaf (no Σ-node). Laws (as monad morphism obligations for the interpreter): interpret ∘ pure = pure, and bind (pure x) k = k x.

  freer.{u, v} {F : Type u → Type v} {α β : Type u} :
    F β → (β → ℙ F α) → ℙ F α

  One-step CPS constructor for the freer monad.

  Categorical reading. This is the “node + continuation” constructor whose catamorphism realizes the constructor algebra α : Σ T ⇒ T under a CPS encoding. Schematic type: freer : Σ β → (β → Freer Σ α) → Freer Σ α It underlies the one-layer inclusion liftFreer : Σ α → Freer Σ α.

  🔗def

  Freely.liftFreer.{u, v} {F : Type u → Type v} {α : Type u} (eff : F α) :
    ℙ F α
  Freely.liftFreer.{u, v}
    {F : Type u → Type v} {α : Type u}
    (eff : F α) : ℙ F α

  Universal arrow ι : F ⇒ ℙ F. Lift an effect request into the free monad.

  This is the canonical inclusion of F into the free monad it generates.

• handlers which simply wrap natural transformations

  The class

  🔗type class

  Freely.Handler.{u} («Σ» m : Type u → Type u) : Type (u + 1)
  Freely.Handler.{u}
    («Σ» m : Type u → Type u) : Type (u + 1)

  A natural transformation «Σ» ⟹ᶠ m (component-wise «Σ» β → m β).

  Instance Constructor

  Freely.Handler.mk.{u}

  Methods

  handle : {β : Type u} → «Σ» β → m β

  The component at α of the natural transformation θ : «Σ» ⟹ᶠ M.

  is a componentwise natural transformation «Σ» ⟹ᶠ m (parametric in β), ensuring the naturality square. Folding by ↓ᵀ handle gives the unique ℙ «Σ» ⟹ᶠ m.

  🔗def

  Freely.cataFreer.{u, v, w} {F : Type u → Type v} {m : Type u → Type w}
    [Monad m] (algebra : {β : Type u} → F β → m β) {α : Type u} :
    ℙ F α → m α
  Freely.cataFreer.{u, v, w}
    {F : Type u → Type v}
    {m : Type u → Type w} [Monad m]
    (algebra : {β : Type u} → F β → m β)
    {α : Type u} : ℙ F α → m α

  Catamorphism / interpreter for ℙ F.

  Given a handler (algebra) algebra : ∀ {β : Type u}, F β → m β for some monad m, cataFreer algebra : ℙ F ⇒ m is the unique monad morphism that:

  sends pure x to pure x, and

  runs one F-node at a time via algebra, then continues with the residual program.

  Termination: for a finite Freer value and a total/non-diverging handler algebra, this fold terminates after one call to algebra per freer node.

  🔗def

  Freely.interpret.{u} {α : Type u} {«Σ» m : Type u → Type u} [Monad m]
    [«Σ» ⟹ᶠ m] : ℙ «Σ» α → m α
  Freely.interpret.{u} {α : Type u}
    {«Σ» m : Type u → Type u} [Monad m]
    [«Σ» ⟹ᶠ m] : ℙ «Σ» α → m α

  Interpret a ℙ «Σ» α program into an m α using a Handler «Σ» m typeclass instance.

  🔗def

  Freely.interpret'.{u} {«Σ» m : Type u → Type u} [Monad m] (θ : «Σ» ⟹ᶠ m)
    {α : Type u} : ℙ «Σ» α → m α
  Freely.interpret'.{u}
    {«Σ» m : Type u → Type u} [Monad m]
    (θ : «Σ» ⟹ᶠ m) {α : Type u} :
    ℙ «Σ» α → m α

  Interpret a ℙ «Σ» α program into m α, using a handler θ : «Σ» ⟹ᶠ m argument. This is akin to interpret but accepts the handler as an argument instead of doing an instance search.

  interpret' θ is the free extension of a handler θ : «Σ» ⟹ᶠ m: the unique monad morphism ℙ «Σ» ⇒ m such that interpret' θ ∘ ↑ᵀ = θ

  ⟦θ⟧ is natural in α and preserves the monad structure:

  • unit: ⟦θ⟧ (ηᵀ a) = pure a (your interpret'_pure)

  • multiplication/bind: ⟦θ⟧ (x >>= k) = ⟦θ⟧ x >>= (fun a => ⟦θ⟧ (k a))

• a co-product of signatures

  We implement «Σ₁» ⊕ᶠ «Σ₂» as SumF, in a pointwise functorial manner.

  🔗inductive type

  Freely.SumF.{u} (F G : Type u → Type u) (α : Type u) : Type u
  Freely.SumF.{u} (F G : Type u → Type u)
    (α : Type u) : Type u

  SumF, written F ⊕ᶠ G, is the binary coproduct of endofunctors on Type u. This is meant to denote a sum of signaturesk the additive combinator on vocabularies of asks.

  Constructors

  inl.{u} {F G : Type u → Type u} {α : Type u} :
    F α → (F ⊕ᶠ G) α

  Left injection of signatures: inl : Σ₁ ⟹ᶠ (Σ₁ ⊕ᶠ Σ₂). Natural in the index; categorically the coproduct inclusion.

  inr.{u} {F G : Type u → Type u} {α : Type u} :
    G α → (F ⊕ᶠ G) α

  Right injection of signatures: inr : Σ₂ ⟹ᶠ (Σ₁ ⊕ᶠ Σ₂). Natural in the index; categorically the coproduct inclusion.

  Handlers for such sums are simply co-pairings of handlers (θ₁, θ₂) : «Σ₁» ⇒ M × «Σ₂» ⇒ M giving θ : «Σ₁» ⊕ᶠ «Σ₂» ⇒ M, as one would expect.

  🔗def

  Freely.copair.{u} {F G m : Type u → Type u} (θF : F ⟹ᶠ m)
    (θG : G ⟹ᶠ m) : (F ⊕ᶠ G) ⟹ᶠ m
  Freely.copair.{u}
    {F G m : Type u → Type u} (θF : F ⟹ᶠ m)
    (θG : G ⟹ᶠ m) : (F ⊕ᶠ G) ⟹ᶠ m

  Copairing of handlers. Given θ₁ : «Σ₁» ⟹ᶠ M and θ₂ : «Σ₂» ⟹ᶠ M, produce [θ₁, θ₂] : («Σ₁» ⊕ᶠ «Σ₂») ⟹ᶠ M with the defining equations [θ₁, θ₂] ∘ inl = θ₁ and [θ₁, θ₂] ∘ inr = θ₂.

  🔗def

  Freely.handleSum.{u} {F G m : Type u → Type u} (θF : F ⟹ᶠ m)
    (θG : G ⟹ᶠ m) : (F ⊕ᶠ G) ⟹ᶠ m
  Freely.handleSum.{u}
    {F G m : Type u → Type u} (θF : F ⟹ᶠ m)
    (θG : G ⟹ᶠ m) : (F ⊕ᶠ G) ⟹ᶠ m

  Handler for a sum of signatures, implemented as copairing of component handlers.

  🔗type class

  Freely.Handles («Σ» m : Type → Type) : Type 1
  Freely.Handles («Σ» m : Type → Type) :
    Type 1

  For many summands we can nest handleSum, but the scalable pattern is a typeclass that supplies a handler for each signature and lifts along sums.

  Instance Constructor

  Freely.Handles.mk

  Methods

  θ : «Σ» ⟹ᶠ m

  θ : «Σ» ⟹ᶠ M (a natural transformation from the signature to the semantic monad).

  🔗def

  Freely.handlesSum {F G m : Type → Type} [Handles F m] [Handles G m] :
    Handles (F ⊕ᶠ G) m
  Freely.handlesSum {F G m : Type → Type}
    [Handles F m] [Handles G m] :
    Handles (F ⊕ᶠ G) m

  Recursive instance for sums (co-pairing).

  These constructions exhibit the categorical universal property of initiality in the category of endofunctors over 𝒞, i.e. End(𝒞). (Note: This is the data types à la carte pattern.)

• membership

  Our

  Member F R  ⊣  inj : F ⇒ R
  

  realises the unique injection of a summand F into a right-associated sum R = G₁ ⊕ … ⊕ Gₖ. This is the functor-level analogue of the Haskell “open union row” (Member eff r) used by libraries such as extensible-effects and freer-simple.

  🔗type class

  Freely.Member.{u} (F R : Type u → Type u) : Type (u + 1)
  Freely.Member.{u}
    (F R : Type u → Type u) : Type (u + 1)

  Member F R says that F can be embedded as a summand of R.

  Instance Constructor

  Freely.Member.mk.{u}

  Methods

  inj : {α : Type u} → F α → R α

  Canonical injection of a summand into a right-associated signature sum.

  Given [Member F R], the natural transformation inj : F ⟹ᶠ R is the unique functorial inclusion determined by the right-spine decomposition of R. Operationally, sendᵀ := (↑ᵀ) ∘ inj : F ⟹ᶠ ℙ R.

• smart constructors

  Our deriveSend! («Σ») F₁ … Fₖ generates façade functions

  «c» : … → ℙ «Σ» _
  

  by composing Member.inj with ↑ᵀ. (In the Haskell ecosystem this role is often covered by Template Haskell splices such as freer-simple’s makeEffect or polysemy’s makeSem that generate send-style functions from GADT effect signatures.)

You may think of «freely» as having in mind two parallel rigs, which it attempts to reify (note: free applicative, tensors, etc. are planned, but have not yet been implemented):

• a rig on signatures: (⊕ᶠ, ⊗ᶠ; 0ᶠ, 𝟙ᶠ) (syntax)

• a rig on handlers: (⊕ᵃ, ⊗ᵃ; zeroHandler, oneHandler) (semantics)

with the idea that there should be some reasonable assumptions / cases where these rigs are preserved under interpretation / catamorphism.

6.1. Ambient setting

Let 𝒞 be a cartesian closed category (CCC) with finite products and finite coproducts. When thinking operationally about Lean, we'll let 𝒞 ≅ Type u.

Formally (in logic) a signature Σ essentially consists of

• a set of sorts or types

• a set of relation symbols

• a set of function symbols along with functions defining the arity of the above symbols.

The concept of a signature Σ allows us to formally describe the syntactic presentation of any fragment of (first order) logical language (inter alia).

So if we have a domain specific language (DSL) in mind, we can speak of the signature Σ of that DSL by formally defining the sorts / types, relations, and function symbols permitted in valid expressions written in that DSL.

Mathematically, a finitary signature Σ determines a polynomial functor: F_\Sigma(X)=\sum_{o\in O} X^{A_o}. This expresses that a signature is a sum over operations o∈O of exponentials X^(Aₒ) of some (finite) arity Aₒ, in a way that is parametric in X.

In «freely», we simply name that functor as «Σ» : Type u → Type u. So for the purposes of this manual, you can read F_\Sigma as equivalent to «Σ». Signatures are implemented in a CPS‑polynomial style, so that operation nodes carry their continuation. (This is an intentional design choice - one that we think is desirable because it will end up making distributivity / strength coherence automatic for folds / catamorphisms.)

6.2. The free monad on a signature

In what follows, we define a carrier functor T := ℙ «Σ» in order to name the functor part of ℙ «Σ» as T, so that e.g. we can write maps in standard mathematical form like α : «Σ» T ⇒ T.

Given «Σ», there exists a free monad on «Σ». Namely, we define ℙ «Σ» = (T, η, μ, ι), where:

• T : 𝒞 → 𝒞 is the underlying (carrier) functor of the monad.

• η : Id ⇒ T is the unit operation

• μ : T ∘ T ⇒ T is the multiplication operation, and

• ι : «Σ» ⇒ T is the universal inclusion operation

This monad is initial among monads equipped with such an ι.

Given «Σ», the free monad ℙ «Σ» = (T ,\eta, \mu, \iota) consists of

• a carrier functor ( T : \mathcal C \to \mathcal C ),

• unit ( \eta : \mathrm{Id} \Rightarrow T ),

• multiplication ( \mu : T \circ T \Rightarrow T ),

• and a universal inclusion of generators ( \iota : «Σ» \Rightarrow T ).

Intuitively, T X can be regarded as the type / object of «Σ»-terms with variables in X.

The free monad also carries its canonical one‑step constructor algebra \alpha : \Sigma T \Rightarrow T defined by \alpha = \mu \circ \iota = \mathrm{join} \circ \mathrm{liftFreer}.

In code, \alpha is not stored, but it is definable from liftFreer and join.

The catamorphism/fold is cataFreer:

Freely.cataFreer.{u, v, w} {F : Type u → Type v} {m : Type u → Type w}
  [Monad m] (algebra : {β : Type u} → F β → m β) {α : Type u} :
  ℙ F α → m α
Freely.cataFreer.{u, v, w}
  {F : Type u → Type v}
  {m : Type u → Type w} [Monad m]
  (algebra : {β : Type u} → F β → m β)
  {α : Type u} : ℙ F α → m α

6.3. Target semantics: (M, θ)

A target monad with handler is a pair (M, θ) where

• M : 𝒞 → 𝒞 is a monad (the semantic/target monad), and

• θ : «Σ» M ⇒ M is a handler (a natural transformation giving one-step «Σ»-semantics in M).

• Handler «Σ» M with handle : «Σ» α → M α (also written «Σ» ⟹ᶠ M).

Equivalent categorical views:

• As an object of Mnd^(«Σ» ): an object is exactly (M, θ); morphisms are monad morphisms preserving θ.

• Via distributive law/strength: a law «Σ» M ⇒ M «Σ» lifts «Σ» to Kleisli/Eilenberg-Moore; then θ is a «Σ»-algebra internal to M, and the interpreter defined below is the initial morphism from the free algebra/monad

6.4. Interpreter, and the universal commuting law

Given (M, θ), there exists an interpreter

⟦-⟧_θ : T ⇒ M

which is the unique monad morphism satisfying the commuting law

⟦-⟧_θ ∘ α = θ ∘ «Σ»(⟦-⟧_θ)

Freely.interpret.{u} {α : Type u} {«Σ» m : Type u → Type u} [Monad m]
  [«Σ» ⟹ᶠ m] : ℙ «Σ» α → m α
Freely.interpret.{u} {α : Type u}
  {«Σ» m : Type u → Type u} [Monad m]
  [«Σ» ⟹ᶠ m] : ℙ «Σ» α → m α

Freely.interpret'.{u} {«Σ» m : Type u → Type u} [Monad m] (θ : «Σ» ⟹ᶠ m)
  {α : Type u} : ℙ «Σ» α → m α
Freely.interpret'.{u}
  {«Σ» m : Type u → Type u} [Monad m]
  (θ : «Σ» ⟹ᶠ m) {α : Type u} :
  ℙ «Σ» α → m α

• Laws

  α = join ∘ liftFreer

  interpret θ ∘ liftFreer = θ.handle
  interpret θ preserves pure / bind
  

  🔗theorem

  Freely.interpret'_pure.{u} {«Σ» m : Type u → Type u} [Monad m]
    (θ : «Σ» ⟹ᶠ m) {α : Type u} (a : α) : ⟦θ⟧ (Freer.pure a) = pure a
  Freely.interpret'_pure.{u}
    {«Σ» m : Type u → Type u} [Monad m]
    (θ : «Σ» ⟹ᶠ m) {α : Type u} (a : α) :
    ⟦θ⟧ (Freer.pure a) = pure a

  ⟦θ⟧ preserves pure.

  🔗theorem

  Freely.interpret'_lift.{u} {«Σ» m : Type u → Type u} [Monad m]
    [LawfulMonad m] (θ : «Σ» ⟹ᶠ m) {α : Type u} (s : «Σ» α) :
    ⟦θ⟧ (liftFreer s) = Handler.handle s
  Freely.interpret'_lift.{u}
    {«Σ» m : Type u → Type u} [Monad m]
    [LawfulMonad m] (θ : «Σ» ⟹ᶠ m)
    {α : Type u} (s : «Σ» α) :
    ⟦θ⟧ (liftFreer s) = Handler.handle s

  ⟦θ⟧ on a single freer-node (via liftFreer).

«Σ» T --α-------> T
  |               |
  | «Σ»(⟦-⟧_θ)    | ⟦-⟧_θ
  v               v
«Σ» M --θ-------> M

6.5. Category of «Σ»-interpreters and initiality

Define Mnd^(«Σ»), the category whose:

• Objects are pairs (M, θ) with θ : «Σ» M ⇒ M.

• Morphisms are monad morphisms φ : M ⇒ N preserving handlers:

  φ ∘ θ_M = θ_N ∘ «Σ»(φ) .
  

(T, α) is an object of Mnd^(«Σ»), initial among such objects.

6.6. Modularity: sums, membership, copairing

We support:

• handler zero/plus 0, ⊕ᵃ ↔ zeroHandler, ⊕ᵃ

• (planned - not yet implemented) signature tensor ⊗ᶠ via Day ↔ Tensor

• (planned - not yet implemented) handler product ⊗ᵃ via Applicative/Day-lift)

6.7. Minimal hypotheses (what is strictly required)

1. 𝒞 has finite products/coproducts (to form polynomial «Σ»).

2. The free monad ℙ «Σ» exists.

3. M admits of strength/distributive-law coherence so that θ : «Σ» M ⇒ M is well-typed and natural.

In code, we achieve (1) and (2) via ℙ «Σ» + MonadLaws. (3) is ensured by CPS signatures and cataFreer, with naturality/monad-morphism properties tested in Naturality.lean and Interpretation.lean.

Our signatures are implemented in a CPS-polynomial style (operation nodes carry continuations), so a handler already returns an M-action for the continuation. In this presentation, the coherence typically packaged as a distributive law is inherent in the typing of the fold. The library still exposes and tests naturality and the interpreter laws, and the initiality statement remains exactly as above.

This earns us:

1. Canonical meaning: fixing θ yields a unique ⟦-⟧_θ.

2. Functorial transport: if φ : M ⇒ N preserves handlers, then φ ∘ ⟦-⟧_θ = ⟦-⟧_{θ’}.

3. Compositionality by construction: evaluation is an algebra homomorphism; substitution is μ.

4. Modularity and extension: extending «Σ» via sums extends programs and handlers modularly.

5. Algebraic location: sums/products live in the syntax shape («Σ»), not in ad-hoc code.

6.8. Two categorical viewpoints: Kleisli and Eilenberg–Moore