1
1
mirror of https://github.com/coot/free-category.git synced 2024-09-11 14:17:30 +03:00

Rename: EffCategory, FreeEffCat

This commit is contained in:
Marcin Szamotulski 2019-01-26 10:44:10 +01:00
parent 7efa4c4430
commit bb0e91b631
No known key found for this signature in database
GPG Key ID: 788D56E52D63FAA4
3 changed files with 33 additions and 31 deletions

View File

@ -23,7 +23,7 @@ import Test.QuickCheck
import Control.Category.Free (Cat)
-- Import classes and combintators used in this example
import Control.Category.Lifting
import Control.Category.FreeEff
{-------------------------------------------------------------------------------
-- Example State Machine, inspired by:
@ -66,16 +66,16 @@ data Tr a from to where
login :: Monad m
=> SStateType st
-> FreeLifting m (Cat (Tr a)) (State a 'LoggedOutType) (State a st)
-> FreeEffCat m (Cat (Tr a)) (State a 'LoggedOutType) (State a st)
login = liftCat . Login
logout :: Monad m
=> Maybe a
-> FreeLifting m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedOutType)
-> FreeEffCat m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedOutType)
logout = liftCat . Logout
access :: Monad m
=> FreeLifting m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedInType)
=> FreeEffCat m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedInType)
access = liftCat Access
type Username = String
@ -149,7 +149,7 @@ accessSecret
-- @'HandleLogin'@ (with a small modifications) but this way we are able to
-- test it with a pure @'HandleLogin'@ (see @'handleLoginPure'@).
-> HandleLogin m String a
-> FreeLifting m (Cat (Tr a)) (State a 'LoggedOutType) (State a 'LoggedOutType)
-> FreeEffCat m (Cat (Tr a)) (State a 'LoggedOutType) (State a 'LoggedOutType)
accessSecret 0 HandleLogin{handleAccessDenied} = lift $ handleAccessDenied $> id
accessSecret n HandleLogin{handleLogin} = lift $ do
st <- handleLogin
@ -159,7 +159,7 @@ accessSecret n HandleLogin{handleLogin} = lift $ do
-- login failure
Left handler' -> return $ accessSecret (pred n) handler'
where
handle :: HandleAccess m a -> Maybe a -> FreeLifting m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedOutType)
handle :: HandleAccess m a -> Maybe a -> FreeEffCat m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedOutType)
handle LogoutHandler ma = logout ma
handle (AccessHandler accessHandler dataHandler) _ = lift $ do
a <- accessHandler
@ -191,7 +191,7 @@ getData nat n handleLogin = case foldNatLift nat (accessSecret n handleLogin) of
-- here, as we don't use the monad in the transformation, we need
-- a transformation into a category that satisfies the @'Lifing'@ constraint.
-- This is bause we will need the monad whn @'foldNatLift'@ will walk over the
-- constructors of '@FreeLifting'@ category.
-- constructors of '@FreeEffCat'@ category.
--
natPure :: forall m a from to. Monad m => Tr a from to -> Kleisli m from to
natPure = liftKleisli . nat

View File

@ -1,5 +1,5 @@
name: free-category
version: 0.0.1.0
version: 0.0.2.0
synopsis: Free category
description: Free categories
category: Algebra, Control, Monads, Category
@ -24,7 +24,7 @@ library
exposed-modules:
Control.Arrow.Free
Control.Category.Free
Control.Category.Lifting
Control.Category.FreeEff
other-modules:
Paths_free_category
hs-source-dirs:

View File

@ -1,7 +1,7 @@
{-# LANGUAGE FunctionalDependencies #-}
module Control.Category.Lifting
( Lifting (..)
, FreeLifting (..)
module Control.Category.FreeEff
( EffCategory (..)
, FreeEffCat (..)
, liftCat
, foldNatLift
, liftKleisli
@ -17,35 +17,37 @@ import Control.Category.Free (Cat (..))
import Control.Algebra.Free2 (FreeAlgebra2 (..))
import Data.Algebra.Free (AlgebraType, AlgebraType0, proof)
-- | Categories which can lift monadic actions.
-- | Categories which can lift monadic actions, i.e. effectful categories.
--
class Category c => Lifting c m | c -> m where
class Category c => EffCategory c m | c -> m where
lift :: m (c a b) -> c a b
instance Monad m => Lifting (Kleisli m) m where
instance Monad m => EffCategory (Kleisli m) m where
lift m = Kleisli (\a -> m >>= \(Kleisli f) -> f a)
instance Lifting (->) Identity where
instance EffCategory (->) Identity where
lift = runIdentity
-- | Category transformer, which adds @'Lifting'@ instance to the underlying
-- base category.
data FreeLifting :: (* -> *) -> (k -> k -> *) -> k -> k -> * where
Base :: c a b -> FreeLifting m c a b
Lift :: m (FreeLifting m c a b) -> FreeLifting m c a b
-- | Category transformer, which adds @'EffCategory'@ instance to the
-- underlying base category.
--
data FreeEffCat :: (* -> *) -> (k -> k -> *) -> k -> k -> * where
Base :: c a b -> FreeEffCat m c a b
Lift :: m (FreeEffCat m c a b) -> FreeEffCat m c a b
instance (Functor m, Category c) => Category (FreeLifting m c) where
instance (Functor m, Category c) => Category (FreeEffCat m c) where
id = Base id
Base f . Base g = Base $ f . g
f . Lift mg = Lift $ (f .) <$> mg
Lift mf . g = Lift $ (. g) <$> mf
instance (Functor m, Category c) => Lifting (FreeLifting m c) m where
instance (Functor m, Category c) => EffCategory (FreeEffCat m c) m where
lift = Lift
type instance AlgebraType0 (FreeLifting m) c = (Monad m, Category c)
type instance AlgebraType (FreeLifting m) c = Lifting c m
instance Monad m => FreeAlgebra2 (FreeLifting m) where
type instance AlgebraType0 (FreeEffCat m) c = (Monad m, Category c)
type instance AlgebraType (FreeEffCat m) c = EffCategory c m
instance Monad m => FreeAlgebra2 (FreeEffCat m) where
liftFree2 = Base
foldNatFree2 nat (Base cab) = nat cab
foldNatFree2 nat (Lift mcab) = lift $ foldNatFree2 nat <$> mcab
@ -54,25 +56,25 @@ instance Monad m => FreeAlgebra2 (FreeLifting m) where
forget2 = proof
-- | Wrap a transition into a free category @'Cat'@ and then in
-- @'FreeLifting'@
-- @'FreeEffCat'@
--
-- prop> liftCat tr = Base (tr :.: Id)
--
liftCat :: Monad m => tr a b -> FreeLifting m (Cat tr) a b
liftCat :: Monad m => tr a b -> FreeEffCat m (Cat tr) a b
liftCat = liftFree2 . liftFree2
-- | Fold @'FreeLifing'@ category based on a free category @'Cat' tr@ using
-- a functor @tr x y -> c x y@.
--
foldNatLift
:: (Monad m, Lifting c m)
:: (Monad m, EffCategory c m)
=> (forall x y. tr x y -> c x y)
-> FreeLifting m (Cat tr) a b
-> FreeEffCat m (Cat tr) a b
-> c a b
foldNatLift nat = foldNatFree2 (foldNatFree2 nat)
-- | Functor from @'->'@ category to @'Kleisli' m@. If @m@ is @Identity@ then
-- it will respect @'lift'@ i.e. @lfitKleisli (lift ar) = lift (liftKleisli <$>
-- it will respect @'lift'@ i.e. @liftKleisli (lift ar) = lift (liftKleisli <$>
-- ar).
--
liftKleisli :: Applicative m => (a -> b) -> Kleisli m a b