3 ms·
> It is unfortunate coincidence, but Haskell sum types don't correspond to sums of spaces. It depends on the perspective. Both are a form of coproduct https://
by knappa 4y ago
> It is unfortunate coincidence, but Haskell sum types don't correspond to sums of spaces.
It depends on the perspective. Both are a form of coproduct https://en.wikipedia.org/wiki/Coproduct https://en.wikipedia.org/wiki/Coproduct which forms a disjoint set for types (and sets and topological spaces) while forming a direct product for vector spaces. Confusingly, the vector space sum is a product of sets. (but you can see that it is an addition when you look at the resulting dimensions) The product operation for vector spaces is the tensor product.
- nextaccountic 4y ago> Confusingly, the vector space sum is a product of sets. But why?
- knappa 4y agoIt's the unique thing that makes the commutative diagram from the wikipedia article work. As in: You want V⊕W to be a vector space that contains the vector spaces V and W. You want that for any linear maps V → U and W → U, you get a linear map V⊕W → U which agrees on the inclusions. Since these maps can be arbitrary, you know that dim(V⊕W)≥dim(V)+dim(W) since you can't have any colinearities between the images of V and W in V⊕W. Plus you want that the map V⊕W → U is unique. This means that the images of V and W span V⊕W. Otherwise you have another vector that you can send to arbitrary places. This all means that V⊕W must be a vector space that has dim(V⊕W)=dim(V)+dim(W). Now all you have to do is provide a concrete candidate for V⊕W and the set of ordered pairs (v,w)∈V×W with coordinate-wise addition (+etc.) works.