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? 
Example of existence proof in dependent typing?
type theory;dependent types