marcosh/crem
1
1
Fork 0
mirror of https://github.com/marcosh/crem.git synced 2024-09-11 12:36:19 +03:00
Code Issues Packages Projects Releases Wiki Activity

complete documentation on how to create a machine

Browse Source
This commit is contained in:
Marco Perone 2023-01-31 17:22:10 +01:00 committed by Marco Perone
parent 9ad45158fb
commit 478e907b33
1 changed files with 215 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

230
docs/how-to-create-a-machine.md
View File

@ -6,20 +6,22 @@ We will represent a machine as such
```
a ┌────┐ b
──┤ ├──
──┤ ├─>
└────┘
```
as black boxes, where inputs are on the left and outputs are on the right.
The `StateMachine a b` data type has four constructors which we can use to construct a machine:
The `StateMachine a b` data type has six constructors which we can use to construct a machine:
- `Basic`
- `Compose`
- `Parallel`
- `Alternative`
- `Feedback`
- `Kleisli`
Let's start with the last three.
Let's start with the last five.
## `Compose`
@ -34,7 +36,7 @@ allows us to sequentially compose two machines
```
a ┌────┐ b b ┌────┐ c
──┤ ├── ──┤ ├──
──┤ ├─> ──┤ ├─>
└────┘ └────┘
```
@ -43,7 +45,7 @@ to get a single machine
```
┌─────────────────┐
a │ ┌╌╌╌╌┐ b ┌╌╌╌╌┐ │ c
──┼╌┤ ├╌╌╌┤ ├╌┼──
──┼╌┤ ├╌>╌┤ ├╌┼─>
│ └╌╌╌╌┘ └╌╌╌╌┘ │
└─────────────────┘
```
@ -63,10 +65,10 @@ allows us to execute two machines in parallel
```
a ┌────┐ b
──┤ ├──
──┤ ├─>
└────┘
c ┌────┐ d
──┤ ├──
──┤ ├─>
└────┘
```
@ -75,11 +77,11 @@ to get a single machine
```
┌────────────┐
│ a ┌╌╌╌╌┐ b │
│┌╌╌┤ ├╌╌┐│
│┌╌╌┤ ├╌>┐│
(a, c) ││ └╌╌╌╌┘ ││ (b, d)
───────┼┤ ├┼───────
───────┼┤ ├┼──────>
││ ┌╌╌╌╌┐ ││
│└╌╌┤ ├╌╌┘│
│└╌╌┤ ├╌>┘│
│ c └╌╌╌╌┘ d │
└────────────┘
```
@ -101,10 +103,10 @@ If we have two machines
```
a ┌────┐ b
──┤ ├──
──┤ ├─>
└────┘
c ┌────┐ d
──┤ ├──
──┤ ├─>
└────┘
```
@ -113,11 +115,11 @@ we can compose them like so
```
┌────────────┐
│ a ┌╌╌╌╌┐ b │
│┌╌╌┤ ├╌╌┐│
│┌╌╌┤ ├╌>┐│
Either a c ││ └╌╌╌╌┘ ││ Either b d
───────────┼┤ ⊕ ├┼───────────
───────────┼┤ ⊕ ├┼──────────>
││ ┌╌╌╌╌┐ ││
│└╌╌┤ ├╌╌┘│
│└╌╌┤ ├╌>┘│
│ c └╌╌╌╌┘ d │
└────────────┘
```
@ -127,6 +129,78 @@ where the `⊕` symbol allows us to distinguish alternative composition from the
In practice, if the composed machine receives a `Left a` as input, the `a` will be passed as input to the first machine that will emit a `b`, which will be wrapped to emit a `Left b` from the composed machine, while the second machine remains untouched.
Similarly, if the composed machine receives a `Right c` as input, the `c` will be passed as input to the second machine that will emit a `d`, which will be wrapped to emit a `Right d` from the composed machine, while the first machine remains untouched.
## `Feedback`
```haskell
Feedback
:: StateMachine a [b]
-> StateMachine b [a]
-> StateMachine a [b]
```
allows us to use a machine to compute some new input to be processed from the output of a given machine.
If we have two machines
```
a ┌────┐ [b]
──┤ ├──>>
└────┘
[a] ┌────┐ b
<<──┤ ├──
└────┘
```
We can compose them like so
```
┌────────────────┐
a │ a ┌╌╌╌╌┐ [b] │ [b]
──┼┬╌╌╌╌┤ ├╌╌>>┬┼──>>
││ └╌╌╌╌┘ ││
││ [a] ┌╌╌╌╌┐ b ││
│└╌<<╌╌┤ ├╌╌╌┘│
│ └╌╌╌╌┘ │
└────────────────┘
```
It works as follows. When an input `a` is received by the input machine, it is processed by the first machine to obtain a list of output `bs :: [b]`. These outputs as fed as inputs into the second machine one by one, obtaining a list of outputs `as :: [a]`. These outputs are then fed again to the first machine and the circle starts again, until one of the two machines emits the empty list `[]`. The composed machine will emit all the `bs` emitted in each round of the loop.
Notice that in fact everything works not only for lists, but for every foldable type.
## `Kleisli`
```haskell
Kleisli
:: StateMachineT m a [b]
-> StateMachineT m b [c]
-> StateMachineT m a [c]
```
is very similar to `Compose`, but it allows us to compose machines which emit multiple outputs.
Consider two machines
```
a ┌────┐ [b] b ┌────┐ [c]
──┤ ├──>> ──┤ ├──>>
└────┘ └────┘
```
We can compose them
```
┌───────────────────┐
a │ ┌╌╌╌╌┐ [b] ┌╌╌╌╌┐ │ [c]
──┼╌┤ ├╌╌>>╌┤ ├╌┼──>>
│ └╌╌╌╌┘ └╌╌╌╌┘ │
└───────────────────┘
```
where the outputs `bs :: [b]` of the first machine are is passed as inputs to the second machine, and processed all one by one.
Notice that in fact everything works not only for lists, but for every foldable type.
## `Basic`
All the other constructors are combinators to construct more complicated machine out of simpler ones. We still miss a way to build the simpler ones! That is exactly what the `Basic` constructor provides. It gives a way to create a machine by specifying precisely its internal behaviour.
@ -165,3 +239,129 @@ In practice, a `Topology` is a list of pairs, where every pair contains a vertex
In fact, we use [`singletons`](https://hackage.haskell.org/package/singletons) to promote `Topology` to the type level and use it to keep track of the available machine transitions at the type level.
We use a `Topology vertex` kind, and we construct types of that kind using the `Topology :: [(vertex, [vertex])] -> Topology vertex` type constructor. In such a use, notice that also `vertex` is a kind.
#### Defining a `Topology`
To define a `Topology`, we first need to define the type of its vertices.
This is usually done by defining an enumeration of the vertices, like
```haskell
data ExampleVertex
= FirstVertex
| SecondVertex
| ThirdVertex
```
Next we want to describe which are the allowed transitions for our topology. We do this by listing them in the format described in the previous paragraph. For example
```haskell
exampleTopology :: Topology ExampleVertex
exampleTopology =
Topology
[ (FirstVertex, [SecondVertex, ThirdVertex])
, (SecondVertex, [ThirdVertex])
]
```
This defines the following topology
```mermaid
stateDiagram-v2
FirstVertex --> SecondVertex
FirstVertex --> ThirdVertex
SecondVertex --> ThirdVertex
```
Since we need the topology information at the type level, we wrap the two type definitions in
```haskell
$( singletons
[d|
...
|]
)
```
### Defining a `BaseMachine`
Now that we have our `exampleTopology`, we can learn how to define a `BaseMachine` where only the transitions listed in the topology are allowed.
A `BaseMachine topology a b` is index by its `topology`, the type `a` of its inputs and the type `b` of its outputs. In fact, there is another type which needs to be defined in order to implement a `BaseMachine` and that is the type of its possible states.
#### Describing the states space
To define the complete set of possible states of our machine, we need to say which are the possible states for every vertex of the topology.
To do this, we need to associate to every vertex the type of the states allowed for that vertex. We can achieve this by using a GADT like the following:
```haskell
data ExampleState (vertex :: ExampleVertex) where
FirstVertexState :: Int -> ExampleState 'FirstVertex
SecondVertexState :: String -> ExampleState 'SecondVertex
ThirdVertexState :: Bool -> ExampleState 'ThirdVertex
```
This says that the first vertex will contain an `Int`, the second vertex a `String` and the third vertex a `Bool`.
Notice how we are using `ExampleVertex` as a kind and `'FirstVertex`, `'SecondVertex` and `'ThirdVertex` as types of that kind.
#### Implementing the machine logic
Now that we have defined all the relevant types (i.e. the topology, the state, the input and the outputs of the machine), we can eventually define its internal logic.
A `BaseMachine` requires two things to be defined, its initial state and its action logic, which defines how to evolve the state and which output should be emitted when an input is received.
##### Defining the initial state
The initial state has type `InitialState state`, which is defined as
```haskell
data InitialState (state :: vertex -> Type) where
InitialState :: state vertex -> InitialState state
```
The `state` parameter is a type of kind `vertex -> Type`. It has a single constructor which requires a value of type `state vertex`.
In our example, we need to define a value of type `InitialState ExampleState` (`ExampleState` is a type of kind `ExampleVertex -> Type`, so it fits perfectly!). Hence, we need a value of type `ExampleState vertex` to construct it. Since `ExampleState` has three constructors, we have three options:
- storing an `Int` in the first vertex, with `FirstVertexState`
- storing a `String` in the second vertex, with `SecondVertexState`
- storing a `Bool` in the third vertex, with `ThirdVertexState`
For the sake of the example, let's say we pick the first option, and we define
```haskell
initialState = InitialState $ FirstVertexState 42
```
##### Defining the action logic
The last thing we need to define is how the machine should react to receiving an input. This is described by the `action` field which has the following type
```haskell
action
:: state initialVertex
-> input
-> ActionResult m topology state initialVertex output
```
In practice, for every possible state and received input, we need to define the final state and the emitted output. The type is a bit fancier because it is actually constraining the state transition to respect the `topology`. If we try to implement a transition which is not allowed by the topology, the code will simply fail to compile. Apart from that, `ActionResult` is just a newtype around a pair `(output, state finalVertex)`.
Concluding our example, we could implement action as follows
```haskell
action = \case
FirstVertexState i -> \input ->
if i > 10
then ActionResult (_, SecondVertexState (_ :: String))
else ActionResult (_, ThirdVertexState (_ :: Bool))
SecondVertexState s -> \input ->
ActionResult (_, ThirdVertexState (_ :: Bool))
ThirdVertexState b -> \input ->
ActionResult (_, ThirdVertexState (not b))
```
where we left some holes, which can be freely filled depending on the output type and the logic of the machine.
Notice that for the third vertex, we implemented our machine so that every transition would just end up in the same vertex. Such a transition is not explicitly included in our `ExampleTopology`. This still works because every trivial transition from a vertex to itself is always allowed.