Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?

On 6/21/11 6:54 PM, Casey McCann wrote:
That said, I don't think either retains the tidy algebraic properties that disjoint unions and tuples have, so I'm not sure if calling them sums and products is actually correct.
I don't think there are any problems[1]. Categorically speaking, a product of A and B is simply a thing, which we can call Foo[2], along with two projections, f :: Foo -> A and oo :: Foo -> B[3], such that the Foo is the "closest" thing to A and B[4]. I chose the funny names intentionally. Nothing in the definition of products says that there has to be any kind of notion of order between the components, only that the composite has projections for each component and that it has no extra junk. Consequently A*B is isomorphic to B*A, which means they are essentially the same thing[5]. The choice of order is just a convention. For a slightly stronger notion of products we can look to monoidal categories which have that A*(B*C) is isomorphic to (A*B)*C, again meaning that they're essentially the same thing. Outside of category theory, we can look to domain theory (or the associated CPO categories), but domain products and smash products both have the same order independence as categorical products. For coproducts, dually. [1] modulo the A:+:A ~ A issue. [2] More conventionally called A*B, but remember: that's just a name. [3] More traditionally, pi_1 and pi_2, or fst and snd, or... [4] That is, for any other Bar with b :: Bar -> A and ar :: Bar -> B, there is a unique function from Bar to Foo such that everything commutes. [5] The clever reader will notice that they are not *exactly* the same thing, not identical; however, category theorists rarely care about the differences between isomorphic things unless it's mucking up a proof. -- Live well, ~wren

On Tue, Jun 21, 2011 at 9:51 PM, wren ng thornton
I don't think there are any problems[1]. (...) [1] modulo the A:+:A ~ A issue.
That issue is exactly my concern, though, and it seems a bit too thorny to handwave aside. For instance, doesn't this also cause problems for anything of the form (A :+: B) :+: (A :+: C)? I don't doubt there exist formulations that make sense, but it's not immediately obvious to me what they would be, and how they'd behave used as types in something like Haskell. You wouldn't be able to have a straightforward function with the type "forall a b c. (a -> b) -> (a :+: c -> b :+: c)", among other things. In contrast, ordered pairs and disjoint unions are tidy, simple, and obvious. - C.
participants (2)
-
Casey McCann
-
wren ng thornton