7
$\begingroup$

Question originally asked in proofassistants.stackexchange

Just like the title says, is it true (in some sensible model)? And if so, how to prove it? Something tells me it should be true and higher-order version of parametricity/theorems-for-free is needed to show this.

A concrete instance of the problem:

∀s. ∀a. (State s a ≅ (∀m. Monad m → StateT s m a))

In general the problem can be stated informally like so:

∀a. (MonadT Id a ≅ (∀ m. Monad m → MonadT m a))

where MonadT is a "schema" standing for arbitrary monad transformer.

The background type theory can be assumed to be system F or some dependent type theory consistent with parametricity. Depending on the theory used, the statement can be either internal or external.

$\endgroup$
2

1 Answer 1

3
$\begingroup$

The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that "a monad transformer is equivalent to its base monad". A monad transformer probably carries more information than its base monad, because there is no known way of mechanically converting a given base monad into its monad transformer.

By definition, a transformer's base monad can be obtained by applying the transformer to Id. This is denoted by F Id. You claim that F Id ≅ ∀ (m: Monad). F m. This seems to be correct.

Also you are correct that a proof will involve parametricity at the level of monads.

A possible proof could go like this. Consider the category of monads: objects are monads and arrows are monad morphisms. In that category, a monad transformer is an endofunctor. (This is true for almost all monad transformers, except Continuation and Codensity and some other variants of those monads. See https://stackoverflow.com/questions/63882053/whats-a-functor-on-the-category-of-monads?rq=3 and see also my answers in Explaining monad transformers in categorical terms and in https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io .)

Then we want to prove the following property:

 F Id ≅ ∀ (m: Monad). F m

where ∀ (m: Monad) goes over all monads.

The first step is to prove that the identity monad Id is an initial object in the category of monads. For any given monad M, there is only one monad morphism between Id and M (that morphism is given by the monad M's unit method, unit: ∀ a. Id a → M a). I omit the proof of this property.

The second step is to use the Yoneda lemma (still in the category of monads). The Yoneda lemma says: For any Set-valued functor G (that is, a functor from the category of monads to the category of sets), the Yoneda lemma says:

 G X ≅ Nat(Hom(X, _), G)  ,

where Nat(K, L) is the set of natural transformations between functors K and L; Hom(X, _) is the Set-valued functor that maps a given monad M into the set of morphisms (in the category of monads) between the monads X and M.

Now we want to apply the Yoneda lemma to our situation where G = F is our monad transformer endofunctor. But then there is a technical difficulty: we cannot use the Yoneda lemma because G is not a set-valued functor (it's a monad-valued functor). We need to map monads into sets in some way. This is not straightforward; for instance, it is not clear how to choose a set that would correspond to the List monad or to the Maybe monad. It is easier to introduce a type parameter t and talk about the type List t or Maybe t. For any given type t there is a well-defined set of all values of type List t. So, we can temporarily choose some arbitrary type t and define a set-valued functor G that maps a monad m into the set of all values of type (F m) t. For this functor G, the Yoneda lemma shown above will hold.

The third step is to choose X = Id in the Yoneda lemma and find:

 G Id ≅ Nat(Hom(Id, _), G)

The fourth step is to see why it makes sense to write the right-hand side as ∀ (m: Monad). G m in the notation of a programming language. In fact, since we are working in a purely functional language where parametricity holds, any value of type ∀ (m: Monad). G m must be implemented in a way that is fully parametric in the monad m: it may use only the monad m's methods but no other knowledge about m.

The set Hom(Id, M) is a single-element set because Id is an initial object and there is only one monad morphism between Id and M. So, the functor Hom(Id, _) is a constant functor that maps any object into a single-element set.

What is the set of natural transformations between that constant functor and G? A component at m of such a transformation is a morphism of type Hom(Id, m) => G m. Here => means the arrow in the category Set.

But Hom(Id, m) is a single-element set. So, a morphism Hom(Id, m) => G m is the same as just choosing one element in the set G m.

We find that a natural transformation between Hom(Id, _) and G is the same as a choice, for each monad m, of an element in the set G m in a way that does not depend on the monad m other than through the monad m's methods (in other words, in a fully parametric way). An element in the set G m is the same as a value of type F m t. In a programming language, we would write that as the type ∀ (m: Monad). F m t assuming that values of that type must be fully parametric. The assumption of parametricity allows us to use the parametricity theorem and is necessary because otherwise the values of type ∀ (m: Monad). F m t would not correspond to natural transformations.

In this way we find, in a programming language notation, that:

 (F Id) t ≅ ∀ (m: Monad). F m t

This holds for all types t. So, we can rewrite this identity more concisely as:

 F Id ≅ ∀ (m: Monad). F m

There are certainly some rough edges in this sketch of a proof, but I'm not sufficiently well-versed in category theory to polish it off.

The analogy with the Yoneda lemma for ordinary types and endofunctors gives the following equivalence between types:

F 0 ≅ ∀ t. F t

because 0 is an initial object in the category of types.

$\endgroup$
19
  • $\begingroup$ How do I get around the rought edge F X ≅ ∀ m. (X → m) => F m? The left-hand side is a set. How do I read the right-hand side as a set? I expected F X ≅ Nat(Hom(X, _), F) which sort of looks like what you wrote, but I am not sure. $\endgroup$ Sep 6, 2023 at 13:41
  • $\begingroup$ I haven't heard about the category of monads. And I can't find a reference on the internet. Could you provide one? $\endgroup$
    – Russoul
    Sep 6, 2023 at 20:52
  • $\begingroup$ @AndrejBauer You may be right about F X ≅ Nat(Hom(X, _), F) but I wish I had a more immediate grasp of the Yoneda lemma in a general category. In principle we just need to write the Yoneda lemma in the category of monads and put F into the right place and then set X = Id. Isn't Nat(Hom(X, _), F) a set? $\endgroup$
    – winitzki
    Sep 8, 2023 at 18:33
  • $\begingroup$ @Russoul There isn't a reference that I have in mind. We just consider a category whose objects are various monads in the usual sense (Maybe, List, State s, Identity etc.) and whose morphisms are monad morphisms. $\endgroup$
    – winitzki
    Sep 8, 2023 at 18:35
  • $\begingroup$ @winitzki: The basic question I have is, in what sense is ∀ m. (Id → m) => F m a set? What does it mean to quantify with and get a set out? $\endgroup$ Sep 8, 2023 at 20:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.