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.

StackExchange Computer Science Q#14060, answer score: 5