{- | Free groups * https://en.wikipedia.org/wiki/Free_group * https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem -} module Data.Group.Free ( FreeGroup , fromList , toList , normalize ) where import Control.Monad (ap) import Data.Constraint (Dict (..)) import Data.Group (Group (..)) import Data.Semigroup (Semigroup (..)) import Data.Algebra.Free ( AlgebraType , AlgebraType0 , FreeAlgebra (..) , Proof (..) ) -- | -- Free group generated by a type @a@. Internally it's represented by a list -- @[Either a a]@ where inverse is given by: -- -- @ -- inverse (FreeGroup [a]) = FreeGroup [either Right Left a] -- @ -- -- It is a monad on a full subcategory of @Hask@ which constists of types which -- satisfy the @'Eq'@ constraint. newtype FreeGroup a = FreeGroup { runFreeGroup :: [Either a a] } deriving (Show, Eq, Ord) instance Functor FreeGroup where fmap f (FreeGroup as) = FreeGroup \$ map (either (Left . f) (Right . f)) as instance Applicative FreeGroup where pure = returnFree (<*>) = ap instance Monad FreeGroup where return a = FreeGroup [Right a] FreeGroup as >>= f = FreeGroup \$ concatMap (runFreeGroup . either f f) as -- | -- Normalize a list, i.e. remove adjusten inverses from a word, i.e. -- @ab⁻¹ba⁻¹c = c@ -- -- Complexity: @O(n)@ normalize :: Eq a => [Either a a] -> [Either a a] normalize (Left a : Right b : bs) | a == b = normalize bs | otherwise = case normalize (Right b : bs) of Right b' : bs' | a == b' -> bs' | otherwise -> Left a : Right b' : bs' bs' -> Left a : bs' normalize (Right a : Left b : bs) | a == b = normalize bs | otherwise = case normalize (Left b : bs) of Left b' : bs' | a == b' -> bs' | otherwise -> Right a : Left b' : bs' bs' -> Right a : bs' normalize (a : as) = case normalize as of a' : as' | either Right Left a == a' -> as' | otherwise -> a : a' : as' [] -> [a] normalize [] = [] -- | -- Smart constructor which normalizes a list. fromList :: Eq a => [Either a a] -> FreeGroup a fromList = FreeGroup . normalize toList :: FreeGroup a -> [Either a a] toList = runFreeGroup instance Eq a => Semigroup (FreeGroup a) where FreeGroup as <> FreeGroup bs = FreeGroup \$ normalize (as ++ bs) instance Eq a => Monoid (FreeGroup a) where mempty = FreeGroup [] instance Eq a => Group (FreeGroup a) where invert (FreeGroup as) = FreeGroup \$ foldl (\acu a -> either Right Left a : acu) [] as type instance AlgebraType0 FreeGroup a = Eq a type instance AlgebraType FreeGroup g = (Eq g, Group g) instance FreeAlgebra FreeGroup where returnFree a = FreeGroup [Right a] foldMapFree _ (FreeGroup []) = mempty foldMapFree f (FreeGroup (a : as)) = either (invert . f) f a <> foldMapFree f (FreeGroup as) proof = Proof Dict forget = Proof Dict