Are Bad churches inhabited?

Question

In type theory, some inductively defined data types allow you to prove absurdity. For example

type Bad a = MkBad (Bad a -> a)
extract : Bad a -> a
extract val@(MkBad f) = f val
absurd : a
absurd = extract (MkBad extract)

Now, when you church encode this datatype it leads to

badChurch : Bad a -> (forall X. ((X -> a) -> X) -> X)
badChurch _ = ?

Now, it seems to me that this function type is actually uninhabited and my intuition says that it could be proven using Theorems for free but alas I can't find a way to actually do that.

The deeper question is this: Would showing the existance of a church encoding be enough to prove consistency of a datatype? And contrary; Are there datatypes whose church encoding is uninhabited with which you can not prove absurdity?

---

Pretend you want to check if you allow a datatype in your language. Would it be enough to check if the type's church encoding exists to safely allow the type in your language?

Answer 1

No, it is not sufficient to check that the 'Church encoding' is uninhabited.

Consider the type:

$$\mathsf{data} \;U = L\ (U → U)\; |\; A\ U\ U$$

The idea is that $U$ is the type of untyped lambda terms. If you allow this as a data type into your language, it causes problems. At the very least, you can write loops in $U$ if you are allowed to inspect its values by case analysis.

δ : U -> U
δ (L f) = f (L f)
δ x = x

ω : U
ω = δ (L δ)

-- ω ==> δ (L δ) ==> δ (L δ) ==> ...

If you are also allowed to do recursion on the presumption that $U$ is well-founded, these loops leak into every other type.

However, the 'Church encoding' of $U$ is not uninhabited:

$$U' = ∀ R. ((R → R) → R) → (R → R → R) → R$$

In fact, this is a somewhat well-known representation of untyped lambda terms in a sort of higher-order abstract syntax. You can write down (an encoding of) any untyped lambda term you want:

$$id : U' = λ L. λA. L (λ x. x)$$ $$comp : U' = λ L. λA. L (λ g. L (λ f. L (λ x. A\ g\ (A\ f\ x))))$$ $$δ' : U' = λ L. λ A. L (λ x. A\ x \ x)$$ $$ω' : U' = λ L. λ A. A\ (L (λ x. A\ x\ x))\ (L (λ x. A\ x\ x))$$

So, this encoding is certainly inhabited. But, the reason I was using scare quotes earlier is that is clearly still not what we expect the original data type to mean, so it's rather unclear whether this should be considered the Church encoding of that data type. For instance, you will be unable to exhibit the equivalence:

$$U' \cong (U' → U') + U' × U'$$

which is expected of the data definition. Also, $U'$ is arguably a more faithful representation of the syntax of untyped lambda terms, because all we can do is abstract and apply, as those are the only things we know about the abstract $R$ type. $U$, at least presuming the usual semantics of data, allows us to write, "exotic terms," which is what δ and ω actually are (note that they're not the same as $δ'$ and $ω'$). And this makes sense, because these exotic terms are what allow us to write loops using the data type, whereas $U'$ is a perfectly acceptable System F type, and System F is strongly normalizing.

So, clearly, some more thorough check is necessary than mere habitation. You must check that the 'encoding' actually models the properties you're going to allow your data type to have.

Answer 2

If we allow types like Bad, then any type is inhabited by absurd, including the type you mention.

Otherwise, if we do not want to use the Bad a argument, we can note that $((X \to A)\to X)\to X$ is Peirce's Law, which is unprovable in intuitionistic logic, hence not inhabited in virtually any (axiom-free) type systems.

Note that we can not even disprove the above law, since it is a theorem of propositional classical logic, so most type systems are consistent with it.

It is a paragon example of an undecidable proposition in intuitionistic systems.