What are the values of a polymorphically encoded recursive algebraic data type?

Question

The following question relates to Recursive algebraic data types via polymorphism in Haskell.

Recursive algebraic data types can be realized in any language with the capabilities of System F using universal parametric polymorphism. For example, the type of natural numbers can be introduced (in Haskell) as

newtype Nat = Nat { runNat :: forall t. (t -> (t -> t) -> t) }

with the 'usual' natural number n being realized as

\ x0 f -> f(f(...(f x0)...))

with n iterations of f used.

Similarly, the type of Booleans can be introduced as

newtype Bool = Bool { runBool :: forall t. t -> t -> t }

with the expected values 'true' and 'false' being realized as

true = \ t f -> t
false = \ t f -> f

Q: Are all terms of type Bool or Nat or any other potentially recursive algebraic data type (encoded in this way) of the above form, up to some reduction rules of operational semantics?

Example 1 (Natural numbers): Is any term of type forall t. t -> (t -> t) -> t 'equivalent' in some sense to a term of the form \ x0 f -> f (f ( ... (f x0) ... ))?

Example 2 (Booleans): Is any term of type forall t. t -> t -> t 'equivalent' in some sense to either \ t f -> t or \ t f -> f?

Addendum (internal version): In case the language under consideration is even capable of expressing propositional equality, this meta-mathematical question could be internalized as follows, and I would be very happy if someone would come up with a solution for it:

For any functor m we can define the universal module and some decoding-encoding function on it as follows:

type ModStr m t = m t -> t
UnivMod m = UnivMod { univProp :: forall t. (ModStr m t) -> t }

classifyingMap :: forall m. forall t. (ModStr m t) -> (UnivMod m -> t)
classifyingMap f = \ x -> (univProp x) f

univModStr :: (Functor m) => ModStr m (UnivMod m)
univModStr = \ f -> UnivMod $ \ g -> g (fmap (classifyingMap g) f)

dec_enc :: (Functor m) => UnivMod m -> UnivMod m
dec_enc x = (univProp x) univModStr

Q: In case the language is capable of expressing this: is the equality type dec_enc = id inhabited?

Answer 1

In System F (AKA λ2), all inhabitants of ∀α.α→α→α are indeed λ-equal to K or K*.

First, if M : ∀α.α→α→α then it has normal form N (since System F is normalizing) and by subject reduction theorem (see Barendregt: Lambda calculi with types) also N : ∀α.α→α→α.

Let's examine how these normal forms can look like. (We'll be using Generation lemma for λ2, see the Barendregt's book for formal details.)

If N is a normal form, that N (or any its subexpression) must be in head normal form, that is an expression of the form λx1 ... xn. y P1 ... Pk, where n and/or k can be also 0.

For the case of N, there must be at least one λ, because initially we don't have any variable bound in the typing context that would take the place of y. So N = λx.U and x:α |- U:α→α.

Now again there must be at least one λ in the case of U, because if U were just y P1 ... Pk then y would have a function type (even for k=0 we'd need y:α→α), but we have just x:α in the context. So N = λxy.V and x:α, y:α |- V:α.

But V can't be λ.., because then it'd have function type τ→σ. So V must be just of the form z P1 ... Pk, but since we don't have any variable of function type in the context, k must be 0 and therefore V can be only x or y.

So there are only two terms in normal form of type ∀α.α→α→α: λxy.x and λxy.y and all other terms of this type are β-equal to one of these.

---

Using similar reasoning we can prove that all inhabitants of ∀α.α→(α→α)→α are β-equal to a Church numeral. (And I think that for type ∀α.(α→α)→α→α the situation is slightly worse; we also need η-equality, as λf.f and λfx.fx correspond to 1, but aren't β-equal, just βη-equal.)

Answer 2

If we disregard bottoms and unsafe stuff, then the only thing you can do universally with functions a -> a is compose them. However, that doesn't quite stop us at finite f (f ( ... (f x0) ... )) expressions: we also have the infinite composition infty x f = f $ infty x f.

Similarly, the only non-recursive boolean values are indeed \t _ -> t and \_ f -> f, but you can also tie knots here, like

blarg t f = blarg (blarg t f) (blarg f t)