# Example of existence proof in dependent typing?

I understand that $\Pi$ types are generalizations of functions and can be interpreted similar to $\forall$ in logic. I also know that $\Sigma$ types are generalizations of tuples and can be interpreted similar to $\exists$ in logic. But whereas I find it easy to imagine $\Pi$ type examples by thinking in Haskell, I am having a hard time thinking of good examples of $\Sigma$ types. Is there a particular "canonical" $\Sigma$ type that gives a good indication of how it can be interpreted as existence when the type is thought of as a proof?

$\Sigma$-types in Haskell appear in various places. Because Haskell is not dependently typed, they often reduce to the non-dependent version of $\Sigma$-types, which are just Cartesian products. So whenever you see an ordered pair, or a record, that is a simple case of a $\Sigma$-type.

At the level of a modules there can be dependencies and so we get actual $\Sigma$-types. For instance, a module which defines a type $T$ and then a value $f$ of type $T \to T$ has the kind $\Sigma_{T : \mathrm{Type}} (T \to T)$. (The module should hide the definition of $T$ in order for this to actually be the case.) Observe that this is a "large" dependent sum because it ranges over "all Haskell types $T$" so I refer to it as a "kind". In fact, the theory of modules is based on the observation that hiding bits of a program behind a layer of abstraction is precisely the same as forming a dependent sum.

Haskell has existential types. These are like depenent sums of the kind I mentioned above. Namely, an existential type

data Calf = forall t . Bull t => Cow(t)


is just a confusing way of writing $$\mathtt{Calf} = \textstyle \sum_{t : \mathtt{Bull}} Cow(t).$$ Strangely, the "forall" keywords indicates the fact that there exists a type $t$ of class $\mathtt{Bull}$ such that $F(t)$. Perhaps some Haskellites can explain the logic behind the notation to me.

• There is no deep logic behind the notation, other than it being a forall in a negative position: $(\forall t. \mathrm{Bull}(t) \Rightarrow \mathrm{Cow}(t)) \equiv \mathrm{Calf}$ – cody Sep 1 '13 at 23:49
• Sorry, but the only equivalence like that I am aware of is that $(\exists t . \phi(t)) \Rightarrow \psi$ is equivalent to $\forall t . (\phi(t) \Rightarrow \psi)$. Notice how $\psi$ does not depend on $t$. Are you talking about something else? – Andrej Bauer Sep 2 '13 at 5:14
• Well no, but in this case $\psi$ is $\mathrm{Calf}$ and not $\mathrm{Cow(t)}$. The type is $\forall t. \mathrm{Bull}(t) \Rightarrow \mathrm{Cow}(t)\Rightarrow \mathrm{Calf}$ which is equivalent to $(\exists t. \mathrm{Bull}(t)\wedge\mathrm{Cow}(t))\Rightarrow \mathrm{Calf}$. Sorry for the confusion. – cody Sep 3 '13 at 3:04
• I don't think this is quite true. The existential in haskell is not exactly a $\Sigma$. A sigma is the dependent version of the connective $\&$ (pronounced with") which is negative, while the haskell existential is more like a dependent (except we erase types, so the first argument disappears) version of $\otimes$ and is positive. We can't express sigma (even when the first argument is a type) in Haskell, because the projections are not typeable without dependent types. On the other hand, ML modules are real sigmas (but at the cost of no longer being first class). – Philip JF Nov 28 '13 at 1:26

Well, how about the proof that every number is zero or has a predecessor? It turns into a function which takes as input an integer, and as output returns either a proof that it is zero, or the predecessor, and a proof that it is indeed the predecessor.

In Coq:

Fixpoint pred (n : nat): {n = 0} + {exists m, S m = n} :=
match n with
| 0 => left (eq_refl 0)
| S m => right (ex_intro _ m (eq_refl (S m)))
end.

Eval compute in (pred 12).
> right (ex_intro (fun m : nat => S m = 12) 11 eq_refl)


In Coq, $\{\_\}+\{\_\}$ is the Either type of Haskell, and exists is just $\Sigma$. You can see that the function matches on the integer, and returns the proof of $0 = 0$ in the first branch, and the pair $(m, p)$ where $p$ is a proof of $m+1 = n$ in the other branch (ex_intro is just a special pair constructor for exists. The predecessor of 12 is correctly computed to be 11 in the following call.