Proposal: merge Data.Functor.Coproduct into transformers

[Ben Millwood]

On Mon, Dec 17, 2012 at 2:39 AM, wren ng thornton <wren at freegeek.org> wrote:
> On 12/16/12 9:36 AM, Andreas Abel wrote:
>>
>> Standing up against the dictator...
>>
>> I like neither 'Product' nor 'Sum'.  For one, they are ambiguous already
>> in type theory.
>
>
> Yeah, this is one of the reasons I prefer Coproduct (or EitherF, or
> Either1). FWIW, I wrote a short blog post about this terminological
> confusion some time back:
>
>     http://winterkoninkje.dreamwidth.org/72346.html
>

Hmm. As I always understood it, the confusion was because a dependent
sum (i.e. a dependent pair type) is really very similar to a disjoint
union of the A-indexed family of types given by "for each a in A, {<a,
b> : b in P(a)}". Categorically, this could also be considered as an
A-indexed coproduct, so I'm not sure you resolve the ambiguity like
that, except by avoiding convention.

(It was one of the great epiphanies in my understanding of Type Theory
that a dependent sum involving a constant dependent type was a
product, by analogy with how the sum over n = 1 to N of a constant
function M is the product NM).