Re: Proposal: merge Data.Functor.Coproduct into transformers

On Mon, Dec 17, 2012 at 2:39 AM, wren ng thornton 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, { : 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).