类型安全流（状态机）

Question

我正在尝试在 Haskell 中创建一个类型安全的问答流程。我将 QnA 建模为有向图，类似于 FSM。

图中的每个节点代表一个问题：

data Node s a s' = Node {
  question :: Question a,
  process :: s -> a -> s'
}

s 是输入状态，a 是问题的答案，s' 是输出状态。节点取决于输入状态s，这意味着要处理答案，我们必须先处于特定状态。

Question a 表示一个简单的问题/答案，产生a 类型的答案。

我的意思是类型安全，例如给定一个节点Node2 :: si -> a -> s2，如果si 依赖于s1，那么所有以Node2 结尾的路径都必须通过一个首先产生s1 的节点。 （如果s1 == si 则Node2 的所有前辈都必须产生s1）。

一个例子

QnA：在一个在线购物网站，我们需要询问用户的体型和喜欢的颜色。

1. e1：询问用户是否知道自己的尺寸。如果是，则转到e2，否则转到e3
2. e2：询问用户尺码，前往ef询问颜色。
3. e3：（用户不知道自己的尺寸），询问用户的体重，去e4。
4. e4：（在e3之后）询问用户的身高并计算他们的大小，然后转到ef.
5. ef：询问用户最喜欢的颜色并以Final结果结束流程。

在我的模型中，Edges 将Nodes 相互连接：

data Edge s sf where
  Edge  :: EdgeId -> Node s a s' -> (s' -> a -> Edge s' sf) -> Edge s sf
  Final :: EdgeId -> Node s a s' -> (s' -> a -> sf) -> Edge s sf

sf 是 QnA 的最终结果，即：(Bool, Size, Color)。

每个时刻的 QnA 状态可以用一个元组表示：(s, EdgeId)。这个状态是可序列化的，我们应该能够通过知道这个状态来继续 QnA。

saveState :: (Show s) => (s, Edge s sf) -> String
saveState (s, Edge eid n _) = show (s, eid)

getEdge :: EdgeId -> Edge s sf
getEdge = undefined --TODO

respond :: s -> Edge s sf -> Input -> Either sf (s', Edge s' sf)
respond s (Edge ...) input = Right (s', Edge ...)
respond s (Final ...) input = Left s' -- Final state

-- state = serialized (s, EdgeId)
-- input = user's answer to the current question
main' :: String -> Input -> Either sf (s', Edge s' sf)
main' state input =
  let (s, eid) = read state :: ((), EdgeId) --TODO
      edge = getEdge eid
  in respond s input edge

完整代码：

{-# LANGUAGE GADTs, RankNTypes, TupleSections #-}

type Input = String
type Prompt = String
type Color = String
type Size = Int
type Weight = Int
type Height = Int

data Question a = Question {
  prompt :: Prompt,
  answer :: Input -> a
}

-- some questions 
doYouKnowYourSizeQ :: Question Bool
doYouKnowYourSizeQ = Question "Do you know your size?" read

whatIsYourSizeQ :: Question Size
whatIsYourSizeQ = Question "What is your size?" read

whatIsYourWeightQ :: Question Weight
whatIsYourWeightQ = Question "What is your weight?" read

whatIsYourHeightQ :: Question Height
whatIsYourHeightQ = Question "What is your height?" read

whatIsYourFavColorQ :: Question Color
whatIsYourFavColorQ = Question "What is your fav color?" id

-- Node and Edge

data Node s a s' = Node {
  question :: Question a,
  process :: s -> a -> s'
}

data Edge s sf where
  Edge  :: EdgeId -> Node s a s' -> (s' -> a -> Edge s' sf) -> Edge s sf
  Final :: EdgeId -> Node s a s' -> (s' -> a -> sf) -> Edge s sf

data EdgeId = E1 | E2 | E3 | E4 | Ef deriving (Read, Show)

-- nodes

n1 :: Node () Bool Bool
n1 = Node doYouKnowYourSizeQ (const id)

n2 :: Node Bool Size (Bool, Size)
n2 = Node whatIsYourSizeQ (,)

n3 :: Node Bool Weight (Bool, Weight)
n3 = Node whatIsYourWeightQ (,)

n4 :: Node (Bool, Weight) Height (Bool, Size)
n4 = Node whatIsYourHeightQ (\ (b, w) h -> (b, w * h))

n5 :: Node (Bool, Size) Color (Bool, Size, Color)
n5 = Node whatIsYourFavColorQ (\ (b, i) c -> (b, i, c))


-- type-safe edges

e1 = Edge E1 n1 (const $ \ b -> if b then e2 else e3)
e2 = Edge E2 n2 (const $ const ef)
e3 = Edge E3 n3 (const $ const e4)
e4 = Edge E4 n4 (const $ const ef)
ef = Final Ef n5 const


ask :: Edge s sf -> Prompt
ask (Edge _ n _) = prompt $ question n
ask (Final _ n _) = prompt $ question n

respond :: s -> Edge s sf -> Input -> Either sf (s', Edge s' sf)
respond s (Edge _ n f) i =
  let a  = (answer $ question n) i
      s' = process n s a
      n' = f s' a
  in Right undefined --TODO n'

respond s (Final _ n f) i =
  let a  = (answer $ question n) i
      s' = process n s a
  in Left undefined --TODO s'


-- User Interaction:

saveState :: (Show s) => (s, Edge s sf) -> String
saveState (s, Edge eid n _) = show (s, eid)

getEdge :: EdgeId -> Edge s sf
getEdge = undefined --TODO

-- state = serialized (s, EdgeId) (where getEdge :: EdgeId -> Edge s sf)
-- input = user's answer to the current question
main' :: String -> Input -> Either sf (s', Edge s' sf)
main' state input =
  let (s, eid) = undefined -- read state --TODO
      edge = getEdge eid
  in respond s edge input

保持边缘类型安全对我来说很重要。例如错误地将e2 链接到e3 的含义必须是一个类型错误：e2 = Edge E2 n2 (const $ const ef) 很好，e2 = Edge E2 n2 (const $ const e3) 一定是一个错误。

我已通过--TOOD 提出我的问题：

• 鉴于我保持边缘类型安全的标准，Edge s sf 必须有一个输入类型变量 (s)，那么如何创建 getEdge :: EdgeId -> Edge s sf 函数？

• 如果给定当前状态 s 和当前边 Edge s sf，我如何创建 respond 函数，它将返回最终状态（如果当前边是 Final）或下一个状态和下一条边(s', Edge s' sf)？

我对@9​​87654371@ 和Edge s sf 的设计可能完全是错误的。我不必坚持下去。

Answer 1

为了有一个简单的例子来解释，我将向您展示一个没有自然支持暂停、持久化和恢复计算的解决方案。最后我会告诉你如何添加它的要点——希望你能自己弄清楚它的本质。

---

这是所谓的索引状态单子：

newtype IStateT m i o a = IStateT { runIState :: i -> m (o, a) }

IStateT 就像一个常规的状态单子转换器，除了隐式状态的类型允许在整个计算过程中改变。在索引状态单子中对动作进行排序要求一个动作的输出状态与下一个动作的输入状态匹配。这种类似多米诺骨牌的排序就是Atkey's parameterised monad（或indexed monad）的用途。

class IMonad m where
    ireturn :: a -> m i i a
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b

(>>>) :: IMonad m => m i j a -> m j k b -> m i k b
mx >>> my = mx >>>= \_ -> my

IMonad 是一类类似 monad 的东西，它描述了通过索引图的路径。 (>>>=) 的类型表示“如果你有一个从 i 到 j 的计算以及从 j 到 k 的计算，我可以加入它们来给你一个从 i 到的计算k"。

我们还需要将计算从经典 monad 提升到索引 monad：

class IMonadTrans t where
    ilift :: Monad m => m a -> t m i i a

请注意，IStateT 的代码与常规状态 monad 的代码相同 - 只是类型变得更智能。

iget :: Monad m => IStateT m s s s
iget = IStateT $ \s -> return (s, s)

iput :: Monad m => o -> IStateT m i o ()
iput x = IStateT $ \_ -> return (x, ())

imodify :: Monad m => (i -> o) -> IStateT m i o ()
imodify f = IStateT $ \s -> return (f s, ())

instance Monad m => IMonad (IStateT m) where
    ireturn x = IStateT (\s -> return (s, x))
    IStateT f >>>= g = IStateT $ \s -> do
                                    (s', x) <- f s
                                    let IStateT h = g x
                                    h s'
instance IMonadTrans IStateT where
    ilift m = IStateT $ \s -> m >>= \x -> return (s, x)

这个想法是像askSize 和askWeight（下）这样的单子操作将向隐式环境添加一些数据，从而增加它的类型。因此，我将从嵌套元组构建隐式环境，将它们视为类型级别的类型列表。嵌套元组比扁平元组更灵活（尽管效率较低），因为它们允许您对列表的尾部进行抽象。这允许您构建任意大小的元组。

type StateMachine = IStateT IO

newtype Size = Size Int
newtype Height = Height Int
newtype Weight = Weight Int
newtype Colour = Colour String

-- askSize takes an environment of type as and adds a Size element
askSize :: StateMachine as (Size, as) ()
askSize = askNumber "What is your size?" Size

-- askHeight takes an environment of type as and adds a Height element
askHeight :: StateMachine as (Height, as) ()
askHeight = askNumber "What is your height?" Height

-- etc
askWeight :: StateMachine as (Weight, as) ()
askWeight = askNumber "What is your weight?" Weight

askColour :: StateMachine as (Colour, as) ()
askColour =
    -- poor man's do-notation. You could use RebindableSyntax
    ilift (putStrLn "What is your favourite colour?") >>>
    ilift readLn                                      >>>= \answer ->
    imodify (Colour answer,)

calculateSize :: Height -> Weight -> Size
calculateSize (Height h) (Weight w) = Size (h - w)  -- or whatever the calculation is

askNumber :: String -> (Int -> a) -> StateMachine as (a, as) ()
askNumber question mk =
    ilift (putStrLn question) >>>
    ilift readLn              >>>= \answer ->
    case reads answer of
        [(x, _)] -> imodify (mk x,)
        _ -> ilift (putStrLn "Please type a number") >>> askNumber question mk

askYN :: String -> StateMachine as as Bool
askYN question =
    ilift (putStrLn question) >>>
    ilift readLn              >>>= \answer ->
    case answer of
        "y" -> ireturn True
        "n" -> ireturn False
        _ -> ilift (putStrLn "Please type y or n") >>> askYN question

我的实现与您的规范略有不同。你说应该不可能询问用户的尺寸，然后询问他们的体重。我说这应该是可能的——结果不一定是你想要的类型（因为你在环境中添加了两件事，而不是一个）。这在这里很有用，其中askOrCalculateSize 只是一个黑盒子，它将Size（仅此而已）添加到环境中。有时它通过直接询问尺寸来做到这一点；有时它通过首先询问身高和体重来计算它。就类型检查器而言，这无关紧要。

interaction :: StateMachine xs (Colour, (Size, xs)) ()
interaction =
    askYN "Do you know your size?" >>>= \answer ->
    askOrCalculateSize answer >>>
    askColour

    where askOrCalculateSize True = askSize
          askOrCalculateSize False =
            askWeight >>>
            askHeight >>>
            imodify (\(h, (w, xs)) -> ((calculateSize h w), xs))

---

还有一个问题：如何从持久状态恢复计算？你并不知道输入环境的类型（尽管假设输出总是(Colour, Size) 是安全的），因为它在整个计算过程中会发生变化，并且在加载持久状态之前你不知道它最多.

诀窍是使用一些 GADT 证据，您可以在这些证据上进行模式匹配以了解类型是什么。 Stage 表示您在此过程中可以达到的位置，并且它按该阶段环境应具有的类型进行索引。 Suspended 将 Stage 与计算暂停时环境中的实际数据配对。

data Stage as where
    AskSize :: Stage as
    AskWeight :: Stage as
    AskHeight :: Stage (Weight, as)
    AskColour :: Stage (Size, as)

data Suspended where
    Suspended :: Stage as -> as -> Suspended

resume :: Suspended -> StateMachine as (Colour, (Size, as)) ()
resume (Suspended AskSize e) =
    iput e                                               >>>
    askSize                                              >>>
    askColour
resume (Suspended AskWeight e) =
    iput e                                               >>>
    askWeight                                            >>>
    askHeight                                            >>>
    imodify (\(h, (w, xs)) -> ((calculateSize h w), xs)) >>>
    askColour
resume (Suspended AskHeight e) =
    iput e                                               >>>
    askHeight                                            >>>
    imodify (\(h, (w, xs)) -> ((calculateSize h w), xs)) >>>
    askColour
resume (Suspended AskColour e) =
    iput e                                               >>>
    askColour

现在您可以在计算中添加暂停点：

-- given persist :: Suspended -> IO ()
suspend :: Stage as -> StateMachine as as ()
suspend stage =
    iget                                  >>>= \env
    ilift (persist (Suspended stage env))

resume 有效，但它非常丑陋并且有很多代码重复。这是因为一旦你把一个状态单子放在一起，你就不能再把它拆开来查看它的内部。您不能在计算中的给定点跳入。这是您原始设计的一大优势，其中您将状态机表示为可以查询的数据结构，以便找出如何恢复计算。这称为 initial 编码，而我的示例（将状态机表示为函数）是 final 编码。最终编码很简单，但初始编码很灵活。希望您能了解如何将初始方法调整到索引 monad 设计。