Quantified types are undecidably powerful
Consider the functor M(p) = ∀a. (p → 1 + a) → 1 + a where p is a type parameter. I've been trying to simplify and analyze this deceptively simple expression, with not much success so far.

[ Notation: I am working in a subcategory of sets where objects are types in a functional programming language, and 0 is the initial object, 1 is the terminal object, a × b is the product and a + b is the co-product (or disjunction) of types a and b, whereas a → b is the function from type a to type b, understood as a function type (exponential object). The symbol → binds less tightly than +, which binds less tightly than ×. So, p → 1 + a means p → (1 + a). Finally, types 1 + 1 + 1 + ... + 1 are "natural number types" and are denoted simply as 2, 3, ... ]

The motivation for studying the functor M comes from the so-called "codensity monad" (see e.g. http://comonad.com/reader/2011/free-monads-for-less/). It is known that the "codensity" construction,

M(p) = ∀a. (p → F(a)) → F(a),

gives a monad M for any functor F. However, it is hard to reason about such a type construction, so I wanted to simplify it. As simplest examples of a functor F, I took the sum (or disjunction), F(a) = 1 + a, the product F(a) = w × a, and the exponential F(a) = e → a, and then I tried to simplify the type expression M(p). I was not able to simplify M(p) for the disjunction example F(a) = 1 + a, although I could do that for the product and the exponential,

∀a. (p → w × a) → w × a = ((p → w) → w) × ((p → w) → p)

∀a. (p → e → a) → e → a = e → e × p

So the question is, why the (seemingly) simpler type constructor, F(a) = 1 + a, does not get simplified nearly as easily as the other elementary types. Am I missing any techniques for simplifying types?

So I first considered a couple of simpler types,

∀a. (p → a) → 1 + a = 1 + p using the Yoneda lemma, ∀a. (p → a) → F(a) = F(p)

∀a. (p → 1 + a) → a = 0 (i.e. a void type) because there is no way of implementing a value of type `a` given an arbitrary function of type p → 1 + a; that function may happen to return always 1 and never any values of type `a`.

∀a. (p → 1 + a) → q (which is a bifunctor in p and q) is a much more interesting story. How can we implement values of this type? We are given a function of type p → 1 + a, where `a` is an arbitrary type, and we are supposed to return a value of a fixed type q. Clearly, values of type `a` are useless for us; we need to choose in advance some values of type q among which we are going to choose a return value of type q. So, a value of type ∀a. (p → 1 + a) → q necessarily needs to contain at least one value of type q. The simplest such value is a function that always returns the same fixed value of type q. This function does not use its argument (which is a function of type p → 1 + a). Can we build a function of type ∀a. (p → 1 + a) → q that does use its argument? We can, if we have a value of type p and apply the function of type p → 1 + a to that p. The result will be either 1 or a value of type `a`. If it is a value of type`a`, we won't be able to use that value to produce a `q` because we don't know what `a` is; so we need to return a fixed value of type `q` that we would need to have already selected beforehand. However, we could return different values of type `q` based on the information we find by applying the given function f of type `p → 1 + a` to some stored values of type p, since that does give us some information - namely, whether the result f(p) is `1` or an `a`, for each stored value of `p`. This is just one bit of information per stored value of `p`; exactly the same information would be obtained from a function of type `p → 1 + 1`. Therefore, we can replace a function of type`p → 1 + a` by a function of type `p → 1 + 1` without loss of information. This observation finally enables us to simplify the type expression as follows:

∀a. (p → 1 + a) → q = ∀a. (p → 1 + 1) → q = (p → 2) → q.

Now we try to apply a similar consideration to M(p) = ∀a. (p → 1 + a) → 1 + a. In order to implement a value of this type, we need to write code that returns either `1` or a value of type `a`. The only thing this code may do is apply a given function `f` of type `p → 1 + a` to some values of `p`, which have to be chosen in advance and stored in the program. Suppose we had three stored values of type `p`, chosen in advance. Applying the function `f` to these, we obtain three values of type `1 + a`; that is, potentially up to 3 different values of type `a`, but maybe fewer. Possibly using this data, we now need to return a value of type `1 + a`. We could return a `1`, or we could return one of the obtained 3 values of type `a`; but we need to make this choice based only on the information we have, that is, on the 3 bits of information obtained by applying `f` to our 3 stored values of type `p`.

However, now we can't simply replace `f : p → 1 + a` by a function of type `p → 1 + 1` because we may need to use one of the values of type `a` returned by `f`. For instance, we could (arbitrarily) decide that we store 3 values of type `p`, apply `f` to each of them, observe 3 bits of information (the bit is equal to 0 if f(p) = 1 and otherwise 1), and compute the integer k in the range [0, 7] represented by these 3 bits. If this integer is zero, we have no choice but to return 1. If this integer is nonzero, we could (arbitrarily) decide that we select the highest nonzero bit of this integer, and if it exists, we return the value returned by f(p) for the corresponding p. This implementation gives a possible value of type ∀a. (p → 1 + a) → 1 + a. How to parameterize all these implementations? The information obtained from the function f is first translated into a string of bits (i.e. we are using a function of type `p → 2`), and we also obtain zero or more values of type `a`. We cannot directly manipulate these values of type `a`; we may only select one of them to be returned (or we may choose to return 1 instead). This decision must be made purely as a function of the string of bits, i.e. from `p → 2`. It appears that the required information is encoded in a value of type (p → 2) → 1 + p.

Is it true that ∀a. (p → 1 + a) → 1 + a = (p → 2) → 1 + p?

I don't think so. The type 1 + p does not express the constraint that we need to select a value of p such that f(p) gives a value of `a`, rather than 1.

However, I haven't figured out how to encode this condition in a type expression. It seems that the quantified type is richer and more complicated than ordinary (non-quantified) type expressions.

While trying to resolve this question, I found that, for any G(a), one can simplify

∀a. G(a) → 1 + a = ∀a. a × G(a) → a,
∀a. G(a) → e + a = ∀a. (e → a) × G(a) → a,

but this did not help me directly to simplify the type M(p).

It would be better to prove equivalence of these types formally, rather than use heuristic considerations based on code that stores some values of `p`. Perhaps another time.

There doesn't seem to be a general way of simplifying ∀a. (p → F(a)) → F(a) for an arbitrary F(a). Nothing suggests that this is possible at all. The argument for F(a) = 1 + a or F(a) = e + a depends on the details of these functors and cannot be easily generalized to, say, `F(a) = p → a + q` or something more complicated. Perhaps this has to do with the undecidability of quantified types (or of logic with quantifiers)?