defaultable-map: An Applicative wrapper for Maps

I’m announcing a small utility Haskell package I created that can wrap arbitrary Map-like types to provide Applicative and Alternative instances. You can find this package on Hackage here:

• defaultable-map: Applicative maps

I can motivate why the Applicative and Alternative instances matter with a small example. Suppose that I define the following three Maps which are sort of like database tables:

import Defaultable.Map 

firstNames :: Defaultable (Map Int) String
firstNames = fromList [(0, "Gabriella"), (1, "Oscar"), (2, "Edgar")]

lastNames :: Defaultable (Map Int) String
lastNames = fromList [(0, "Gonzalez"), (2, "Codd"), (3, "Bryant")]

handles :: Defaultable (Map Int) String
handles = fromList [(0, "GabriellaG439"), (1, "posco"), (3, "avibryant")]

If you squint, you can think of these as analogous to database tables, where the primary key is an Int index:

> CREATE TABLE firstNames (id integer, firstName text);
> INSERT INTO firstNames (id, firstName) VALUES (0, 'Gabriella');
> INSERT INTO firstNames (id, firstName) VALUES (1, 'Oscar');
> INSERT INTO firstNames (id, firstName) VALUES (2, 'Edgar');
> SELECT * FROM firstNames;
id | firstName
---+----------
0  | Gabriella
1  | Oscar
2  | Edgar

> CREATE TABLE lastNames (id integer, lastName text);
> INSERT INTO lastNames (id, lastName) VALUES (0, 'Gonzalez');
> INSERT INTO lastNames (id, lastName) VALUES (2, 'Codd');
> INSERT INTO lastNames (id, lastName) VALUES (3, 'Bryant');
> SELECT * FROM lastNames;
id | lastName
---+---------
0  | Gonzalez
2  | Codd
3  | Bryant

> CREATE TABLE handles (id integer, handle text);
> INSERT INTO handles (id, handle) VALUES (0, 'GabriellaG439');
> INSERT INTO handles (id, handle) VALUES (1, 'posco');
> INSERT INTO handles (id, handle) VALUES (3, 'avibryant');
> SELECT * FROM handles;
id | handle
---+--------------
0  | GabriellaG439
1  | posco
3  | avibryant

The Defaultable (Map Int) type has a law-abiding Applicative instance, so we can safely “join” these “tables” using Applicative operations. For example, if we enable Haskell’s ApplicativeDo language extension then we can compute an “inner join” on tables like this:

{-# LANGUAGE ApplicativeDo #-}

innerJoin :: Defaultable (Map Int) (String, String)
innerJoin = do
    firstName <- firstNames
    lastName  <- lastNames
    return (firstName, lastName)

… and that evaluates to the following result:

Defaultable
    (fromList
        [ (0, ("Gabriella","Gonzalez"))
        , (2, ("Edgar"    ,"Codd"    ))
        ]
    )
    Nothing

… which is the same result we would have gotten from doing an inner join in SQL:

> SELECT firstNames.id, firstName, lastName
>     FROM firstNames INNER JOIN lastNames on firstNames.id = lastNames.id;
id | firstName | lastName
---+-----------+---------
0  | Gabriella | Gonzalez
2  | Edgar     | Codd

The Defaultable (Map Int) type also has a law-abiding Alternative instance, which we can combine with the Applicative instance to compute “left/right/outer joins”. For example, this “left join”:

leftJoin :: Defaultable (Map Int) (String, Maybe String)
leftJoin = do
    firstName <- firstNames
    lastName  <- optional lastNames
    return (firstName, lastName)

… evaluates to:

Defaultable
    (fromList
        [ (0, ("Gabriella",Just "Gonzalez"))
        , (1, ("Oscar"    ,Nothing        ))
        , (2, ("Edgar"    ,Just "Codd"    ))
        ]
    )
    Nothing

… which is analogous to this SQL left join:

> SELECT firstNames.id, firstName, lastName
>     FROM firstNames LEFT JOIN lastNames on firstNames.id = lastNames.id;
id | firstName | lastName
---+-----------+---------
0  | Gabriella | Gonzalez
1  | Oscar     |
2  | Edgar     | Codd

Since Haskell is a more fully-featured language than SQL, we can do more sophisticated things more easily than in SQL. For example, the following three-way join with some post-processing logic is much easier to express in Haskell than SQL:

display :: String -> Maybe String -> String -> String
display firstName Nothing handle =
    firstName <> ": @" <> handle
display firstName (Just lastName) handle =
    firstName <> " " <> lastName <> ": @" <> handle

interestingJoin :: Defaultable (Map Int) String
interestingJoin = do
    firstName <- firstNames
    lastName  <- optional lastNames
    handle    <- handles
    return (display firstName lastName handle)

… which evaluates to:

Defaultable
    (fromList
        [ (0, "Gabriella Gonzalez: @GabriellaG439")
        , (1, "Oscar: @posco"                     )
        ]
    )
    Nothing

The Defaultable type constructor

The central data type exported by the package is the Defaultable type constructor, which has the following simple definition:

data Defaultable map value = Defaultable (map value) (Maybe value)

Here the map type parameter can be any Map-like type that includes the type of the key. For example, a typical instantiation of the Defaultable type constructor might be Defaultable (Map key) value or Defaultable IntMap value.

The first field of the type is the actual map that you want to wrap in order to get an Applicative and Alternative instance. The second field is an optional default value stored alongside the map that can be returned if a lookup does not find a matching key.

The default value is not required (it can be Nothing), but that default value is what makes the Applicative instance work. Specifically, without the ability to specify a default value there would be no way to implement pure for a Map-like type.

In case you’re curious, here is what the Applicative instance looks like:

instance (Apply map, forall a . Monoid (map a)) => Applicative (Defaultable map)
  where
    pure v = Defaultable mempty (pure v)

    Defaultable fMap fDefault <*> Defaultable xMap xDefault =
        Defaultable fxMap fxDefault
      where
        fxMap = (fMap <.> xMap) <> fFallback <> xFallback
          where
            fFallback =
                case fDefault of
                    Nothing -> mempty
                    Just f  -> fmap f xMap

            xFallback =
                case xDefault of
                    Nothing -> mempty
                    Just x  -> fmap ($ x) fMap

        fxDefault = fDefault <*> xDefault

The neat part of the above instance is the class constraint:

          ↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓
instance (Apply map, forall a . Monoid (map a)) => Applicative (Defaultable map)

The Defaultable type is set up in such a way that you can wrap any Map-like type that satisfies that constraint (which is basically all of them) and get a law-abiding Applicative instance (See the Appendix for a proof of the Applicative laws).

In particular, this constraint makes use of the QuantifiedConstraints language extension introduced in GHC 8.6. Without that instance then we wouldn’t be able to generalize this type to wrap arbitrary Maps and we’d have to hard-code the package to work with a specific Map like Data.Map.Map.

The Defaultable type also implements Alternative, too, although that instance is much simpler:

instance (Apply map, forall a . Monoid (map a)) => Alternative (Defaultable map) where
    empty = Defaultable mempty empty

    Defaultable lMap lDefault <|> Defaultable rMap rDefault =
        Defaultable (lMap <> rMap) (lDefault <|> rDefault)

This instance is only possible because the Defaultable type constructor doesn’t require the default value to be present. If the default value were required then we could not sensibly define empty.

Prior art

I was surprised that something like this didn’t already exist on Hackage. The closest package I could find was this one:

• total-map: Finitely represented total maps

However, that wasn’t exactly what I wanted, because it requires the default value to be present. That means that you can’t implement an Alternative instance for the TMap type from that package and you therefore can’t do things like left/right/outer joins as I mentioned above.

Also, more generally, sometimes you want a Map to have an Applicative instance without having to specify a default value. Requiring the default to always be present is not necessary to implement Applicative.

The other issue I had with that package is that it’s hard-coded to use Data.Map.Map under the hood, whereas I wanted an API that could be used in conjunction with any Map-like type.

Conclusion

The idea for this package originated from a LambdaConf presentation I gave a while ago where I brainstormed what a good “data science” ecosystem for Haskell might look like:

• Data science APIs in Haskell - slides

I sat on this idea for years without publishing anything to Hackage because my original vision was a bit too ambitious and included much more than just an Applicative Map type. However, recently I needed this Applicative Map type, so I settled for publishing a narrower and more focused package to Hackage.

The personal use case I have in mind for this package is no longer data science, but I hope that people interested in building a data science ecosystem for Haskell consider using this package as a building block since I believe it is well-suited for that purpose.

Appendix - Proof of the Applicative laws

These proofs require a few additional assumptions about the interaction between the Apply and Monoid constraint on the map type parameter to Defaultable. These assumptions hold for Map-like types.

The first assumption is that fmap is a Monoid homomorphism:

fmap f mempty = mempty

fmap f (x <> y) = fmap f x <> fmap f y

The second assumption is that f <.> is a Monoid homorphism:

f <.> mempty = mempty

f <.> (x <> y) = (f <.> x) <> (f <.> y)

The final assumption is specific to maps, which is:

-- Given:
mf :: map (a -> b)
mx :: map a
kf :: (a -> b) -> c
kx :: a -> c

  (mf <.> mx) <> fmap kf mf <> fmap kx mx
= (mf <.> mx) <> fmap kx mx <> fmap kf mf

The intuition here is if that map is a Map-like type constructor then we can think of those three expressions as having a set of keys associated with them, such that:

-- Given:
keys :: map a -> Set key

keys (mf <.> mx) = keys (fmap kf mf) `intersection` keys (fmap kx mx)

So normally the following equality would not be true:

  fmap kf mf <> fmap kx mx
= fmap kx mx <> fmap kf mf

… because the result would change if there was a key collision. Then the order in which we union (<>) the two maps would change the result.

However, if you union yet another map (mf <.> mx) that shadows the colliding keys then result remains the same.

The proof below uses that assumption a bit less formally by just noting that we can commute a union operation if there is a downstream union operation that would shadow any colliding keys that might differ.

Proof of identity law

pure id <*> v

-- pure v = Defaultable mempty (pure v)
= Defaultable mempty (pure id) <*> v

-- Expand: v = Defaultable xMap xDefault
= Defaultable mempty (pure id) <*> Defaultable xMap xDefault

-- Definition of (<*>)
= Defaultable fxMap fxDefault
  where
    fxMap = (mempty <.> xMap) <> fFallback <> xFallback
      where
        fFallback =
            case pure id of
                Nothing -> mempty
                Just f  -> fmap f xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- mempty <.> xMap = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback =
            case pure id of
                Nothing -> mempty
                Just f  -> fmap f xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- Simplify `case pure id of …`
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback = fmap id xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- fmap id x = x
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback = xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> fmap ($ x) mempty

    fxDefault = pure id <*> xDefault

-- fmap f mempty = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = mempty < >fFallback <> xFallback
      where
        fFallback = xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> mempty

    fxDefault = pure id <*> xDefault

-- pure id <*> v = v
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> fFallback <> xFallback
      where
        fFallback = xMap

        xFallback =
            case xDefault of
                Nothing -> mempty
                Just x  -> mempty

    fxDefault = xDefault

-- Simplify
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> xMap <> mempty

    fxDefault = xDefault

-- x <> mempty = x
-- mempty <> x = x
= Defaultable fxMap fxDefault
  where
    fxMap = xMap

    fxDefault = xDefault

-- Simplify
= Defaultable xMap xDefault

-- Contract: v = Defaultable xMap xDefault
= v

Proof of the composition law

pure (.) <*> u <*> v <*> w

-- Expand:
-- u = Defaultable uMap uDefault
-- v = Defaultable vMap vDefault
-- w = Defaultable wMap wDefault
=       pure (.)
    <*> Defaultable uMap uDefault
    <*> Defaultable vMap vDefault
    <*> Defaultable wMap wDefault

-- pure v = Defaultable mempty (pure v)
=       Defaultable mempty (pure (.))
    <*> Defaultable uMap uDefault
    <*> Defaultable vMap vDefault
    <*> Defaultable wMap wDefault

… before continuing, it’s easiest to prove all eight possible combinations of:

• uDefault is pure u or empty
• vDefault is pure v or empty
• wDefault is pure w or empty

To avoid lots of repetition, I’ll only prove the most difficult case (where all defaults are present), since the other proofs are essentially subsets of that proof where some subterms disappear because they become mempty.

Case:

• uDefault = pure u
• vDefault = pure v
• wDefault = pure w

=       Defaultable mempty (pure (.))
    <*> Defaultable uMap (pure u)
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- Definition of (<*>)
=       (Defaultable cuMap cuDefault
          where
            cuMap = (mempty <.> uMap) <> fmap (.) uMap <> fmap ($ u) mempty

            cuDefault = pure (.) <*> pure u
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- mempty <.> x = mempty
=       (Defaultable cuMap cuDefault
          where
            cuMap = mempty <> fmap (.) uMap <> fmap ($ u) mempty

            cuDefault = pure (.) <*> pure u
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- fmap f mempty = mempty
=       (Defaultable cuMap cuDefault
          where
            cuMap = mempty <> fmap (.) uMap <> mempty

            cuDefault = pure (.) <*> pure u
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- pure f <*> pure x = pure (f x)
=       (Defaultable cuMap cuDefault
          where
            cuMap = mempty <> fmap (.) uMap <> mempty

            cuDefault = pure ((.) u)
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- x <> mempty = x
-- mempty <> x = x
=       (Defaultable cuMap cuDefault
          where
            cuMap = fmap (.) uMap

            cuDefault = pure ((.) u)
        )
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- Simplify
=       (Defaultable (fmap (.) uMap) (pure (u .)))
    <*> Defaultable vMap (pure v)
    <*> Defaultable wMap (pure w)

-- Definition of (<*>)
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap ($ v) (fmap (.) uMap)

            cuvDefault = pure (u .) <*> pure v
        )
    <*> Defaultable wMap (pure w)

-- fmap f (fmap g x) = fmap (f . g) x
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap (. v) uMap

            cuvDefault = pure (u .) <*> pure v
        )
    <*> Defaultable wMap (pure w)

-- ((.) u) = \v -> u . v
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap (. v) uMap

            cuvDefault = pure (u .) <*> pure v
        )
    <*> Defaultable wMap (pure w)

-- pure f <*> pure x = pure (f x)
=       (Defaultable cuvMap cuvDefault
          where
            cuvMap =
                    (fmap (.) uMap <.> vMap)
                <>  fmap (u .) vMap
                <>  fmap (. v) uMap

            cuvDefault = pure (u . v)
        )
    <*> Defaultable wMap (pure w)

-- Definition of (<*>)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap = (cuvMap <.> wMap) <> fmap (u . v) wMap <> fmap ($ w) cuvMap 
      where
        cuvMap =
                (fmap (.) uMap <.> vMap)
            <>  fmap (u .) vMap
            <>  fmap (. v) uMap

    cuvwDefault = pure (u . v) <*> pure v

-- (f <> g) <.> x = (f <.> x) <> (g <.> x)
-- fmap f (x <> y) = fmap f x <> fmap f y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (fmap (.) uMap <.> vMap <.> wMap)
        <>  (fmap (u .) vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u . v) <*> pure w

-- pure f <*> pure x = pure (f x)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (fmap (.) uMap <.> vMap <.> wMap)
        <>  (fmap (u .) vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap (.) u <.> v <.> w = u <.> (v <.> w)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (fmap (u .) vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (x <.> y) = fmap (f .) x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (fmap (. v) uMap <.> wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- x <.> fmap f y = fmap (. f) x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  fmap ($ w) (fmap (.) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (x <.> y) = fmap (f .) x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (fmap (($ w) .) (fmap (.) uMap) <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) x
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (fmap ((($ w) .) . (.)) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- ((($ w) .) . (.))
-- = \u -> (($ w) .) ((.) u)
-- = \u -> (($ w) .) (u .)
-- = \u -> ($ w) . (u .)
-- = \u v -> ($ w) ((u .) v)
-- = \u v -> ($ w) (u . v)
-- = \u v -> (u . v) w
-- = \u v -> u (v w)
-- = \u v -> u (($ w) v)
-- = \u -> u . ($ w)
-- = (. ($ w))
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (fmap (. ($ w)) uMap <.> vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- x <.> (f <$> y) = (. f) <$> x <.> y
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (u . v) wMap
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap ($ w) (fmap (u .) vMap)
        <>  fmap ($ w) (fmap (. v) uMap)

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) w
-- (f . g) = \x -> f (g x)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- `fmap (\w -> u (v w)) wMap <> (uMap <.> fmap ($ w) vMap)` commutes because
-- the colliding keys are shadowed by `(uMap <.> (vMap <.> wMap))`
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- `fmap u (vMap <.> wMap) <> (uMap <.> fmap v wMap)` commutes because the
-- colliding keys are sahdowed by `(uMap <.> (vMap <.> wMap))`
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> fmap v wMap)
        <>  fmap u (vMap <.> wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- `fmap u (vMap <.> wMap) <> (uMap <.> fmap ($ w) vMap)` commutes because the
-- colliding keys are sahdowed by `(uMap <.> (vMap <.> wMap))`
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap (\w -> u (v w)) wMap
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- \w -> u (v w) = u . v
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap (u . v) wMap)
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) x, in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap (\v -> u (v w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- \v -> u (v w)
-- = \v -> u (($ w) v)
-- = u . ($ w)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap (u . ($ w)) vMap
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- fmap f (fmap g x) = fmap (f . g) x, in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap u (fmap ($ w) vMap)
        <>  fmap (\u -> u (v w)) uMap

    cuvwDefault = pure (u (v w))

-- \f -> f x = ($ x)
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap =
            (uMap <.> (vMap <.> wMap))
        <>  (uMap <.> (fmap v wMap)
        <>  (uMap <.> fmap ($ w) vMap)
        <>  fmap u (vMap <.> wMap)
        <>  fmap u (fmap v wMap)
        <>  fmap u (fmap ($ w) vMap)
        <>  fmap ($ (v w)) uMap

    cuvwDefault = pure (u (v w))

-- f <.> (x <> y) = (f <.> x) <> (f <.> y), in reverse
-- fmap f (x <> y) = fmap f x <> fmap f y, in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap = (uMap <.> vwMap) <> fmap u vwMap <> fmap ($ (v w)) uMap
      where
        vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap

    cuvwDefault = pure (u (v w))

-- pure f <*> pure x = pure (f x), in reverse
= Defaultable cuvwMap cuvwDefault
  where
    cuvwMap = (uMap <.> vwMap) <> fmap u vwMap <> fmap ($ (v w)) uMap
      where
        vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap

    cuvwDefault = pure u <*> pure (v w)

-- Definition of (<*>), in reverse
=   (   Defaultable uMap (pure u)
    <*> (Defaultable vwMap vwDefault
          where
            vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap

            vwDefault = pure (v w)
        )
    )

-- pure f <*> pure x = pure (f x), in reverse
=   (   Defaultable uMap (pure u)
    <*> (Defaultable vwMap vwDefault
          where
            vwMap = (vMap <.> wMap) <> fmap v wMap <> fmap ($ w) vMap 

            vwDefault = pure v <*> pure w
        )
    )

-- Definition of (<*>), in reverse
=   (   Defaultable uMap (pure u)
    <*> (   Defaultable vMap (pure v)
        <*> Defaultable wMap (pure w)
        )
    )

-- Contract:
-- u = Defaultable uMap uDefault
-- v = Defaultable vMap vDefault
-- w = Defaultable wMap wDefault
= u <*> (v <*> w)

Proof of homomorphism law

pure f <*> pure x

-- pure v = Defaultable mempty (pure v)
= Defaultable mempty (pure f) <*> Defaultable mempty (pure x)

-- Definition of (<*>)
= Defaultable fxMap fxDefault
  where
    fxMap =  (mempty <.> mempty) <> fmap f mempty <> fmap ($ x) mempty

    fxDefault = pure f <*> pure x

-- fmap f mempty = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = (mempty <.> mempty) <> mempty <> mempty

    fxDefault = pure f <*> pure x

-- mempty <.> x = mempty
= Defaultable fxMap fxDefault
  where
    fxMap = mempty <> mempty <> mempty

    fxDefault = pure f <*> pure x

-- mempty <> x = x
= Defaultable fxMap fxDefault
  where
    fxMap = mempty

    fxDefault = pure f <*> pure x

-- pure f <*> pure x = pure (f x)
= Defaultable fxMap fxDefault
  where
    fxMap = mempty

    fxDefault = pure (f x)

-- Simplify
= Defaultable mempty (pure (f x))

-- pure v = Defaultable mempty (pure v), in reverse
= pure (f x)

Proof of interchange law

u <*> pure y

-- pure v = Defaultable mempty (pure v)
= u <*> Defaultable mempty (pure y)

-- Expand: u = Defaultable uMap uDefault
= Defaultable uMap uDefault <*> Defaultable mempty (pure y)

-- Definition of (<*>)
= Defaultable uyMap uyDefault
  where
    uyMap = (uMap <.> mempty) <> uFallback <> fmap ($ y) uMap
      where
        uFallback =
            case uDefault of
                Nothing -> mempty
                Just u  -> fmap y mempty

    uyDefault = uDefault <*> pure y

-- fmap f mempty = mempty
= Defaultable uyMap uyDefault
  where
    uyMap = (uMap <.> mempty) <> uFallback <> fmap ($ y) uMap
      where
        uFallback =
            case uDefault of
                Nothing -> mempty
                Just u  -> mempty

    uyDefault = uDefault <*> pure y

-- Simplify `case uDefault of …`
= Defaultable uyMap uyDefault
  where
    uyMap = (uMap <.> mempty) <> uFallback <> fmap ($ y) uMap
      where
        uFallback = mempty

    uyDefault = uDefault <*> pure y

-- f <.> mempty = mempty
= Defaultable uyMap uyDefault
  where
    uyMap = mempty <> uFallback <> fmap ($ y) uMap
      where
        uFallback = mempty

    uyDefault = uDefault <*> pure y

-- mempty <> x = x
= Defaultable uyMap uyDefault
  where
    uyMap = fmap ($ y) uMap

    uyDefault = uDefault <*> pure y

-- u <*> pure y = pure ($ y) <*> u
= Defaultable uyMap uyDefault
  where
    uyMap = fmap ($ y) uMap

    uyDefault = pure ($ y) <*> uDefault

-- pure f <*> x = fmap f x
= Defaultable uyMap uyDefault
  where
    uyMap = fmap ($ y) uMap

    uyDefault = fmap ($ y) uDefault

-- Definition of `fmap`, in reverse
= fmap ($ y) (Defaultable uMap uDefault)

-- Contract: u = Defaultable uMap uDefault
= fmap ($ y) u

-- pure f <*> x = fmap f x, in reverse
= pure ($ y) <*> u