mirror of
https://github.com/coot/free-category.git
synced 2024-10-26 15:15:00 +03:00
parent
4ce35b64d8
commit
2cdbb82c09
@ -53,12 +53,14 @@ data State a (st :: StateType) where
|
||||
runLoggedOut :: State a 'LoggedOutType -> Maybe a
|
||||
runLoggedOut (LoggedOut a) = a
|
||||
|
||||
|
||||
-- | Graph of transitions in the state machine. In abstract representation the
|
||||
-- states do not show up, the only way to record some data is to addit to the
|
||||
-- transition. Thus @'Logout'@ can carry data. When interpreted in a some
|
||||
-- states do not show up, the only way to record some data is to add it to the
|
||||
-- transition. Thus @'Logout'@ can carry data. When interpreted in some
|
||||
-- category (e.g. @'Kleisli' m@) then the data will be avalable on
|
||||
-- @'LoggedOut{} :: 'State' a st@.
|
||||
--
|
||||
|
||||
data Tr a from to where
|
||||
Login :: SStateType to -> Tr a (State a 'LoggedOutType) (State a to)
|
||||
Logout :: Maybe a -> Tr a (State a 'LoggedInType) (State a 'LoggedOutType)
|
||||
@ -168,9 +170,8 @@ accessSecret n HandleLogin{handleLogin} = lift $ do
|
||||
|
||||
-- | Get data following the protocol defined by the state machine.
|
||||
--
|
||||
-- Note: in GHC-8.6 we'd need @'MonadFail'@ constraint which prevents from
|
||||
-- running this in @'Identity'@ monad. To avoid this we use @'runLoggedOut'@
|
||||
-- function.
|
||||
-- Note: in GHC-8.6.1 we'd need @'MonadFail'@ which prevents from running this in
|
||||
-- @'Identity'@ monad. To avoid this we use the @'runLoggedOut'@ function.
|
||||
getData
|
||||
:: forall m a . Monad m
|
||||
=> (forall x y. Tr a x y -> Kleisli m x y)
|
||||
@ -183,15 +184,15 @@ getData nat n handleLogin = case foldNatLift nat (accessSecret n handleLogin) of
|
||||
return ma
|
||||
|
||||
-- * Interpreters
|
||||
-- To write an interpret it is enough to supply a natural transformation from
|
||||
-- To write an interpreter it is enough to supply a natural transformation from
|
||||
-- @'Tr' a from to@ to @'Kleisli' m@ for some monad @m@.
|
||||
|
||||
-- | A pure natural transformation from @'Tr'@ to @'Kleisli' m@ for some
|
||||
-- @'Monad' m@. Note, that even though @'Kleisli'@ category seems redundant
|
||||
-- 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 '@FreeEffCat'@ category.
|
||||
-- This is because we will need the monad whn @'foldNatLift'@ will walk over the
|
||||
-- constructors of the '@FreeLifting'@ category.
|
||||
--
|
||||
natPure :: forall m a from to. Monad m => Tr a from to -> Kleisli m from to
|
||||
natPure = liftKleisli . nat
|
||||
|
Loading…
Reference in New Issue
Block a user