This is a quick revision of my past article 多項式Applicative Functorの一般論. Rewritten in English, sum of any applicatives rather than Reader, etc.
Suppose F0, F1, F2, ... are Applicative and F is their sum
data F a = C0 (F0 a) | C1 (F1 a) | C2 (F2 a) | ...Also, suppose F has Applicative instance defined as:
instance Applicative F where
pure a = C0 (pure @F0 a)
Ci x <*> Cj y = C(i<>j) (left i j x <*> right i j y)
where
Applicatives Fi and tags Ci are indexed by (i :: M)
<> is a Monoid operation on M
0 is the unit of <>
left and right are family of Applicative morphisms
left :: (i :: M) -> (j :: M) -> (∀a. F(i) a -> F(i<>j) a)
right :: (i :: M) -> (j :: M) -> (∀a. F(j) a -> F(i<>j) a)By the applicative laws, these conditions on left and right must hold.
(Well, it’s not trivial but teduous calculations)
left i 0 = id :: F(i) ~> F(i<>0)right 0 j = id :: F(j) ~> F(0<>j)left (i <> j) k . left i j = left i (j <> k) :: F(i) ~> F(i<>j<>k)right i (j <> k) . right j k = right (i <> j) k :: F(k) ~> F(i<>j<>k)left (i <> j) k . right i j = right i (j <> k) . left j k :: F(j) ~> F(i<>j<>k)
Let mid be the composition occured in 5.
mid :: ∀i j k :: M -> F(j) ~> F(i <> j <> k)
mid i j k = left (i <> j) k . right i j
-- = right i (j <> k) . left j kThese properties about mid follows from 1-5.
mid 0 i j = left i jmid i j 0 = right i jmid 0 j 0 = idmid i' (i <> j <> k) k' . mid i j k = mid (i' <> i) j (k <> k')
Here, we want to show that if (M,<>,0) was a group not just a monoid, left i j and right i j must be isomorphisms.
It’s equivalent to say mid i j k must be isomorphism.
Since M is a group, i and k have their inverses i⁻¹, k⁻¹ resp.
Then mid i⁻¹ (i <> j <> k) k⁻¹ is the inverse of mid i j k.
mid i⁻¹ (i <> j <> k) k⁻¹ . mid i j k
= mid (i⁻¹ <> i) j (k <> k⁻¹)
= mid 0 j 0
= id
mid i j k . mid i⁻¹ (i <> j <> k) k⁻¹
= mid i (i⁻¹ <> i <> j <> k <> k⁻¹) k . mid i⁻¹ (i <> j <> k) k⁻¹
= mid (i <> i⁻¹) (i <> j <> k) (k⁻¹ <> k)
= mid 0 (i <> j <> k) 0
= id