Proposal: merge Data.Functor.Coproduct into transformers

[wren ng thornton]

On 12/17/12 7:13 AM, Ben Millwood wrote:> 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 [...]

I'm not entirely sure I'd call it "a confusion" in type theory; it's
really more of a clash of traditions/perspectives. The confusion is what
arises in newcomers first encountering this discrepancy.


As for sigma types being similar to disjoint unions, that's only if we
consider type tags to be literally part of the data. While that's a
feasible perspective, I'm not sure it's the most perspicuous one. The
thing is, we have both a family of adjunctions between products and
exponentials:

    (a*_) --| (_^a)

as well as an adjunction chain relating coproducts to products:

    (_+_) --| \diag --| (_*_)

However, these result in conflicting notions of duality for products. The
set-theoretic terminology highlights the former adjunctions, whereas the
functional-programming terminology highlights the latter adjunctions. Even
if you can encode colimits with limits in a particular category, I
wouldn't say they're the same thing. In certain lattices we can encode
meets with joins (and vice versa), but noone would say those're the same
operation.

-- 
Live well,
~wren