mirror of
https://github.com/marcosh/crem.git
synced 2024-09-11 12:36:19 +03:00
add Loop constructor to state machines
This commit is contained in:
parent
ca4d6826ad
commit
e096f7d33f
41
decision-log/2023-01-25-loop-constructor.yaml
Normal file
41
decision-log/2023-01-25-loop-constructor.yaml
Normal file
@ -0,0 +1,41 @@
|
||||
name: Add Loop constructor
|
||||
date: 2023-01-25
|
||||
context: >
|
||||
We would like to have machines which are able to feed back their output as
|
||||
input to themselves, if types align correctly.
|
||||
|
||||
One option to do this is to use the `Costrong` instance for machines, or
|
||||
similarly an `ArrowLoop` instance. This would require the use of a `fix`
|
||||
style using `unfirst` or `loop`.
|
||||
|
||||
The other option is adding a new constructor `Loop` to `StateMachine` and use
|
||||
that to loop over the provided machine when the machine is run.
|
||||
In general it does not make much sense to loopa machine of type
|
||||
`StateMachine a a`, since that would mean never stopping.
|
||||
One option to signal the stopping would be to restrict `Loop` only to
|
||||
machines with an output of type `m b`, where `m` admits and instance of
|
||||
`MonadError e m`. This does not work as good as we would like, since we are
|
||||
very much interested in using `m = []` and currently there is no `MonadError`
|
||||
instance for lists.
|
||||
The other option is using directly `Loop` only on machines of type
|
||||
`StateMachine a [a]`. This also makes sense since `StateMachine a b` is
|
||||
isomorphic to `(NonEmpty a) -> b` and then `[a]` could be seen as the sum of
|
||||
the stop case (`[]`) and the continuation case `NonEmpty a`.
|
||||
|
||||
Moreover, adding a new constructor, we could use that information when we
|
||||
need to represent graphically our machines.
|
||||
decision: >
|
||||
For the moment, until we understand more about the categorical setting which
|
||||
underlies the issue, we are going to use
|
||||
|
||||
```
|
||||
Loop :: StateMachine a [a] -> StateMachine a [a]
|
||||
```
|
||||
consequences: >
|
||||
A new `Loop` constructor is added to the `StateMachine` data type.
|
||||
|
||||
For the moment we can compute the topology of a looping machine as transitive
|
||||
closure of the original topology.
|
||||
|
||||
It could be possible in the future to use that information in representing
|
||||
correctly the flow on the machine.
|
9
spec/CRM/Example/PlusOneUpToFour.hs
Normal file
9
spec/CRM/Example/PlusOneUpToFour.hs
Normal file
@ -0,0 +1,9 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
|
||||
module CRM.Example.PlusOneUpToFour where
|
||||
|
||||
import "crm" CRM.StateMachine (StateMachine, stateless)
|
||||
|
||||
plus1UpTo4 :: StateMachine Int [Int]
|
||||
plus1UpTo4 =
|
||||
stateless (\i -> [i + 1 | i < 5])
|
22
spec/CRM/Example/TriangularMachine.hs
Normal file
22
spec/CRM/Example/TriangularMachine.hs
Normal file
@ -0,0 +1,22 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
|
||||
module CRM.Example.TriangularMachine where
|
||||
|
||||
import CRM.BaseMachine (ActionResult (..), InitialState (..))
|
||||
import CRM.StateMachine (StateMachine, unrestrictedMachine)
|
||||
|
||||
data TriangularState (a :: ()) where
|
||||
OnlyState :: Int -> TriangularState '()
|
||||
|
||||
triangular :: StateMachine Int Int
|
||||
triangular =
|
||||
unrestrictedMachine
|
||||
( \case
|
||||
OnlyState state ->
|
||||
\input ->
|
||||
ActionResult
|
||||
(OnlyState $ state + 1)
|
||||
(state + input)
|
||||
)
|
||||
(InitialState (OnlyState 0))
|
@ -18,3 +18,10 @@ spec =
|
||||
, ((1, 'a'), (2, 'b'))
|
||||
, ((1, 'c'), (2, 'd'))
|
||||
]
|
||||
|
||||
describe "transitiveClosureGraph" $ do
|
||||
it "computes correctly the transitive closure of a graph" $
|
||||
do
|
||||
transitiveClosureGraph
|
||||
(Graph [(1 :: Int, 2), (2, 3), (1, 4)])
|
||||
`shouldBe` Graph [(2, 3), (1, 2), (1, 4), (1, 3)]
|
||||
|
@ -2,6 +2,7 @@ module CRM.StateMachineSpec where
|
||||
|
||||
import CRM.Example.BooleanStateMachine (booleanStateMachine)
|
||||
import CRM.Example.LockDoor
|
||||
import CRM.Example.PlusOneUpToFour (plus1UpTo4)
|
||||
import CRM.Example.Switch (switchMachine)
|
||||
import "crm" CRM.StateMachine
|
||||
import "base" Data.List.NonEmpty (NonEmpty, fromList)
|
||||
@ -108,3 +109,12 @@ spec =
|
||||
\input ->
|
||||
nonEmptyFunction input
|
||||
`shouldBe` (cosieve . cotabulate @StateMachine $ nonEmptyFunction) input
|
||||
|
||||
describe "Loop constructor runs correctly" $ do
|
||||
describe "with the plus1UpTo4 machine" $ do
|
||||
it "runs correctly on a single input" $ do
|
||||
run (Loop plus1UpTo4) 1 `shouldOutput` [2, 3, 4, 5]
|
||||
run (Loop plus1UpTo4) 5 `shouldOutput` []
|
||||
|
||||
it "processes correctly multiple inputs" $ do
|
||||
runMultiple (Loop plus1UpTo4) [1, 1] `shouldOutput` [2, 3, 4, 5, 2, 3, 4, 5]
|
||||
|
@ -1,5 +1,7 @@
|
||||
module CRM.Graph where
|
||||
|
||||
import "base" Data.List (nub)
|
||||
|
||||
-- * Graph
|
||||
|
||||
-- | A graph is just a list of edges between vertices of type `a`
|
||||
@ -21,10 +23,30 @@ productGraph (Graph edges1) (Graph edges2) =
|
||||
)
|
||||
<$> [(edge1, edge2) | edge1 <- edges1, edge2 <- edges2]
|
||||
|
||||
-- computes all the possible paths in the input graph and considers them as
|
||||
-- edges.
|
||||
-- Notive that the current implementation is removing duplicates
|
||||
transitiveClosureGraph :: Eq a => Graph a -> Graph a
|
||||
transitiveClosureGraph graph@(Graph edges) =
|
||||
Graph $
|
||||
foldr
|
||||
( \a edgesSoFar ->
|
||||
edgesSoFar <> pathsStartingWith graph a
|
||||
)
|
||||
[]
|
||||
(nub $ fst <$> edges)
|
||||
where
|
||||
pathsStartingWith :: Eq a => Graph a -> a -> [(a, a)]
|
||||
pathsStartingWith graph'@(Graph edges') a =
|
||||
let
|
||||
edgesStartingWithA = filter ((== a) . fst) edges'
|
||||
in
|
||||
edgesStartingWithA <> ((a,) . snd <$> (pathsStartingWith graph' . snd =<< edgesStartingWithA))
|
||||
|
||||
-- * UntypedGraph
|
||||
|
||||
-- A data type to represent a graph which is not tracking the vertex type
|
||||
data UntypedGraph = forall a. (Show a) => UntypedGraph (Graph a)
|
||||
data UntypedGraph = forall a. (Eq a, Show a) => UntypedGraph (Graph a)
|
||||
|
||||
instance Show UntypedGraph where
|
||||
show :: UntypedGraph -> String
|
||||
@ -34,3 +56,8 @@ instance Show UntypedGraph where
|
||||
untypedProductGraph :: UntypedGraph -> UntypedGraph -> UntypedGraph
|
||||
untypedProductGraph (UntypedGraph graph1) (UntypedGraph graph2) =
|
||||
UntypedGraph (productGraph graph1 graph2)
|
||||
|
||||
-- same as `transitiveClosureGraph` but for `UntypedGraph`
|
||||
untypedTransitiveClosureGraph :: UntypedGraph -> UntypedGraph
|
||||
untypedTransitiveClosureGraph (UntypedGraph graph) =
|
||||
UntypedGraph (transitiveClosureGraph graph)
|
||||
|
@ -54,3 +54,5 @@ machineAsGraph (Alternative machine1 machine2) =
|
||||
untypedProductGraph
|
||||
(machineAsGraph machine1)
|
||||
(machineAsGraph machine2)
|
||||
machineAsGraph (Loop machine) =
|
||||
untypedTransitiveClosureGraph (machineAsGraph machine)
|
||||
|
@ -7,7 +7,8 @@ module CRM.StateMachine where
|
||||
import CRM.BaseMachine as BaseMachine
|
||||
import CRM.Topology
|
||||
import "base" Control.Category (Category (..))
|
||||
import "base" Data.Bifunctor (bimap)
|
||||
import "base" Data.Bifunctor (Bifunctor (..), bimap)
|
||||
import "base" Data.Foldable (foldl')
|
||||
import "base" Data.Kind (Type)
|
||||
import "base" Data.List.NonEmpty (NonEmpty (..), fromList)
|
||||
import "profunctors" Data.Profunctor (Choice (..), Costrong (..), Profunctor (..), Strong (..))
|
||||
@ -24,6 +25,7 @@ data StateMachine input output where
|
||||
. ( Demote vertex ~ vertex
|
||||
, SingKind vertex
|
||||
, SingI topology
|
||||
, Eq vertex
|
||||
, Show vertex
|
||||
)
|
||||
=> BaseMachine topology input output
|
||||
@ -40,6 +42,9 @@ data StateMachine input output where
|
||||
:: StateMachine a b
|
||||
-> StateMachine c d
|
||||
-> StateMachine (Either a c) (Either b d)
|
||||
Loop
|
||||
:: StateMachine a [a]
|
||||
-> StateMachine a [a]
|
||||
|
||||
-- | a state machine which does not rely on state
|
||||
stateless :: (a -> b) -> StateMachine a b
|
||||
@ -47,7 +52,12 @@ stateless f = Basic $ statelessBase f
|
||||
|
||||
-- | a machine modelled with explicit state, where every transition is allowed
|
||||
unrestrictedMachine
|
||||
:: (Demote vertex ~ vertex, SingKind vertex, SingI (AllowAllTopology @vertex), Show vertex)
|
||||
:: ( Demote vertex ~ vertex
|
||||
, SingKind vertex
|
||||
, SingI (AllowAllTopology @vertex)
|
||||
, Eq vertex
|
||||
, Show vertex
|
||||
)
|
||||
=> ( forall initialVertex
|
||||
. state initialVertex
|
||||
-> a
|
||||
@ -74,7 +84,6 @@ instance Profunctor StateMachine where
|
||||
lmap f (Compose machine1 machine2) = Compose (lmap f machine1) machine2
|
||||
lmap f machine = Compose (stateless f) machine
|
||||
|
||||
|
||||
rmap :: (b -> c) -> StateMachine a b -> StateMachine a c
|
||||
rmap f (Basic baseMachine) = Basic $ rmap f baseMachine
|
||||
rmap f (Compose machine1 machine2) = Compose machine1 (rmap f machine2)
|
||||
@ -90,6 +99,7 @@ instance Strong StateMachine where
|
||||
second' = Parallel Control.Category.id
|
||||
|
||||
-- * Choice
|
||||
|
||||
-- | An instance of `Choice` allows us to have parallel composition of state machines, meaning that we can pass two inputs to two state machines and get out the outputs of both
|
||||
instance Choice StateMachine where
|
||||
left' :: StateMachine a b -> StateMachine (Either a c) (Either b c)
|
||||
@ -170,3 +180,19 @@ run (Alternative machine1 machine2) a =
|
||||
case a of
|
||||
Left a1 -> bimap Left (`Alternative` machine2) $ run machine1 a1
|
||||
Right a2 -> bimap Right (machine1 `Alternative`) $ run machine2 a2
|
||||
run (Loop machine) a =
|
||||
let
|
||||
(as, machine') = run machine a
|
||||
in
|
||||
first (as <>) $ runMultiple (Loop machine') as
|
||||
|
||||
-- | process multiple inputs in one go, accumulating the results in a monoid
|
||||
runMultiple
|
||||
:: (Foldable f, Monoid b)
|
||||
=> StateMachine a b
|
||||
-> f a
|
||||
-> (b, StateMachine a b)
|
||||
runMultiple machine =
|
||||
foldl'
|
||||
(\(b, machine') -> first (b <>) . run machine')
|
||||
(mempty, machine)
|
||||
|
Loading…
Reference in New Issue
Block a user