Created
August 10, 2020 04:47
-
-
Save adamwespiser/f5af0d6447417d989d8667ad54532153 to your computer and use it in GitHub Desktop.
Finite State Machine ~ in Haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- stack | |
--resolver lts-16.8 | |
--packages "transformers" | |
exec ghci | |
-} | |
{-# Language | |
EmptyDataDeriving | |
, GADTs | |
, GeneralizedNewtypeDeriving | |
, InstanceSigs | |
, LambdaCase | |
, TypeApplications | |
, TypeFamilies #-} | |
module FSM where | |
-- inspired by: https://github.com/keksnicoh/tortoise-service | |
import Control.Monad.IO.Class | |
import Control.Monad.Reader | |
import Text.Read (readMaybe) | |
import Control.Concurrent (threadDelay) | |
{- phantom types representing state -} | |
data Initialzing deriving (Eq, Show) | |
data HasData deriving (Eq, Show) | |
data OutputData deriving (Eq, Show) | |
data Terminating deriving (Eq, Show) | |
main :: IO () | |
main = runFSM | |
where | |
runFSM :: IO () | |
runFSM = do | |
(runT $ mkFSM ioHandler ) >>= \case | |
reason -> do | |
putStrLn $ "FSM has terminated with: " <> show reason | |
ioHandler :: (Monad m, MonadIO m) => Handlers m | |
ioHandler = Handlers { | |
readData = liftIO $ readMaybe <$> getLine | |
, peakData = return True | |
, storeData = liftIO . putStrLn . ((<>) " to storage") . show | |
, delay = liftIO . threadDelay $ 100000 | |
, logMsg = liftIO . putStrLn | |
, myData = Nothing | |
} | |
-- | FSM: A class describing our Finite state machine | |
-- Methods are parameterized on the Transitions, restricting possible origins | |
-- 'State' is Associated typeclass | |
class (MonadIO m) => FSM m where | |
type State m :: * -> * | |
initialize :: m (State m Initialzing) | |
checkData :: HasDataEvent m -> m (State m HasData) | |
outputData :: ReadEvent m -> m (State m OutputData) | |
terminate :: TxnTerminating m -> m (State m Terminating) | |
{- | |
Transitions: each transition is set up as follows: | |
-- Type Constructor: Describes where the txn is going TO | |
-- Data Constructors: Enumerates where the txn can come from | |
-} | |
data ReadEvent m | |
= ReadDataFromEnv (State m HasData) | |
data HasDataEvent m | |
= StartMonitor (State m Initialzing) | |
| RetryHasData (State m HasData) | |
data TxnTerminating m | |
= NoData (State m HasData) | |
| NoInit (State m Initialzing) | |
| FailOutput (State m OutputData) | |
| SuccussOutput (State m OutputData) | |
-- | RunState: A GADT for Indexing our Monad | |
-- Each Constructor is a State in our FSM graph | |
data RunState s where | |
Initialzing :: RunState Initialzing | |
HasData :: RunState HasData | |
OutputData :: RunState OutputData | |
Terminating :: RunState Terminating | |
instance Show (RunState s) where | |
show Initialzing = "Initialzing" | |
show HasData = "HasData" | |
show OutputData = "OutputData" | |
show Terminating = "Terminating" | |
-- | Our monad | |
newtype RunT m a = RunT { runT :: m a } | |
deriving (Functor, Monad, Applicative, MonadIO) | |
-- | Define our monad, RutT, as an Instance of FSM | |
-- Also, define the associated type family for each method to | |
-- return the State GADT, RunState | |
instance (MonadIO m, Monad m) => FSM (RunT m) where | |
type State (RunT m) = RunState | |
initialize :: (RunT m ~ n) => n (State n Initialzing) | |
initialize = do | |
liftIO $ putStrLn "initialize" | |
return Initialzing | |
checkData :: (RunT m ~ n) => HasDataEvent n -> n (State n HasData) | |
checkData _ = do | |
liftIO $ putStrLn "checkData" | |
return HasData | |
outputData :: (RunT m ~ n) => ReadEvent n -> n (State n OutputData) | |
outputData _ = do | |
liftIO $ putStrLn "outputData" | |
return OutputData | |
terminate :: (RunT m ~ n) => TxnTerminating n -> n (State n Terminating) | |
terminate _ = do | |
liftIO $ putStrLn "terminate" | |
return Terminating | |
-- | ADT for effect handler | |
data Handlers m = Handlers | |
{ readData :: m (Maybe Integer) | |
, peakData :: m Bool | |
, storeData :: Integer -> m () | |
, delay :: m () | |
, logMsg :: String -> m () | |
, myData :: Maybe Integer | |
} | |
mkFSM :: (FSM m, Monad m) => Handlers m -> m (State m Terminating) | |
mkFSM h = initialize >>= start h | |
start :: (FSM m, Monad m, MonadIO m) | |
=> Handlers m | |
-> State m Initialzing | |
-> m (State m Terminating) | |
start h state = do | |
peakData h >>= \case | |
False -> terminate $ NoInit state | |
True -> checkData >=> ingestData h $ StartMonitor state | |
ingestData :: (FSM m, Monad m, MonadIO m) | |
=> Handlers m | |
-> State m HasData | |
-> m (State m Terminating) | |
ingestData h state = do | |
readData h >>= \case | |
Nothing -> terminate $ NoData state | |
Just x -> do | |
checkData >=> ingestData (h {myData = Just x}) $ RetryHasData state | |
writeData :: (FSM m, Monad m, MonadIO m) | |
=> Handlers m | |
-> State m OutputData | |
-> m (State m Terminating) | |
writeData h state = do | |
case myData h of | |
Nothing -> terminate $ FailOutput state | |
Just x -> do | |
storeData h $ x | |
terminate $ SuccussOutput state |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env bash | |
# just run this as a one off command | |
ghcid -c "stack ghci FSM.hs" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment