Rethinking Tricky Classes: Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms

OpenKinds.markdown

Reddit discussion

Continuation of Encoding Overlapping, Extensible Isomorphisms: encoding "open kinds" to better express some awkward type classes.

Further reading

• Monoids: Theme and Variations (Functional Pearl)
• Verified Parallel String Matching in Haskell

Monoid (Homo)morphisms

data MHOM :: Type -> Type -> Type

type m ·-> m' = MHOM m m' -> Type

class (Monoid m, Monoid m') => MonHom (mhom :: m ·-> m') where
  monHom :: m -> m'

length & mconcat

length & mconcat both form monoid morphisms

data MonHom_Len     :: [a] ·-> Sum Int
data MonHom_MConcat :: [a] ·-> a

instance MonHom (MonHom_Len :: [a] ·-> Sum Int) where
  monHom :: [a] -> Sum Int
  monHom xs = Sum (length xs)

instance Monoid a => MonHom (MonHom_MConcat :: [a] ·-> a) where
  monHom :: [a] -> a
  monHom = mconcat

Action as a monoid morphism

The laws of monoid actions m ·- a

act mempty    ≡ id
act (m <> m') ≡ act m . act m'

can be seen as specifying a monoid homomorphism: a function from m to the monoid Endo a

actHom :: forall m a act. Action (act :: m ·- a) => m -> Endo a
actHom m = Endo (act @m @a @act m)

actHom mempty    ≡ mempty
actHom (m <> m') ≡ actHom m <> actHom m'

We specify this with a monoid homomorphism (m ·-> Endo a) indexed by a monoid Action (m ·- a)

data MonHom_Action :: (m ·- a) -> (m ·-> Endo a)

instance Action act => MonHom (MonHom_Action act) where
  monHom :: m -> Endo a
  monHom = actHom @m @a @act

Given Action Action_Cayley we see that there is a monoid homomorphism from any Monoid m to Monoid (Endo m)

monHom @m @(Endo m) @(MonHom_Action Action_Cayley) :: forall m. Monoid m => m -> Endo m

foldMap

Given a function f, foldMap @[] f is a monoid morphism. Assuming we have -XDependentTypes we can write

data MonHom_FoldMap :: (a ~> m) -> ([a] ·-> m)

instance pi f. MonHom (MonHom_FoldMap f) where
  monHom :: [a] -> m
  monHom = foldMap @[] f

Further reading

• Abstracting with Applicatives
• Constructing Applicative Functors
• Denotational Design

I want to define an Applicative instance for Sum but I run into a problem.

-- Sum f g a = Either (f a) (g a)
data Sum f g a = InL (f a) | InR (g a)

In the case of (<*>) we are combing two Sums:

• If they are both InL we combine them with (<*>) @f.
• If they are both InR we combine them with (<*>) @g.

instance (Applicative f, Applicative g, ??) => Applicative (Sum f g) where
  pure :: a -> Sum f g a
  pure = InR . pure

  (<*>) :: Sum f g (a -> b) -> Sum f g a -> Sum f g b
  InL ff <*> InL fx = InL (ff <*> @f fx)
  InR gf <*> InR gx = InR (gf <*> @g gx)
  ...

but what about when they differ? We have no way of transforming between f a into a g a.

Applicative Morphisms

Applicative morphisms are functions f ~> g, so do we just make a type class? That's what Abstracting with Applicatives does, and now we can fill in the remaining cases:

type f ~> g = forall xx. f xx -> g xx

class Natural f g where
    eta :: f ~> g
 
instance (Applicative f, Applicative g, Natural g f) => Applicative (Sum f g) where
  pure :: a -> Sum f g a
  pure = InR . pure

  (<*>) :: Sum f g (a -> b) -> Sum f g a -> Sum f g b
  InL ff <*> InL fx = InL (ff     <*> @f     fx)
  InR gf <*> InR gx = InR (gf     <*> @g     gx)
  InL ff <*> InR gx = InL (ff     <*> @f eta gx)
  InR gf <*> InL fx = InL (eta gf <*> @f     fx)

but we are greeted with a familiar story

In theory, there should also be a natural transformation that can be built magically from the product of any other two natural transformations, but that will just confuse the Haskell typechecker hopelessly. This is because we know that often different "paths" of typeclass choices will often be isomorphic, but the compiler has to actually pick one "canonical" composition of natural transformations to compute with, although multiple paths will typically be possible.

For similar reasons of avoiding overlap, we can't both have the terminal homomorphism that sends everything to Const m and the initial homomorphism that sends Identity to anything like so:

instance Monoid m => Natural f (Const m) where
  eta :: f ~> Const m
  eta _ = Const mempty

instance Applicative g => Natural Identity g where
  eta :: Identity ~> g
  eta (Identity a) = pure @g a

— Abstracting with Applicatives

with a familiar solution

data APPL :: (Type -> Type) -> (Type -> Type) -> Type

type f ·~> f' = APPL f f' -> Type

class (Applicative f, Applicative f') => AppHom (app :: f ·~> f') where
  appHom :: f ~> f'

We can create a newtype of Sum with a phantom witness of an Applicative morphism (this can derive for Sum using -XDerivingVia since it has the same representation)

newtype Sum_ (app :: f ·~> f') a = S_ (Sum f' f a)
  deriving newtype Functor

instance AppHom (app :: f' ·~> f) => Applicative (Sum_ app)

and this allows us to derive Sum f Identity (also known as Lift f)

data App_Initial  f   :: Identity ·~> f
data App_Terminal f m :: f ·~> Const m

instance Applicative f => AppHom (App_Initial f) where
  appHom :: Identity ~> f
  appHom (Identity a) = pure @f a

instance (Applicative f, Monoid m) => AppHom (App_Terminal f m) where
  appHom :: f ~> Const m
  appHom _ = Const mempty

-- Either (f a) a
newtype Lift f a = Lift (Sum f Identity a)
  deriving (Functor, Applicative)
    via (Sum_ (App_Initial f))

-- Either String (f a)
newtype Foo f a = Foo (Sum (Const String) f a)
  deriving (Functor, Applicative)
    via (Sum_ (App_Terminal f String))

Product of two Applicative morphisms

Returning to the other example that didn't work with the standard encoding:

In theory, there should also be a natural transformation that can be built magically from the product of any other two natural transformations, but that will just confuse the Haskell typechecker hopelessly.

Can be easily written as

data App_Comp :: (f ·~> f') -> (f' ·~> f'') -> (f ·~> f'')

instance (AppHom app, AppHom app') => AppHom (App_Comp app app' :: f ·~> f'') where
  appHom :: f ~> f''
  appHom = appHom @_ @_ @app' . appHom @_ @_ @app

We can also define a Semigroup action, and make it a super class of Monoid actions:

-- act (a <> @s b) = act a . act b
class Semigroup s => SemigroupAction (act :: s ·- a) where
  act :: s -> (a -> a)

-- m_act (mempty @m) = id
class (SemigroupAction act, Monoid m) => MonoidAction (act :: m ·- a) where

Lifting a Semigroup action to a Monoid action

If we wanted to lift a SemigroupAction to a MonoidAction in the style of semigroups-actions we would need to define a newtype OptionSet s a = OptionSet a and the final type would look like:

act :: (Monoid s, SemigroupAct s a) => Option s -> OptionSet s a -> OptionSet s a 

Using the approach under study the type becomes the more palatable Option s -> (a -> a):

data Action_Lift :: (s ·- a) -> (Option s ·- a)

instance (SemigroupAction act, Semigroup s) => SemigroupAction (Action_Lift act :: Option s ·- a) where
  act :: Option s -> (a -> a)
  act = \case
    Option Nothing  -> id
    Option (Just s) -> act @s @a @act @s

instance (SemigroupAction act, Monoid m) => MonoidAction (Action_Lift act :: Option m ·- a)

Generalize Cayley to Semigroup

Differentiating between SemigroupAction and MonoidAction allows us to use the more general (<>) in the definition

data Action_Cayley :: s ·- s

instance Semigroup => SemigroupAction (Action_Cayley :: s ·- s) where
  act :: s -> (s -> s)
  act = (<>)

instance Monoid m => MonoidAction (Action_Cayley :: m ·- m)

With semigroups-actions act would get the unnecessarily wrapped type SelfAct s -> (SelfAct s -> SelfAct s).

Repeating n-times

data Action_Repeat :: Product Int ·- m

instance Monoid m => SemigroupAction (Action_Repeat :: Product Int ·- m) where
  act :: Product Int -> (m -> m)
  act (Product n) = mconcat . replicate n

Acting on Enum

From Data.Semigroup.Act.Enum. Semigroup action of an integer acting on an Enum.

data Action_Enum :: Sum Int ·- a

instance Enum a => SemigroupAction (Action_Enum :: Sum Int ·- a) where
  act :: Sum Int -> (a -> a)
  act (Sum n) = toEnum . (+ n) . fromEnum

N

e

x

t

up

...

Adjunctions?

Really witnessed by a natural isomorphism (Iso1).

Functors?

Once we go Category polymorphic we start running into similar issues: See reddit thread.