6
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

$\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.

$\endgroup$
  • 1
    $\begingroup$ 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}$ $\endgroup$ – cody Sep 1 '13 at 23:49
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Sep 2 '13 at 5:14
  • $\begingroup$ 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. $\endgroup$ – cody Sep 3 '13 at 3:04
  • $\begingroup$ 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). $\endgroup$ – Philip JF Nov 28 '13 at 1:26
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.