Can one simplify the Codensity monad on Maybe?

Question

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?

Gumboil

My guess is that CMaybe is a bit more complicated. A value for CMaybe Int could take f as input, compute map f [0..99], and observe which results are Nothing or Just x_i. Depending on these "100 bits" of information, we can either return Nothing or Just x_j which is more or less like returning a number in [-1..99] (Nothing or the index j). So... maybe it's closer to (a -> Bool) -> Nat? I can't really say. – Adriannaadrianne

I think the problem is that Maybe is a sum type Maybe a = 1 + a, and sum types are defined by mapping out. Instead here you have a mapping into a sum. You essentially have (1+r)^(1+r)^a which, even as a high-school algebraic expression, doesn't have a compact form. – Sawmill

Answer 1

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.

Vesicle

Could you write more explicitly here the types that you have proved to be equivalent? – Gumboil

Could you prove formally that forall r. (a -> Maybe r) -> Maybe r is equivalent to (a -> Bool) -> Maybe a with additional restrictions? – Gumboil

I gave a link to an Agda proof. – Vesicle