Haskell accepts the definition of these two types

data PowerPower = PP ((PowerPower -> Bool) -> Bool)
data Power = P (Power -> Bool)

Type PowerPower is used extensively in the Reynolds' paper that refutes set semantics for System F. It is represented by this type of System F

PowerPower = forall A, (((A -> Bool) -> Bool) -> A) -> A
PP = \ z A f -> f (\ u -> z (\ x -> u (x A f)))

Reynolds' refutation ends by arguing that PowerPower is isomorphic to the powerset of the powerset of PowerPower, which contradicts Cantor's theorem about cardinals. The two nested powersets correspond to the two arrows towards Bool in the definition of PowerPower.

The refutation would be greatly simplified if we could use type Power instead of PowerPower. One powerset is enough to apply Cantor's theorem. The question then becomes: can we represent type Power in System F? It may be difficult, because Power's underlying type functor, \X -> (X -> Bool), is contravariant instead of covariant. Since Haskell accepts the definition of Power, we might use its representation in Haskell's memory model to derive a type in System F.

CodePudding user response：

Let B be any type (Bool, in your case), and assume an isomorphism, with its inverse

iso :: P -> (P -> B)
osi :: (P -> B) -> P

Now, take any f :: B->B. We prove that f has a fixed point. (This is an instance of Lawvere's fixed point theorem.)

Define

 g :: P -> B
 g p = f (iso p p)

We then have (I'll leave to you to check that the following is well-typed):

g (osi g) = f (iso (osi g) (osi g)) = f (g (osi g))

Hence, g (osi g) is a fixed point of f.

In Haskell, this is not a big deal. After all we have fix that can always produce a (least) fixed point of any endo f :: B->B.

However, most typed lambda calculi like the simply-typed lambda calculus, System F, the calculus of (inductive) constructions, etc. are normalizing. There, we do not have arbitrary recursion, and the evaluation of each (closed) term always terminates, reducing to its normal form, which has a canonical shape.

If we take B = Bool, and g = not, we have that there is a boolean b equal to not b. This can not happen in such calculi (suitably extended with Bool if not present) since b would then normalize to either True or False, but neither is a fixed point.

Again, in Haskell we can take the non terminating b = fix not, but we do not have such option in terminating calculi.