I know that an existential type $ \exists t. t $ can be represented using universally quantified types as $ \forall r. (\forall t. t \rightarrow r) \rightarrow r $ and I have some basic intuition for this result. I wanted to try to derive this representation by hand to gain more understanding of it. I tried the following steps:

$$ \begin{align*} \exists t. t &\quad\text{}\\ \bigvee_{t \in T} t &\quad\text{Definition(?) of existential type} &(1) \\ \lnot \lnot \bigvee_{t \in T} t &\quad\text{Double negation} &(2)\\ \lnot \bigwedge_{t \in T} \lnot t &\quad\text{De Morgan} &(3)\\ \lnot \bigwedge_{t \in T} t \rightarrow False &\quad\text{Substituting $\lnot t = t \rightarrow False$} &(4)\\ (\bigwedge_{t \in T} t \rightarrow False) \rightarrow False &\quad\text{Substituting $\lnot t = t \rightarrow False$} &(5)\\ (\forall t. t \rightarrow False) \rightarrow False &\quad\text{Definition of universal type} &(6) \end{align*} $$

So my derivation for $ \exists t. t$ is $ (\forall t. t \rightarrow Void) \rightarrow Void $ where $Void$ is an uninhabited type. I can see that the first representation (starting with $\forall r.$) can represent this by simply specializing to $r = Void$, however I'm not sure if it's possible to get from my derivation to the correct one. In addition, writing code with this Void derivation seems impossible; I can't possibly learn anything about the value since the continuation only returns Void.

I have a feeling that I am translating predicate logic to type logic too literally, and some of my steps may be wrong, for example I'm not sure if it's meaningful to negate a type. Also in step 1, I am representing the existential type with an [inclusive] disjunction, even though an existential type can only have one type at a time.

That said, it seems like my derivation is close so I'm wondering if there's some truth to what I've done. Have I gone wrong somewhere in my proof? Is it possible to connect this to the correct derivation of existential types?

Side note: proof of $ \lnot t = t \rightarrow False $:

$$ % \begin{align*} \lnot t \\ False \vee \lnot t \\ t \rightarrow False % \end{align*} $$

  • $\begingroup$ This question is related however it doesn't give the derivation that I'm looking for $\endgroup$ Commented Dec 28, 2021 at 19:35
  • 1
    $\begingroup$ You are using classical logic all over the place. In this case it will lead you astray. You should use the rules of intuitionistic logic instead. The law you are looking for is the equivalence of $(\exists x . \phi (x)) \to \psi$ and $\forall x . (\phi(x) \to \psi)$, which is intuitionistically valid. $\endgroup$ Commented Jan 1, 2022 at 20:32
  • $\begingroup$ Yes, now that you mention it I can see that $ \lnot \lnot t = t $ does not hold in intuitionistic logic, which makes sense because it would imply that $ Int = \lnot \lnot Int = \lnot False = \lnot \lnot String = String $ It seems like I need a different double-negation law, or the law that you gave. $\endgroup$ Commented Jan 1, 2022 at 23:11
  • $\begingroup$ Just forget about double negation. $\endgroup$ Commented Jan 1, 2022 at 23:38


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.