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

• The classic Monoids: Theme and Variations (Functional Pearl)
• How to Twist Pointers without Breaking Them.

(Left) Monoid Action

With actions we can can transform as with m-values.

class Action m a where
  act :: m -> (a -> a)
  act _ = id

The documentation for Action includes this unpleasantness

It is a bit awkward dealing with instances of Action, since it is a multi-parameter type class but we can't add any functional dependencies---the relationship between monoids and the types on which they act is truly many-to-many. In practice, this library has chosen to have instance selection for Action driven by the first type parameter. That is, you should never write an instance of the form Action m SomeType since it will overlap with instances of the form Action SomeMonoid t. Newtype wrappers can be used to (awkwardly) get around this.

Let's see how it looks by encoding it as an open kind:

data ACT :: Type -> Type -> Type

type m ·- a = ACT m a -> Type

class Monoid m => Action (act :: m ·- a) where
  act :: m -> (a -> a)

No Action

First we encode what is the default definition of act, where the action does nothing at all:

data Act_Id :: m ·- a

instance Monoid m => Action (Act_Id :: m ·- a) where
  act :: m -> (a -> a)
  act _ = id

Action of [Either m m']

Action of a list of alternating monoidal values ((:+:)): parameterized by the actions act, act' of the individual monoids:

data Act_Eithers :: (m ·- a) -> (m' ·- a) -> ([Either m m'] ·- a)

instance (Action act, Action act') => Action (Act_Eithers act act' :: [Either m m'] ·- a) where
  act :: [Either m m'] -> (a -> a)
  act = appEndo . foldMap (Endo . either (act @_ @_ @act) (act @_ @_ @act'))

HList of Actions (sketchy)

We can specify a heterogeneous list of monoid actions. First we give a standard definition of HList and with elementwise Monoid instances.

data HList :: [Type] -> Type where
  HNil :: HList '[]
  HCons :: a -> HList as -> HList (a:as)

instance Semigroup (HList '[]) where
  (<>) :: HList '[] -> HList '[] -> HList '[]
  HNil <> HNil = HNil

instance (Semigroup s, Semigroup (HList ss)) => Semigroup (HList (s:ss)) where
  (<>) :: HList (s:ss) -> HList (s:ss) -> HList (s:ss)
  HCons a as <> HCons b bs = HCons (a <> b) (as <> bs)

instance Monoid (HList '[]) where
  mempty :: HList '[]
  mempty = HNil

instance (Monoid s, Monoid (HList ss)) => Monoid (HList (s:ss)) where
  mempty :: HList (s:ss)
  mempty = HCons mempty mempty

And then we define the actions inductively:

data Action_Nil :: HList '[] ·- a

data Action_Cons :: (m ·- a) -> (HList ms ·- a) -> (HList (m:ms) ·- a)

instance Action (Action_Nil :: HList '[] ·- a) where
  act :: HList '[] -> (a -> a)
  act HNil = id

instance (Action act, Action acts) => Action (Action_Cons act acts :: HList (m:ms) ·- a) where
  act :: HList (m:ms) -> (a -> a)
  act (HCons m ms) = act @m @a @act m . act @(HList ms) @a @acts ms

Action of pairs

data Action_Pair :: (m ·- a) -> (m ·-> b) -> (m ·-> (a, b))

instance (Action act, Action act') => Action (Action_Pair act act' :: m ·-> (a, b)) where
  act :: m -> ((a, b) -> (a, b))
  act m (a, b) = (a', b') where
    a' = act @m @a @act
    b' = act @m @b @act'

Cayley representation

Monoid Action of some monoid m on its own elements:

data Action_Cayley :: m ·- m

instance Monoid m => Action (Action_Cayley :: m ·- m) where
  act :: m -> (m -> m)
  act = mappend

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.