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

Question

The next question relates to Recursive algebraic data types through polymorphism in Haskell .

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

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

with an "ordinary" natural number n is realized as

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

with n iterations f .

Similarly, a Boolean type can be entered as

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

while the expected values ​​of "true" and "false" are implemented as

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

Q: All members of the Bool or Nat or any other potentially recursive type of algebraic data (encoded in this way) of the above form, up to some rules for reducing working semantics?

Example 1 (natural numbers): Any member of type forall t. t -> (t -> t) -> t forall t. t -> (t -> t) -> t 'is in a sense equivalent to the term of the form \ x0 f -> f (f ( ... (f x0) ... )) ?

Example 2 (Booleans): Any member of type forall t. t -> t -> t forall t. t -> t -> t "in a sense" is equivalent to either \ tf -> t or \ tf -> f ?

Addition (internal version) . If the language in question is even able to express propositional equality, this metamathematical question can be internalized as follows, and I would be very happy if someone came up with a solution for this:

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

 type ModStr mt = mt -> t UnivMod m = UnivMod { univProp :: forall t. (ModStr mt) -> t } classifyingMap :: forall m. forall t. (ModStr mt) -> (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: If the language is capable of expressing this: is the equality type dec_enc = id populated?

Answer 1

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

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

See how these normal shapes look. (We will use the generation lemma for λ2; see Book Barendregt for formal details.)

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

For case N must be at least one λ, because initially we do not have any variable in the input context that would replace y . So, N = λx.U and x:α |- U:α→α .

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

But V cannot be λ.. , because then it will have the type of function τ→σ . So, V should only be of the form z P1 ... Pk , but since we do not have any kind of function type variable in the context, K must be 0, and therefore V can only be x or y .

Thus, in the normal form of type ∀α.α→α→α there are only two members: λxy.x and λxy.y , and all other members of this type are β-equal to one of them.

---

Using similar reasoning, we can prove that all the inhabitants of ∀α.α→(α→α)→α β-equal to the church digit. (And I think that for the type ∀α.(α→α)→α→α situation is a little worse, we also need p-equality, since λf.f and λfx.fx correspond to 1 , but not β-equal, just βη-equal.)

Answer 2

If we ignore the bottom and unsafe things, then the only thing you can do universally with the functions a -> a is to compile them. However, this does not completely stop us with finite expressions f (f ( ... (f x0) ... )) : we also have infinite composition infty xf = f $ infty xf .

Similarly, the only non-recursive boolean values ​​are really \t _ -> t and \_ f -> f , but you can also tie the nodes here, for example

 blarg tf = blarg (blarg tf) (blarg ft)