
21 Jun
2011
21 Jun
'11
10:48 p.m.
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.