如何打包状态机库

Question

我想使用 Haskell 进行有限状态机分析和记录。我希望库足够通用，以便在实例化特定 FSM 时需要很少的样板。

状态机定义基于状态s、事件e 和动作a。主要要求是：

• 将机器显示为文本（定义或派生Show）。
• 以花哨的形式显示，例如为 Graphviz 发出 dot 符号。
• 确定有向图的正确性（对于正确性的某些定义）、终止条件和其他属性。
• 使用状态机定义来帮助确保以其他语言实现 FSM 的测试覆盖率（源代码生成、测试覆盖率分析）。

我最初的实现是这样的：

import Data.List

data StateMachine s e a =
    StateMachine { 
                   states :: [s]                    -- ^states that the machine can be in
                 , events :: [e]                    -- ^events that the machine can process
                 , actions :: [a]                   -- ^actions the machine can perform
                 , initialStates :: [s]             -- ^starting states
                 , transitions :: [((s,e),(a,s))]   -- ^state transitions
                 }

-- |Find the action and next state for an event in the given state
nextOperation :: (Ord s, Ord e, Eq a) => 
                 StateMachine s e a -> s -> e -> Maybe (a, s)
nextOperation sm st ev = lookup (st, ev) (transitions sm)

-- |Find the next state from this state for an event, if present
nextTransition :: (Ord s, Ord e, Eq a) => StateMachine s e a -> s -> e -> Maybe s
nextTransition sm st ev = fmap snd $ nextOperation sm st ev
allNextStates :: (Ord s, Ord e, Eq a) => StateMachine s e a -> s -> [e] -> [s]
allNextStates _ _ [] = []
allNextStates sm st (ev:es) = case nextTransition sm st ev of
                                Just st' -> st': allNextStates sm st es
                                Nothing  -> allNextStates sm st es

-- |Compute the set of states reachable from a state
reachableStates :: (Ord s, Ord e, Eq a) => StateMachine s e a -> s -> [s]
reachableStates sm st = nub $ allNextStates sm st (events sm)

-- |Compute the transitive closure from the initial states
transitiveClosure :: (Ord s, Ord e, Eq a) => StateMachine s e a -> [s]
transitiveClosure sm = transitives sm (initialStates sm) (initialStates sm)
    where
        transitives :: (Ord s, Ord e, Eq a) => StateMachine s e a -> [s] -> [s] -> [s]
        transitives _ [] reach = reach
        transitives stm reachable@(st: sts) reach =
             let r = reachableStates stm st
                 rs = [r' | r' <- r, not (r' `elem` reach)]
             in
                if null rs
                then transitives stm sts reach
                else transitives stm (sts ++ rs) (reach ++ rs)

从那里开始，几乎所有测试可达性所需的操作和传递闭包都可以轻松构建。但是，我最终到处都遇到了(Ord s, Ord e, Eq a) 约束，并且一直遇到“模棱两可的类型”问题。这也让我很恼火，因为我可以很容易地使用 Java 中的抽象类来定义它，比方说。

我的第二种方法是使用类型族，但这并不顺利。第一步是定义类：

{-# language TypeFamilies #-}
{-# language MultiParamTypeClasses #-}

...    

class (Ord s, Show s) => SMstate s
class (Ord e, Show e) => SMevent e
class (Eq a, Show a) => SMaction a

class (SMstate s, SMevent e, SMaction a) => MachineState s e a where
    data MS s e a
    allEvents      :: MS s e a -> [e]
    initialStates  :: MS s e a -> [s]
    allStates      :: MS s e a -> [s]
    allActions     :: MS s e a -> [a]
    nextOperation  :: MS s e a -> s -> e -> Maybe (a,s)
nextTransition :: MS s e a -> s -> e -> Maybe s
nextTransition sm st ev = fmap snd $ nextOperation sm st ev
nextState      :: MS s e a -> s -> e -> s
nextState sm st ev = case nextTransition sm st ev of
                        Just st' -> st'
                        Nothing  -> st
allNextStates  :: MS s e a -> s -> [e] -> [s]
allNextStates _ _ [] = []
allNextStates sm st (ev:evs) =
    let nextStates = allNextStates sm st evs
    in  (maybeToList $ nextTransition sm st ev) ++ nextStates
reachableStates :: MS s e a -> s -> [s]
reachableStates sm s = nub $ allNextStates sm s (allEvents sm)
transitiveClosure :: MS s e a -> [s]
transitiveClosure sm = transitivesOf sm (initialStates sm) (initialStates sm)
    where
        transitivesOf :: MachineState s e a => MS s e a -> [s] -> [s] -> [s]
        transitivesOf _ [] reach = reach
        transitivesOf sm reachable@(st:sts) reach =
            let r = reachableStates sm st
                rs = [r' | r' <- r, r' `notElem` reach]
            in
                if null rs
                then transitivesOf sm sts reach
                else transitivesOf sm (sts ++ rs) (reach ++ rs)

由于类约束与MachineState 周围的定义相关联，我不再需要担心传播约束。

类型族是解决这个问题的方法吗？如何将StateMachine 连接到MachineState 类？

Answer 1

该数据系列并没有真正完成您的具体参数化StateMachine 没有完成的任何事情。唯一真正的区别是约束被打包到单个约束中，作为MachineState 的“超类”。但这并不需要数据族——你也可以使用

class (SMstate s, SMevent e, SMaction a) => MachineState s e a
 {- Empty! -}

data StateMachine s e a =
    StateMachine { states :: [s]
                 , ... }

事实上，您甚至根本不需要为此开设课程：

{-# LANGUAGE ConstraintKinds #-}
type MachineState s e a = (Ord s, Show s, Ord e, Show e, Eq a, Show a)

...虽然我认为总是要求Show 是个好主意。

所以，不，我想说数据系列不是要走的路。您的原始方法是可行的方法，只需列出每个函数实际需要的任何约束。

如果您遇到模棱两可的类型，这可能意味着您在函数中不小心提到了一个类型变量，该函数没有使用完整的StateMachine，而只是一些例如行动清单。在这种情况下，通常只需删除约束就足够了。

在某些应用程序中，歧义类型实际上很有用。我认为您的情况不应该是这样，但是您可以查看 -XTypeApplications 扩展，这是调用具有歧义类型的函数所需要的。

---

一般的工作流程，我推荐这个：

1. 以签名开始您的函数，但没有任何约束并且实现为空。

   nextOperation :: StateMachine s e a -> s -> e -> Maybe (a, s)
   nextOperation = _
   

2. 让 GHC 的 typed-hole 功能帮助您编写实现。

3. 添加编译器需要的任何约束。

如果它还抱怨缺少 扩展，以下是我总是会毫不犹豫地做的：

• FlexibleInstances（包括TypeSynonymInstances）
• FlexibleContexts
• TypeFamilies
• GADTs
• ConstraintKinds

不是没有争议，但 IMO 也没什么大不了的

• UndecidableInstances
• LiberalTypeSynonyms
• AllowAmbiguousTypes+TypeApplications
• Rank2Types

不要使用，除非你真的想使用

• OverlappingInstances（分别是Overlapping/Overlappable pragmas）
• 绝对不是IncoherentInstances
• ImpredicativeTypes

Answer 2

过去我需要一些状态机，而 AFAIR 一切都归结为一个转换函数和几个基本类型类的使用。 你的nextOperation 函数应该够用了

例如，假设我有

type Transition s e a :: s -> e -> Maybe (a,s)

data State = Pending | InProgress | Processed 
data Even = Start | Finished

nextOperation :: Transition State Event (IO ())
nextOperation Pending Start = Just (print "started", InProgress)
nextOperation InProgress Finished = Just (print "finished", Processed)
nextOperation _ _ = Nothing

您可以创建一个给定转换列表的函数，创建一个 nextOperation 类似函数

fromTransition :: [(s, e), (a,s)] -> s -> e -> Maybe (a,s)

（我让你实现）

要编写transitiveClosure 函数，您需要所有状态、所有事件和所有初始状态的列表。使用[minBound .. maxBound] 可以轻松获取所有状态和所有事件，这需要GHC 自动生成的Enum 和Bounded 约束，所以您只需要

data State = Pending | InProgress | Processed deriving (Eq, Show, Enum, Bounded)

对于初始状态，您有两个选择，您可以将其作为参数传递给 transitiveClosure 或创建一个新的类型类

class Initials a where
     initials :: [a]

有几个常见的例子

实例首字母 () 其中首字母 = [()] instance Initials (Maybe a) where initials = [Nothing] instance Initials Bool where initials = [False] instance Num a => Initials a where initials = [0]

元组之类的东西开始变得有趣

instance (Initials a, Initials b) => Initials (a,b) 
     where initials = liftA2 (,) initials initials

当然还有State

instance Initials State where initials = [Pending]

那么transitiveClosure只需要下面的签名

transitiveClosure :: ( Bounded s, Enum s, Initials s
                     , Bounded e, Enum )
                  => (Transition s e a) -> [s]

我们只创建了一个类型类 (Initials)，它（几乎）与状态机无关，可以重用于其他事情。此外，通过(,) 实例，您可以轻松扩展您的状态并免费获得新的初始状态。

其他一切都只是函数，它们操纵或创建Transitions（我在这里使用类型同义词，但您可以只使用普通函数类型）。某些功能可能会更多地限制其他功能（例如，Show 或 Ord、Enum 等...），但这就是它的美妙之处。

TL;DR 简而言之，状态机只是一个转换函数s -> e -> Maybe (a,s)。 Haskell 如果是一种函数式语言，那么我们实际上可以将它建模为一个函数。仅此而已