typelevel
Feature Request: Smash Product, Wedge Sum, Pointed Product
Some new abstractions that provide useful and principled variations on a theme:
- Slides: https://github.com/cohomolo-gy/Hulk-Smash/blob/master/Smash.pdf
- Arithmetic derivation: https://github.com/emilypi/smash/tree/master/smash-core/README.md
Happy to help explain and guide the implementation of these (including their monad transformers and optics).
Hmm, do you have a set of identities governing the behavior? I didn't see that in the haskell docs. Obviously most of it is relatively straightforward from the types, but I'm always leery whenever zeros are involved. I'm also curious about other inhabitants if you have any nice examples off-hand (didn't read through the presentation entirely, so if they're in there, feel free to redirect).
Just looking at the haskell type signatures this seems pretty neat and I've wanted a Wedge data type at some point. Do you have any cool usage examples for these?
@djspiewak I wrote these down in the headers to the modules and in the README for that package:
Can:
Can is a pointed product. This means it's a discrete limiting diagram Hask -> */Hask from Hask to the category of pointed spaces (the slice category of Hask under the terminal object), which preserves the usual associativity, symmetry, and distributivity over pointed coproducts that one might expect. It has the usual product legs that project an element of the product, analogous to fst and snd, but now you have pointed objects instead of the usual haskell type (e.g. canFst :: Can a b -> Maybe a). You can relate them to concrete, well-known patterns that we've probably all found ourselves in at one point:
(Maybe a, Maybe a)
~ (1 + a) * (1 + b)
-- products distribute over coproducts
~ 1 + b + a + a*b
-- coproducts are associative
~ 1 + (b + a + a*b)
~ 1 + These a b
~ Maybe (These a b)
~ Can a b
Can being a limit satisfies the pointed version of the tensor-hom adjunction in */Hask, so you have a form of pointed currying and uncurrying of Cans: canCurry :: (Can a b -> Maybe c) -> Maybe a -> Maybe b -> Maybe c) etc. You also have all the nice facts about associativity, symmetry, distributivity, over pointed colimits (i.e. Wedge), adjoint functor theorems etc. that come from being a product.
Wedge
Likewise, Wedge is the less intuitive encoding of the pointed coproduct, which is obtained by adjoining a unit to discrete coproduct diagrams in Hask, but in order to be "correct" in the sense that it lands in the right category and has the right behavior, we actually construct these via pushout a0 <- * -> b0, which has the following legs as data (analogous to inL and inR for the coproduct): wedgeL :: Maybe a -> Wedge a b and wedgeR :: Maybe b -> Wedge a b. It's a colimit, so it satisfies all of the nice laws you have for pairing (via yoneda), associativity etc etc.
Either (Maybe a) (Maybe b)
~ (1 + a) + (1 + b)
-- units are the same via pushout
~ 1 + a + b
~ Maybe (Either a b)
~ Wedge a b
Smash
The Smash product is a collapsed product of pointed types (a pointed product modulo a wedge).
Can a b / Wedge a b
~ 1 + a + b + a*b / 1 + a + b
-- def. of quotient
~ 1 + a * b
~ Maybe (a,b)
~ Smash a b
This datatype forms its own monoidal tensor of pointed types separate from the pointed product, and so is a separate form of limit available in */Hask which has its own facts about currying, associativity, distributivity over Wedges, symmetry and so on that one might want.
As a datatype, This one is a little less useful than the previous two, but it has some nice properties in and of itself.
I hope that answers your questions.
@LukaJCB Nope! I mean, I've run into them in the wild, so there's sporadicly useful situations where they come up, but the packages were mostly pedagogical and the datatypes have a lot of apparently nice interplay with each other 😄