A dependent sum is a generalization of a
particular way of thinking about the
Either a b can be thought of as a
(tag, value), where the value of the
tag determines the type of the value. In
tag = Left and
value :: a
tag = Right and
value :: b.
This package allows you to define your own dependent sum types by using your own "tag" types.