Nerd sniping: free monads without the universe bump

Stream: general

[Paul Reichert]

It has come up a few times that we can construct a free monad from a functor f in Lean:

inductive FreeMonad (f : Type v → Type v) : Type v → Type (v + 1) where
| pure : ∀ {α}, α → FreeMonad f α
| lift : ∀ {α}, f α → FreeMonad f α
| bind : ∀ {α β}, FreeMonad f α → (α → FreeMonad f β) → FreeMonad f β

We can then take a suitable quotient so that FreeMonad f is indeed a lawful monad, and if f is a lawful functor, then I think that FreeMonad f is indeed the free monad we were looking for.

Unfortunately, FreeMonad f suffers a universe bump since its codomain is Type (v + 1). After I was angry at Lean about this for some time, I finally convinced myself that this bump is unavoidable for some choices of f. For example, let f α := α → Bool. If we had a free monad FreeMonad f : Type v → Type v, then we could lift elements from f (FreeMonad f α) into FreeMonad f (FreeMonad f α) and flatten this into FreeMonad f α. I think, without having a formal proof, that this mapping is injective. But the cardinality of the power set f (FreeMonad f α) = (FreeMonad f α → Bool) is strictly larger than that of FreeMonad f α, so this injection is impossible. Contradiction.

However, I can't help but ask whether we can avoid the universe bump in the following more restricted situation: Let m : Type v → Type v be any lawful monad. Can we construct the most general monad m' : Type v → Type v, without universe bump, that extends m by a new operation op : m' PUnit? By "most general", I mean that we don't assume any equations involving op except those we need to obtain a lawful monad.

More formal problem statement

Is there a monad m' : Type v → Type v together with a morphism m -> m' (i.e. a family of maps m α → m' α that preserves the monadic operations) such that for every monad morphism m -> n and a choice of opn : n Unit there is exactly one lift m' -> n that maps op : m' PUnit to opn : n PUnit?

Motivation

I have arrived at this question while working on the new iterator library. There, an iterator is represented as an element of some type α : Type u. In a simplified setting, we can iterate with repeated applications of step : α → m (Option (α x β)), where β : Type v contains the potential outputs of the iterator. I was wondering whether we can sometimes "squash" α into a lower universe if v (remember: β : Type v) is small enough. The idea is to represent the information of the iterator without reference to α, and this information could be encoded as a monad the extends m with a carefully chosen family of monadic step operations that only return the iterator's output value and keep the iterator object itself hidden in its internal state. This monad, in turn, gives rise to an interpreter of the free extension of m by the step operations, and if this free construction lives in a small universe, then we can "squash" α into this small universe.
There are lots of complications I'm leaving out here. Moreover, even if we can find a construction without universe bumps, that wouldn't mean we could actually efficiently squash α, so this question is driven by curiosity, not practical applications.

The following obvious construction almost solves the problem but it requires a universe bump:

inductive FreeMonad (m : Type v → Type v) : Type v → Type (v + 1) where
| lift : ∀ {α}, m α → FreeMonad m α
| bind : ∀ {α β}, FreeMonad m α → (α → FreeMonad m β) → FreeMonad m β
| op : FreeMonad m PUnit.{v + 1}

I feel like m being a lawful monad should help us prevent paradoxes like the one from the power set example above. However, I couldn't come up with a concrete construction. Any ideas?

[Quang Dao]

I came up against the same limitation in my own project! One answer is that the free monad of a polynomial functor PFunctor does not require a universe bump.

import Mathlib.Data.PFunctor.Univariate.Basic

universe u v

/-- The free monad on a polynomial functor.
This extends the `W`-type construction with an extra `pure` constructor. -/
inductive FreeM (P : PFunctor.{u}) : Type v → Type (max u v)
  | pure {α} (x : α) : FreeM P α
  | roll {α} (a : P.A) (r : P.B a → FreeM P α) : FreeM P α
deriving Inhabited

/-- Lift an object of the base polynomial functor into the free monad. -/
@[always_inline, inline]
def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))

/-- Bind operator on `FreeM P` operation used in the monad definition. -/
@[always_inline, inline]
protected def bind : FreeM P α → (α → FreeM P β) → FreeM P β
  | FreeM.pure x, g => g x
  | FreeM.roll x r, g => FreeM.roll x (λ u ↦ FreeM.bind (r u) g)

Lots of functors are polynomials, though I'm not sure if they apply to your use case

[Paul Reichert]

Thanks! Very interesting! Unfortunately, I fear that that construction won't help in the general case of adjoining some new operation to an arbitrary monad. I find it more and more plausible that even such a modest extension can require a universe bump... quite surprising if you ask me.

[Serhii Khoma (srghma)]

@Quang Dao interesting, are there more low-level/without-deps approach to make a coinductive types?

[Quang Dao]

Coinductives aren't supported by the Lean kernel, so I'm afraid the best way to get to them is via M-type construction / quotients of polynomial functors (QPF in mathlib)

[Serhii Khoma (srghma)]

I made free monad using church encoding (though I couldnt make Proxy using it - couldnt make the function flipComposeResponse)

Also tried to make Church-encoded Proxy (though couldnt make connectProducerConsumer too and theorems that are present in coq version)

@Quang Dao I have a question. Is it possible to use Church encoding everywhere for coinductive datatypes instead of QPF?

[Eric Wieser]

Is @Tanner Duve's #25491 relevant to this thread?

[Quang Dao]

Serhii Khoma (srghma) said:

I made free monad using church encoding (though I couldnt make Proxy using it - couldnt make the function flipComposeResponse)

Also tried to make Church-encoded Proxy (though couldnt make connectProducerConsumer too and theorems that are present in coq version)

Quang Dao I have a question. Is it possible to use Church encoding everywhere for coinductive datatypes instead of QPF?

This is really cool, and I'm out of my depth here. Perhaps others can answer