Continuation of Encoding Overlapping, Extensible Isomorphisms: encoding "open kinds" to better express some awkward type classes.
-
-
Save Icelandjack/865476f2299a4916d4e237d0f8ed0119 to your computer and use it in GitHub Desktop.
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.
Further reading
I want to define an
Applicative
instance forSum
but I run into a problem.In the case of
(<*>)
we are combing twoSum
s:InL
we combine them with(<*>) @f
.InR
we combine them with(<*>) @g
.but what about when they differ? We have no way of transforming between
f a
into ag 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:but we are greeted with a familiar story
with a familiar solution
We can create a newtype of
Sum
with a phantom witness of anApplicative
morphism (this can derive forSum
using-XDerivingVia
since it has the same representation)and this allows us to derive
Sum f Identity
(also known asLift f
)Product of two
Applicative
morphismsReturning to the other example that didn't work with the standard encoding:
Can be easily written as