{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeApplications #-} module Data.Algebra.Free ( -- * Free algebra class FreeAlgebra (..) -- ** Type level witnesses , Proof (..) , -- ** Algebra types \/ constraints AlgebraType , AlgebraType0 -- * Combinators , unFoldMapFree , foldFree , natFree , fmapFree , joinFree , bindFree , cataFree , foldrFree , foldrFree' , foldlFree , foldlFree' -- * General free type , Free (..) , DNonEmpty (..) ) where import Prelude import Data.DList as DList import Data.Functor.Identity (Identity (..)) #if MIN_VERSION_data_fix(0,3,0) import Data.Fix (Fix, foldFix) #else import Data.Fix (Fix, cata) #endif import Data.Group (Group (..)) import Data.Kind (Constraint, Type) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NonEmpty import Data.Monoid (Endo (..), Dual (..)) import Data.Algebra.Pointed (Pointed (..)) -- -- Prerequisites for @'FreeAlgebra'@ -- -- | Type family which for each free algebra @m@ returns a type level lambda -- from types to constraints. It is describe the class of algebras for which -- this free algebra is free. -- -- A lawful instance for this type family must guarantee -- that the constraint @'AlgebraType0' m f@ is implied by the @'AlgebraType' -- m f@ constraint. This guarantees that there exists a forgetful functor from -- the category of types of kind @* -> *@ which satisfy @'AlgebraType' m@ -- constrain to the category of types of kind @* -> *@ which satisfy the -- @'AlgebraType0 m@ constraint. -- type family AlgebraType (f :: k) (a :: l) :: Constraint -- | Type family which limits Hask to its full subcategory which satisfies -- a given constraints. Some free algebras, like free groups, or free abelian -- semigroups have additional constraints on on generators, like @Eq@ or @Ord@. -- type family AlgebraType0 (f :: k) (a :: l) :: Constraint -- | A proof that constraint @c@ holds for type @a@. -- data Proof (c :: Constraint) (a :: l) where Proof :: c => Proof c a -- | A lawful instance has to guarantee that @'unFoldFree'@ is an inverse of -- @'foldMapFree'@ (in the category of algebras of type @'AlgebraType' m@). -- -- This in turn guaranties that @m@ is a left adjoint functor from full -- subcategory of Hask (of types constrained by @'AlgebraType0' m) to algebras -- of type @'AlgebraType' m@. The right adjoint is the forgetful functor. The -- composition of left adjoin and the right one is always a monad, this is why -- we will be able to build monad instance for @m@. -- class FreeAlgebra (m :: Type -> Type) where {-# MINIMAL returnFree, foldMapFree #-} -- | Injective map that embeds generators @a@ into @m@. returnFree :: a -> m a -- | The freeness property. foldMapFree :: forall d a . ( AlgebraType m d , AlgebraType0 m a ) => (a -> d) -- ^ a mapping of generators of @m@ into @d@ -> (m a -> d) -- ^ a homomorphism from @m a@ to @d@ -- | Proof that @AlgebraType0 m a => m a@ is an algebra of type -- @AlgebraType m@. This proves that @m@ is a mapping from the full -- subcategory of @Hask@ of types satisfying @AlgebraType0 m a@ constraint -- to the full subcategory satisfying @AlgebraType m a@, @'fmapFree'@ below -- proves that it's a functor. (@'codom'@ from codomain) -- codom :: forall a. AlgebraType0 m a => Proof (AlgebraType m (m a)) (m a) default codom :: forall a. AlgebraType m (m a) => Proof (AlgebraType m (m a)) (m a) codom = forall {l} (c :: Constraint) (a :: l). c => Proof c a Proof -- | Proof that the forgetful functor from types @a@ satisfying -- @AgelbraType m a@ to @AlgebraType0 m a@ is well defined. -- forget :: forall a. AlgebraType m a => Proof (AlgebraType0 m a) (m a) default forget :: forall a. AlgebraType0 m a => Proof (AlgebraType0 m a) (m a) forget = forall {l} (c :: Constraint) (a :: l). c => Proof c a Proof -- -- Free combinators -- -- | Inverse of @'foldMapFree'@ -- -- It is uniquely determined by its universal property (by Yoneda lemma): -- -- prop> unFoldMapFree id = returnFree -- -- Note that @'unFoldMapFree' id@ is the unit of the -- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the -- adjunction imposed by the @'FreeAlgebra'@ constraint. -- unFoldMapFree :: FreeAlgebra m => (m a -> d) -> (a -> d) unFoldMapFree :: forall (m :: * -> *) a d. FreeAlgebra m => (m a -> d) -> a -> d unFoldMapFree m a -> d f = m a -> d f forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (m :: * -> *) a. FreeAlgebra m => a -> m a returnFree {-# INLINABLE unFoldMapFree #-} -- | All types which satisfy @'FreeAlgebra'@ constraint are foldable. -- -- prop> foldFree . returnFree == id -- -- @foldFree@ is the -- [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of the -- adjunction imposed by @FreeAlgebra@ constraint. -- -- Examples: -- -- > foldFree @[] = foldMap id -- > = foldr (<>) mempty -- > foldFree @NonEmpty -- > = foldr1 (<>) -- -- Note that @foldFree@ replaces the abstract \/ free algebraic operation in -- @m a@ to concrete one in @a@. -- foldFree :: forall m a . ( FreeAlgebra m , AlgebraType m a ) => m a -> a foldFree :: forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType m a) => m a -> a foldFree m a ma = case forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType m a) => Proof (AlgebraType0 m a) (m a) forget @m @a of Proof (AlgebraType0 m a) (m a) Proof -> forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree forall a. a -> a id m a ma {-# INLINABLE foldFree #-} -- | The canonical quotient map from a free algebra of a wider class to a free -- algebra of a narrower class, e.g. from a free semigroup to -- free monoid, or from a free monoid to free commutative monoid, -- etc. -- -- prop> natFree . natFree == natFree -- prop> fmapFree f . natFree == hoistFree . fmapFree f -- -- the constraints: -- * the algebra @n a@ is of the same type as algebra @m@ (this is -- always true, just GHC cannot prove it here) -- * @m@ is a free algebra generated by @a@ -- * @n@ is a free algebra generated by @a@ -- natFree :: forall m n a . ( FreeAlgebra m , FreeAlgebra n , AlgebraType0 m a , AlgebraType m (n a) ) => m a -> n a natFree :: forall (m :: * -> *) (n :: * -> *) a. (FreeAlgebra m, FreeAlgebra n, AlgebraType0 m a, AlgebraType m (n a)) => m a -> n a natFree = forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree forall (m :: * -> *) a. FreeAlgebra m => a -> m a returnFree {-# INLINABLE natFree #-} -- | All types which satisfy @'FreeAlgebra'@ constraint are functors. The -- constraint @'AlgebraType' m (m b)@ is always satisfied. -- fmapFree :: forall m a b . ( FreeAlgebra m , AlgebraType0 m a , AlgebraType0 m b ) => (a -> b) -> m a -> m b fmapFree :: forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => (a -> b) -> m a -> m b fmapFree a -> b f m a ma = case forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType0 m a) => Proof (AlgebraType m (m a)) (m a) codom @m @b of Proof (AlgebraType m (m b)) (m b) Proof -> forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree (forall (m :: * -> *) a. FreeAlgebra m => a -> m a returnFree forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> b f) m a ma {-# INLINABLE fmapFree #-} -- | @'FreeAlgebra'@ constraint implies @Monad@ constrain. -- joinFree :: forall m a . ( FreeAlgebra m , AlgebraType0 m a ) => m (m a) -> m a joinFree :: forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType0 m a) => m (m a) -> m a joinFree m (m a) mma = case forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType0 m a) => Proof (AlgebraType m (m a)) (m a) codom @m @a of Proof (AlgebraType m (m a)) (m a) Proof -> forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType m a) => m a -> a foldFree m (m a) mma {-# INLINABLE joinFree #-} -- | The monadic @'bind'@ operator. @'returnFree'@ is the corresponding -- @'return'@ for this monad. This just @'foldMapFree'@ in disguise. -- bindFree :: forall m a b . ( FreeAlgebra m , AlgebraType0 m a , AlgebraType0 m b ) => m a -> (a -> m b) -> m b bindFree :: forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType0 m a, AlgebraType0 m b) => m a -> (a -> m b) -> m b bindFree m a ma a -> m b f = case forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType0 m a) => Proof (AlgebraType m (m a)) (m a) codom @m @b of Proof (AlgebraType m (m b)) (m b) Proof -> forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree a -> m b f m a ma {-# INLINABLE bindFree #-} -- | @'Fix' m@ is the initial algebra in the category of algebras of type -- @'AlgebraType' m@ (the initial algebra is a free algebra generated by empty -- set of generators, e.g. the @Void@ type). -- -- Another way of putting this is observing that @'Fix' m@ is isomorphic to @m -- Void@ where @m@ is the /free algebra/. This isomorphisms is given by -- @ -- fixToFree :: (FreeAlgebra m, AlgebraType m (m Void), Functor m) => Fix m -> m Void -- fixToFree = cataFree -- @ -- For monoids the inverse is given by @'Data.Fix.ana' (\_ -> [])@. -- cataFree :: ( FreeAlgebra m , AlgebraType m a , Functor m ) => Fix m -> a #if MIN_VERSION_data_fix(0,3,0) cataFree :: forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType m a, Functor m) => Fix m -> a cataFree = forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a foldFix forall (m :: * -> *) a. (FreeAlgebra m, AlgebraType m a) => m a -> a foldFree #else cataFree = cata foldFree #endif -- | A version of @'Data.Foldable.foldr'@, e.g. it can specialize to -- -- * @foldrFree \@[] :: (a -> b -> b) -> [a] -> b -> b@ -- * @foldrFree \@'Data.List.NonEmpty.NonEmpty' :: (a -> b -> b) -> 'Data.List.NonEmpty.NonEmpty' a -> b -> b@ -- foldrFree :: forall m a b . ( FreeAlgebra m , AlgebraType m (Endo b) , AlgebraType0 m a ) => (a -> b -> b) -> b -> m a -> b foldrFree :: forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType m (Endo b), AlgebraType0 m a) => (a -> b -> b) -> b -> m a -> b foldrFree a -> b -> b f b z m a t = forall a. Endo a -> a -> a appEndo (forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree (forall a. (a -> a) -> Endo a Endo forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> b -> b f) m a t) b z -- | Like @'foldrFree'@ but strict. -- foldrFree' :: forall m a b . ( FreeAlgebra m , AlgebraType m (Dual (Endo (b -> b))) , AlgebraType0 m a ) => (a -> b -> b) -> m a -> b -> b foldrFree' :: forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType m (Dual (Endo (b -> b))), AlgebraType0 m a) => (a -> b -> b) -> m a -> b -> b foldrFree' a -> b -> b f m a xs b z0 = forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType m (Dual (Endo b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b foldlFree (b -> b) -> a -> b -> b f' forall a. a -> a id m a xs b z0 where f' :: (b -> b) -> a -> b -> b f' b -> b k a x b z = b -> b k forall a b. (a -> b) -> a -> b $! a -> b -> b f a x b z -- | Generalizes @'Data.Foldable.foldl'@, e.g. it can specialize to -- -- * @foldlFree \@[] :: (b -> a -> b) -> b -> [a] -> b@ -- * @foldlFree \@'Data.List.NonEmpty.NonEmpty' :: (b -> a -> b) -> b -> 'Data.List.NonEmpty.NonEmpty' a -> b@ -- foldlFree :: forall m a b . ( FreeAlgebra m , AlgebraType m (Dual (Endo b)) , AlgebraType0 m a ) => (b -> a -> b) -> b -> m a -> b foldlFree :: forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType m (Dual (Endo b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b foldlFree b -> a -> b f b z m a t = forall a. Endo a -> a -> a appEndo (forall a. Dual a -> a getDual (forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree (forall a. a -> Dual a Dual forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. (a -> a) -> Endo a Endo forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a b c. (a -> b -> c) -> b -> a -> c flip b -> a -> b f) m a t)) b z -- | Like @'foldlFree'@ but strict. -- foldlFree' :: forall m a b . ( FreeAlgebra m , AlgebraType m (Endo (b -> b)) , AlgebraType0 m a ) => (b -> a -> b) -> b -> m a -> b foldlFree' :: forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType m (Endo (b -> b)), AlgebraType0 m a) => (b -> a -> b) -> b -> m a -> b foldlFree' b -> a -> b f b z0 m a xs = forall (m :: * -> *) a b. (FreeAlgebra m, AlgebraType m (Endo b), AlgebraType0 m a) => (a -> b -> b) -> b -> m a -> b foldrFree a -> (b -> b) -> b -> b f' forall a. a -> a id m a xs b z0 where f' :: a -> (b -> b) -> b -> b f' a x b -> b k b z = b -> b k forall a b. (a -> b) -> a -> b $! b -> a -> b f b z a x -- -- Instances -- type instance AlgebraType0 Identity a = () type instance AlgebraType Identity a = () instance FreeAlgebra Identity where returnFree :: forall a. a -> Identity a returnFree = forall a. a -> Identity a Identity foldMapFree :: forall d a. (AlgebraType Identity d, AlgebraType0 Identity a) => (a -> d) -> Identity a -> d foldMapFree a -> d f = a -> d f forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. Identity a -> a runIdentity type instance AlgebraType0 NonEmpty a = () type instance AlgebraType NonEmpty m = Semigroup m -- | @'NonEmpty'@ is the free semigroup in the class of semigroup which are -- strict in the left argument. -- instance FreeAlgebra NonEmpty where returnFree :: forall a. a -> NonEmpty a returnFree a a = a a forall a. a -> [a] -> NonEmpty a :| [] -- @'foldMap'@ requires @'Monoid' d@ constraint which we don't need to -- satisfy here foldMapFree :: forall d a. (AlgebraType NonEmpty d, AlgebraType0 NonEmpty a) => (a -> d) -> NonEmpty a -> d foldMapFree a -> d f (a a :| []) = a -> d f a a foldMapFree a -> d f (a a :| (a b : [a] bs)) = a -> d f a a forall a. Semigroup a => a -> a -> a <> forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree a -> d f (a b forall a. a -> [a] -> NonEmpty a :| [a] bs) -- | 'DNonEmpty' is the free semigroup in the class of all semigroups. -- newtype DNonEmpty a = DNonEmpty ([a] -> NonEmpty a) instance Semigroup (DNonEmpty a) where DNonEmpty [a] -> NonEmpty a f <> :: DNonEmpty a -> DNonEmpty a -> DNonEmpty a <> DNonEmpty [a] -> NonEmpty a g = forall a. ([a] -> NonEmpty a) -> DNonEmpty a DNonEmpty ([a] -> NonEmpty a f forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. NonEmpty a -> [a] NonEmpty.toList forall b c a. (b -> c) -> (a -> b) -> a -> c . [a] -> NonEmpty a g) type instance AlgebraType0 DNonEmpty a = () type instance AlgebraType DNonEmpty m = Semigroup m instance FreeAlgebra DNonEmpty where returnFree :: forall a. a -> DNonEmpty a returnFree a a = forall a. ([a] -> NonEmpty a) -> DNonEmpty a DNonEmpty (a a forall a. a -> [a] -> NonEmpty a :|) foldMapFree :: forall d a. (AlgebraType DNonEmpty d, AlgebraType0 DNonEmpty a) => (a -> d) -> DNonEmpty a -> d foldMapFree a -> d f (DNonEmpty [a] -> NonEmpty a g) = forall (m :: * -> *) d a. (FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) => (a -> d) -> m a -> d foldMapFree a -> d f ([a] -> NonEmpty a g []) type instance AlgebraType0 [] a = () type instance AlgebraType [] m = Monoid m -- | Note that @'[]'@ is a free monoid only for monoids which multiplication is -- strict in the left argument -- [ref](http://comonad.com/reader/2015/free-monoids-in-haskell/). Note that -- being strict adds additional equation to the monoid laws: -- -- prop> undefined <> a = undefined -- -- Thus, expectedly we get an equational theory for left / right / two-sided -- strict monoids. -- -- Snoc lists are free monoids in the class of monoids which are strict in the -- right argument, @'Free' Monoid@ and @'DList' are free in the class of all -- Haskell monoids. -- instance FreeAlgebra [] where returnFree :: forall a. a -> [a] returnFree a a = [a a] foldMapFree :: forall d a. (AlgebraType [] d, AlgebraType0 [] a) => (a -> d) -> [a] -> d foldMapFree = forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap type instance AlgebraType0 Maybe a = () type instance AlgebraType Maybe m = Pointed m instance FreeAlgebra Maybe where returnFree :: forall a. a -> Maybe a returnFree = forall a. a -> Maybe a Just foldMapFree :: forall d a. (AlgebraType Maybe d, AlgebraType0 Maybe a) => (a -> d) -> Maybe a -> d foldMapFree a -> d _ Maybe a Nothing = forall p. Pointed p => p point foldMapFree a -> d f (Just a a) = a -> d f a a -- | @'Free' c a@ represents free algebra for a constraint @c@ generated by -- type @a@. -- newtype Free (c :: Type -> Constraint) a = Free { forall (c :: * -> Constraint) a. Free c a -> forall r. c r => (a -> r) -> r runFree :: forall r. c r => (a -> r) -> r } instance Semigroup (Free Semigroup a) where Free forall r. Semigroup r => (a -> r) -> r f <> :: Free Semigroup a -> Free Semigroup a -> Free Semigroup a <> Free forall r. Semigroup r => (a -> r) -> r g = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free forall a b. (a -> b) -> a -> b $ \a -> r k -> forall r. Semigroup r => (a -> r) -> r f a -> r k forall a. Semigroup a => a -> a -> a <> forall r. Semigroup r => (a -> r) -> r g a -> r k type instance AlgebraType0 (Free Semigroup) a = () type instance AlgebraType (Free Semigroup) a = Semigroup a instance FreeAlgebra (Free Semigroup) where returnFree :: forall a. a -> Free Semigroup a returnFree a a = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free forall a b. (a -> b) -> a -> b $ \a -> r k -> a -> r k a a foldMapFree :: forall d a. (AlgebraType (Free Semigroup) d, AlgebraType0 (Free Semigroup) a) => (a -> d) -> Free Semigroup a -> d foldMapFree a -> d f (Free forall r. Semigroup r => (a -> r) -> r k) = forall r. Semigroup r => (a -> r) -> r k a -> d f instance Semigroup (Free Monoid a) where Free forall r. Monoid r => (a -> r) -> r f <> :: Free Monoid a -> Free Monoid a -> Free Monoid a <> Free forall r. Monoid r => (a -> r) -> r g = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free forall a b. (a -> b) -> a -> b $ \a -> r k -> forall r. Monoid r => (a -> r) -> r f a -> r k forall a. Monoid a => a -> a -> a `mappend` forall r. Monoid r => (a -> r) -> r g a -> r k instance Monoid (Free Monoid a) where mempty :: Free Monoid a mempty = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free (forall a b. a -> b -> a const forall a. Monoid a => a mempty) #if __GLASGOW_HASKELL__ <= 802 mappend = (<>) #endif type instance AlgebraType0 (Free Monoid) a = () type instance AlgebraType (Free Monoid) a = Monoid a instance FreeAlgebra (Free Monoid) where returnFree :: forall a. a -> Free Monoid a returnFree a a = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free forall a b. (a -> b) -> a -> b $ \a -> r k -> a -> r k a a foldMapFree :: forall d a. (AlgebraType (Free Monoid) d, AlgebraType0 (Free Monoid) a) => (a -> d) -> Free Monoid a -> d foldMapFree a -> d f (Free forall r. Monoid r => (a -> r) -> r k) = forall r. Monoid r => (a -> r) -> r k a -> d f type instance AlgebraType0 DList a = () type instance AlgebraType DList a = Monoid a -- | @'DList'@ is isomorphic to @'Free' Monoid@; it is free in the class of all -- monoids. -- instance FreeAlgebra DList where returnFree :: forall a. a -> DList a returnFree = forall a. a -> DList a DList.singleton foldMapFree :: forall d a. (AlgebraType DList d, AlgebraType0 DList a) => (a -> d) -> DList a -> d foldMapFree = forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap instance Semigroup (Free Group a) where Free forall r. Group r => (a -> r) -> r f <> :: Free Group a -> Free Group a -> Free Group a <> Free forall r. Group r => (a -> r) -> r g = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free forall a b. (a -> b) -> a -> b $ \a -> r k -> forall r. Group r => (a -> r) -> r f a -> r k forall a. Monoid a => a -> a -> a `mappend` forall r. Group r => (a -> r) -> r g a -> r k instance Monoid (Free Group a) where mempty :: Free Group a mempty = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free (forall a b. a -> b -> a const forall a. Monoid a => a mempty) #if __GLASGOW_HASKELL__ <= 802 mappend = (<>) #endif instance Group (Free Group a) where invert :: Free Group a -> Free Group a invert (Free forall r. Group r => (a -> r) -> r k) = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free (forall r. Group r => (a -> r) -> r k forall b c a. (b -> c) -> (a -> b) -> a -> c . forall m. Group m => m -> m invert) type instance AlgebraType0 (Free Group) a = () type instance AlgebraType (Free Group) a = Group a instance FreeAlgebra (Free Group) where returnFree :: forall a. a -> Free Group a returnFree a a = forall (c :: * -> Constraint) a. (forall r. c r => (a -> r) -> r) -> Free c a Free forall a b. (a -> b) -> a -> b $ \a -> r k -> a -> r k a a foldMapFree :: forall d a. (AlgebraType (Free Group) d, AlgebraType0 (Free Group) a) => (a -> d) -> Free Group a -> d foldMapFree a -> d f (Free forall r. Group r => (a -> r) -> r k) = forall r. Group r => (a -> r) -> r k a -> d f