11

In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.

In "Types and Programming Languages", the following exercise appears:

Can we encode universal types in terms of existential types?

My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?

I am not even sure what I need to prove to formally show this result.

Agnishom Chattopadhyay
  • 1,971
  • 14
  • 32
  • 1
    You might want to look into skolemization: https://en.wikipedia.org/wiki/Skolem_normal_form – Juan Pablo Santos Nov 19 '18 at 16:34
  • 1
    @JuanPabloSantos I fail to see the connection – Agnishom Chattopadhyay Nov 19 '18 at 16:41
  • I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of Yoneda `T ~ (forall a. (T->a)->a)` where we can take `T = exists b. f b` and exploit the type isomorphism `(T->a) ~ (forall b. f b -> a)`, leading to the encoding above. The analogous strategy would be using co-Yoneda `T ~ (exists a. a * (a -> T))`, but here `T` is in positive (covariant) position, so choosing `T ~ (forall b. f b)` does not allow to turn `forall` into some `exists`. – chi Jan 11 '19 at 14:05
  • There is an extended Curry–Howard isomorphism (aka the Brouwer–Heyting–Kolmogorov interpretation) between intuitionistic predicate calculus and simply-typed lambda calculus.¹ In classical logic the following formulas hold. ◦ `∃xφ(x)↔¬∀x¬φ(x)`, ◦ `∃x(φ(x)→∀yφ(y))`, ◦ `∀x(φ(x)∨¬φ(x))`. In intuitionistic logic these formulas do not hold, although the following do. ◦ `∃xφ(x)→¬∀x¬φ(x)`, ◦ `∀x¬¬(φ(x)∨¬φ(x))`.² See: ¹http://www.cs.nott.ac.uk/~psznza/papers/Alechina++:01a.pdf ²http://www.phil.uu.nl/~iemhoff/Mijn/Slides/seattle17.pdf – Netsu May 05 '19 at 04:17

0 Answers0