On 12/17/12 7:13 AM, Ben Millwood wrote:> On Mon, Dec 17, 2012 at 2:39 AM,
wren ng thornton
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:
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