smash: Combinators for Maybe types

This package consists of 3 interesting datatypes and their respective monad transformers:

• Wedge: Isomorphic to Maybe (Either a b). The Wedge datatype represents the coproduct in the category Hask* of pointed Hask types, called a wedge sum. One can derive this type as follows:

  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
  

• Can: Isomorphic to Maybe (These a b). The Can datatype represents the product in Hask*. One can derive this as follows:

  (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
  

• Smash: Isomorphic to Maybe (a,b). The Smash datatype represents a special type of product, a smash product, in the category Hask*. The smash product is a symmetric, monoidal tensor in Hask* that is the quotient of Can over Wedge. It can be derived as follows:

  Can a b / Wedge a b
  ~ 1 + a + b + a*b / 1 + a + b
  -- reassoc coproduct
  ~ (1 + a + b) + a*b / 1 + a + b
  -- def. of quotient: (1 + a + b) ~ 1
  ~ 1 + a * b
  ~ Maybe (a,b)
  ~ Smash a b