§ Practical example of semidirect product

-- | represents a string with indexes into it.
type IndexedString = (String , [Nat])

• If we combine the strings together as t = s1 + s2, how do the indexes of s1, s2 change to become an index of t?

instance Semigroup IndexedString where
  (IndexedString s1 ixs1) <> (IndexedString s2 ixs2) =
    (s1 <> s2, ix1 <> ((+) (length s1)) <$>  ixs2)

• See that we "twist" the indexes of the second by the length of the string. Because we are sticking the "origin" of the second to the "tip" of the first, we need to change the indexes to point to the "new" origin.
• One can check that this is going to be a semidirect product.
• In general, if we have data, pointers into the data, and ways to combine the data, then the bundled up abstraction of (data+pointers into data) should have a semidirect structure.