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.

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.