The codensity monad on a type constructor f is defined by:

 newtype C f a = C { unC ∷ forall r. (a → f r) → f r }

It is well known that C f is a monad for any type constructor f (not necessarily covariant). The codensity monad is useful in several ways but it is a complicated type that contains a higher-order function under a universal type quantifier.

My question is, for what f can one show that C f is equivalent to a simpler monad that is defined without type quantifiers?

Some examples where a simplification is possible:

• f a = a (the identity functor), for which C f a = a.

• f a = r -> a (the Reader monad), for which C f is the State monad.

• f a = (w, a) (the Writer monad), for which C f a = ((a -> w) -> a, (a -> w) -> w)

In all those cases, the type equivalence follows from the Yoneda identity: forall r. (a -> r) -> F r = F a when F is a covariant functor.

I looked at some other examples and found that in most cases C f does not seem to be equivalent to anything simpler.

Even if we just take f a = Maybe a the resulting type does not seem to be equivalent to a simpler type expression:

 newtype CMaybe a = CMaybe { unCMaybe ∷ forall r. (a → Maybe r) → Maybe r }

The Yoneda identity cannot be used here. My best guess (I have no proof so far) is that CMaybe a = (a -> Bool) -> Bool with some additional laws imposed on the functions of that type. Imposing equations on values can be adequately expressed only within a dependently-typed language.

Can one simplify the codensity monad on Maybe?

Are there other examples of type constructors f where C f can be simplified to a type without type quantifiers?

CodePudding user response：

As mentioned in the comments, a function C Maybe a returns a bit more information than a boolean because the r it returns identifies a single input in the callback, so f k chooses an x such that k x is Just.

Simplifying the callback type from a -> Maybe r to a -> Bool, we obtain the following dependent function type, written in Agda and in Coq respectively for reference:

-- Agda

(∀ {r} → (a → Maybe r) → Maybe r)
≡
((k : a → Bool) → Maybe (∃[ x ] k x ≡ true))

(* Coq *)

(forall r, (a -> option r) -> option r)
=
(forall (k : a -> bool), option { x : a | k x = true })

Proof of equivalence in Agda: https://gist.github.com/Lysxia/79846cce777f0394a6f69d84576a325b

This proves the equivalence of ∀ {r} → (a → Maybe r) → Maybe r and a type without a quantifier: ((f : a → Bool) → Maybe (∃[ x ] f x ≡ true)), which is equivalent to q:: (a → Bool) → Maybe a with the restriction that q(p) equals Just x only if p(x) = true.

Note that if a is finite, then C Maybe a is also finite. One approach to the problem then is to compute the corresponding cardinality function.

• You can reinterpret the expression of the cardinality as a type, giving a solution to your problem for types of the form Finite a -> C f a.

• You can look it up on the online encyclopedia of integer sequences, to find alternative combinatorial interpretations. Sadly, the relevant sequence doesn't have much information.

  Product_{j=1..n} j^C(n-1,j-1)
  
  -- https://oeis.org/A064320
  

• If you could find a simpler type for C f a, with only sums, products (not indexed by the cardinality of a), and exponentials, this may correspond to a non-trivial combinatorial identity. Conversely, difficulty in finding such a combinatorial identity provides compelling evidence for the non-existence of simple solutions. It also gives a quick way to test a candidate simplification for validity, by comparing its cardinality with the expected one.