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?