Library for typesafe state machines. Make impossible state transitions impossible and more
The Hebrew word for “okay” and for “alright” is “beseder” (be-se-der)
- Provide a way of capturing protocols, APIs, business data model and business rules in an uniformed manner that covers all aspects of resource lifecycle: resource creation resource disposal, invoking requests, external changes at resources states
- Strong type safety and compile time guarantees:
- all allocated resources are released, even in most messy cases of interleaved resource usage
- only operations that are supported for given resource state are allowed
- all possible resource state changes are observed
- Effortless parallelism
- Structured concurrency done naturally and seamlessly
- Informal notion of linear types: no access to a stale resource states, no state can be left unhandled
- Allows describing properties of the system as constraints, reducing the number of required tests.
- Leverage the powerful type system, type inference and type level computation to enable interactive and entertaining domain exploration and development process.
- [Finite-State Machines articles by Oskar Wickström] (https://wickstrom.tech/finite-state-machines/2017/11/10/finite-state-machines-part-1-modeling-with-haskell.html)
- [Control Flow in Haskell - Flow with Variant by Sylvain Henry] (https://hsyl20.fr/home/posts/2016-12-12-control-flow-in-haskell-part-3.html)
- [Indexed Monads by Kwang Yul Seo] (https://kseo.github.io/posts/2017-01-12-indexed-monads.html)
- [Thinking with types by Sandy Maguire] (https://leanpub.com/thinking-with-types)
- [Introducing ST: Working with State] (http://docs.idris-lang.org/en/latest/st/state.html)
-
The basic entity at Beseder is a resource. The system state at any given moment is represented by the states of the resources. In other words state of the system is a product of the system's resources states.
-
Resources are created, going through a series of state transitions and eventually deleted. The state transition is caused by request (operation) invoked on the resource or change in resource state that happened outside of the system (unsolicited state change). Every resource state is represented by a specific distinctive Haskell type. The following type classes capture all supported resource related operations:
--create resource
class MkRes ctx res where
type ResSt ctx res :: *
mkRes :: res -> ctx (ResSt ctx res)
--clear resource
class TermState ctx state where
terminate :: state -> ctx ()
--unsolicted resource state transition
class Transition ctx state1 where
type NextStates state1 :: [*]
next :: state1 -> (V (NextStates state1) -> ctx Bool) -> ctx Bool
-- request invocation
class Request ctx req state1 where
type ReqResult (req :: *) (st :: *) :: [*]
request :: req -> state1 -> ctx (V (ReqResult req state1))
The simplest way to create new resource is to use type class that defines resource initial and terminated states, as well as supported requests and state transitions for every state. Then we call buildRes that uses Template Haskell to generate all required declarations. As a bonus buildRes also generates resource state diagram
- Here is an example of CardReader resource definition from ATM demo program:
Door (door resource) gets open when either the fob is read (fobReader) or internal proximity sensor (inDet) was triggered. The door should stay open for predefined time interval (doorTimeoutSec). The door should stay open as long as at least one of proximity sensors (inDet or outDet) are on
doorHandler doorTimeoutSec =
handleEvents $ do
on @("fobReader" :? IsMessageReceived) $ do
invoke #fobReader GetNextMsg
openDoorIfClosed doorTimeoutSec
on @("inDet" :? IsBinMonitorOn) $ do
openDoorIfClosed doorTimeoutSec
on @("doorTimer" :? IsTimerTriggered) $ do
onOrElse @("inDet" :? IsBinMonitorOn :|| "outDet" :? IsBinMonitorOn)
(restartTimer doorTimeoutSec)
closeDoor
openDoorIfClosed :: Int -> STransData m sp _ ()
openDoorIfClosed doorTimeoutSec = do
on @("door" :? IsBinSwitchOff) $ do
invoke #door TurnOn
newRes #doorTimer TimerRes
invoke #doorTimer (StartTimer doorTimeoutSec)
closeDoor :: STransData m sp _ ()
closeDoor = do
clear #doorTimer
invoke #door TurnOff
restartTimer :: Int -> STransData m sp _ ()
restartTimer doorTimeoutSec = do
clear #doorTimer
newRes #doorTimer TimerRes
invoke #doorTimer (StartTimer doorTimeoutSec)
and here is state diagram extracted for this application: