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 (C f a = r -> (a, r)).
f a = (w, a) (the Writer monad), for which C f a = ((a -> w) -> a, (a -> w) -> w)
f a = a -> s (a contravariant functor) and then C f a = (a -> s) -> s (the continuation monad).
f a = a -> a (neither covariant nor contravariant) and the C f a = List a
In the first four of those cases, the type equivalence can be derived from the Yoneda identity: forall r. (a -> r) -> F r = F a when F is a covariant functor. The last case is derived via the Church encoding of the inductive type List.
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?
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.