{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
-- | A type class for free objects of kind @k -> k -> Type@, i.e. /graphs/ (we
-- will use this name for types of this kind in this documentation). Examples
-- include various flavors of /free categories/ and /arrows/ which
-- are not included in this package, see
-- __[free-category](https://hackage.haskell.org/package/free-category)__ on
-- /Hackage/).
--
module Control.Algebra.Free2
( -- * Free algebra class
FreeAlgebra2 (..)
-- ** Type level witnesses
, Proof (..)
-- ** Algebra types \/ constraints
, AlgebraType0
, AlgebraType
-- * Combinators
, wrapFree2
, foldFree2
, unFoldNatFree2
, hoistFree2
, hoistFreeH2
, joinFree2
, bindFree2
, assocFree2
) where
import Control.Monad (join)
import Data.Kind (Type)
import Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..))
-- | Free algebra class similar to @'FreeAlgebra1'@ and @'FreeAlgebra'@, but
-- for types of kind @k -> k -> Type@.
--
class FreeAlgebra2 (m :: (k -> k -> Type) -> k -> k -> Type) where
{-# MINIMAL liftFree2, foldNatFree2 #-}
-- | Lift a graph @f@ satsifying the constraint @'AlgebraType0'@ to a free
-- its object @m f@.
--
liftFree2 :: AlgebraType0 m f
=> f a b
-> m f a b
-- | This represents the theorem that @m f@ is indeed free object (as
-- in propositions as types). The types of kind @k -> k -> Type@ form
-- a category, where an arrow from @f :: k -> k -> Type@ to @d :: k ->
-- k -> Type@ is represented by type @forall x y. f x y -> d x y@.
-- @foldNatFree2@ states that whenever we have such a morphism and @d@
-- satisfies the constraint @AlgebraType m d@ then we can construct
-- a morphism from @m f@ to @d@.
--
-- prop> foldNatFree2 nat (liftFree2 tr) = nat tr
-- prop> foldNatFree2 nat . foldNatFree2 nat' = foldNatFree2 (foldNatFree2 nat . nat')
--
foldNatFree2 :: forall (d :: k -> k -> Type)
(f :: k -> k -> Type) a b .
( AlgebraType m d
, AlgebraType0 m f
)
=> (forall x y. f x y -> d x y)
-> (m f a b -> d a b)
-- | A proof that for each @f@ satisfying @AlgebraType0 m f@, @m f@
-- satisfies @AlgebraType m (m f)@ constrant. This means that @m@ is
-- a well defined /functor/ from the full sub-category of types of kind @k
-- -> k -> Type@ which satisfy the @AlgebraType0 m@ constraint to the full
-- subcategory of types of the same kind which satifsfy the constraint
-- @AlgebraType m@.
--
codom2 :: forall (f :: k -> k -> Type).
AlgebraType0 m f
=> Proof (AlgebraType m (m f)) (m f)
default codom2 :: forall a. AlgebraType m (m a)
=> Proof (AlgebraType m (m a)) (m a)
codom2 = Proof
-- | A proof that each type @f :: k -> k -> Type@ satisfying the @Algebra
-- m f@ constraint also satisfies @AlgebraType0 m f@. This states that
-- there is a well defined /forgetful functor/ from the category of types
-- of kind @k -> k -> Type@ which satisfy the @AlgebraType m@ to the
-- category of types of the same kind which satisfy the @AlgebraType0 m@
-- constraint.
--
forget2 :: forall (f :: k -> k -> Type).
AlgebraType m f
=> Proof (AlgebraType0 m f) (m f)
default forget2 :: forall a. AlgebraType0 m a
=> Proof (AlgebraType0 m a) (m a)
forget2 = Proof
-- Combinators
--
-- | Version of @wrap@ from @free@ package but for graphs.
--
wrapFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type)
(f :: Type -> Type -> Type)
a b .
( AlgebraType0 m f
, FreeAlgebra2 m
, Monad (m f a)
)
=> f a (m f a b)
-> m f a b
wrapFree2 = join . liftFree2
{-# INLINABLE wrapFree2 #-}
-- | Like @'foldFree'@ or @'foldFree1'@ but for graphs.
--
-- A lawful instance will satisfy:
--
-- @
-- 'foldFree2' . 'liftFree2' == 'id' :: f a b -> f a b
-- @
--
-- It is the [unit](https://ncatlab.org/nlab/show/unit+of+an+adjunction) of
-- adjuction defined by @'FreeAlgebra1'@ class.
--
foldFree2 :: forall k
(m :: (k -> k -> Type) -> k -> k -> Type)
(f :: k -> k -> Type)
a b .
( FreeAlgebra2 m
, AlgebraType m f
)
=> m f a b
-> f a b
foldFree2 = case forget2 :: Proof (AlgebraType0 m f) (m f) of
Proof -> foldNatFree2 id
{-# INLINABLE foldFree2 #-}
-- | Inverse of @'foldNatFree2'@.
--
-- It is uniquelly determined by its universal property (by Yonneda lemma):
--
-- prop> unFoldNatFree id = liftFree2
--
unFoldNatFree2
:: forall k
(m :: (k -> k -> Type) -> k -> k -> Type)
(f :: k -> k -> Type)
d a b.
( FreeAlgebra2 m
, AlgebraType0 m f
)
=> (forall x y. m f x y -> d x y)
-> f a b -> d a b
unFoldNatFree2 nat = nat . liftFree2
{-# INLINABLE unFoldNatFree2 #-}
-- | Hoist the underlying graph in the free structure. This is a higher
-- version of a functor (analogous to @'fmapFree'@, which defined functor
-- instance for @'FreeAlgebra'@ instances) and it satisfies the functor laws:
--
-- prop> hoistFree2 id = id
-- prop> hoistFree2 f . hoistFree2 g = hoistFree2 (f . g)
--
hoistFree2 :: forall k
(m :: (k -> k -> Type) -> k -> k -> Type)
(f :: k -> k -> Type)
g a b .
( FreeAlgebra2 m
, AlgebraType0 m g
, AlgebraType0 m f
)
=> (forall x y. f x y -> g x y)
-> m f a b
-> m g a b
hoistFree2 nat = case codom2 :: Proof (AlgebraType m (m g)) (m g) of
Proof -> foldNatFree2 (liftFree2 . nat)
{-# INLINABLE [1] hoistFree2 #-}
{-# RULES
"hositFree2/foldNatFree2"
forall (nat :: forall x y. g x y -> c x y)
(nat0 :: forall x y. f x y -> g x y)
(f :: m f a b).
foldNatFree2 nat (hoistFree2 nat0 f) = foldNatFree2 (nat . nat0) f
#-}
-- | Hoist the top level free structure.
--
hoistFreeH2 :: forall m n f a b .
( FreeAlgebra2 m
, FreeAlgebra2 n
, AlgebraType0 m f
, AlgebraType0 n f
, AlgebraType m (n f)
)
=> m f a b
-> n f a b
hoistFreeH2 = foldNatFree2 liftFree2
{-# INLINABLE [1] hoistFreeH2 #-}
{-# RULES
"hoistFreeH2/foldNatFree2" forall (nat :: forall x y. f x y -> c x y)
(f :: AlgebraType m c => m f a b).
foldNatFree2 nat (hoistFreeH2 f) = foldNatFree2 nat f
#-}
-- | 'FreeAlgebra2' m@ is a monad on some subcategory of graphs (types of kind
-- @k -> k -> 'Type'@), 'joinFree' it is the 'join' of this monad.
--
-- prop> foldNatFree2 nat . joinFree2 = foldNatFree2 (foldNatFree2 nat)
--
-- This property is analogous to @foldMap f . concat = foldMap (foldMap f)@,
--
joinFree2 :: forall k
(m :: (k -> k -> Type) -> k -> k -> Type)
(f :: k -> k -> Type)
a b .
( FreeAlgebra2 m
, AlgebraType0 m f
)
=> m (m f) a b
-> m f a b
joinFree2 = case codom2 :: Proof (AlgebraType m (m f)) (m f) of
Proof -> case forget2 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
Proof -> foldFree2
{-# INLINABLE joinFree2 #-}
-- | @bind@ of the monad defined by @m@ on the subcategory of graphs (types of
-- kind @k -> k -> Type@).
--
-- prop> foldNatFree2 nat (bindFree mf nat') = foldNatFree2 (foldNatFree2 nat . nat') mf
--
bindFree2 :: forall m f g a b .
( FreeAlgebra2 m
, AlgebraType0 m g
, AlgebraType0 m f
)
=> m f a b
-> (forall x y . f x y -> m g x y)
-> m g a b
bindFree2 mfa nat = case codom2 :: Proof (AlgebraType m (m g)) (m g) of
Proof -> foldNatFree2 nat mfa
{-# INLINABLE bindFree2 #-}
assocFree2 :: forall (m :: (Type -> Type -> Type) -> Type -> Type -> Type)
(f :: Type -> Type -> Type)
a b .
( FreeAlgebra2 m
, AlgebraType m f
, Functor (m (m f) a)
)
=> m f a (m f a b)
-> m (m f) a (f a b)
assocFree2 = case forget2 :: Proof (AlgebraType0 m f) (m f) of
Proof -> case codom2 :: Proof (AlgebraType m (m f)) (m f) of
Proof -> case forget2 :: Proof (AlgebraType0 m (m f)) (m (m f)) of
Proof -> case codom2 :: Proof (AlgebraType m (m (m f))) (m (m f)) of
Proof -> fmap foldFree2 . foldNatFree2 (hoistFree2 liftFree2 . liftFree2)
{-# INLINABLE assocFree2 #-}