haskell - 如何在 Haskell/Idris 中拥有受约束的有限状态机？

Question

编辑:用户@apocalisp和@BenjaminHodgson在下面留下了很棒的答案，跳过阅读大部分问题并跳转到他们的答案。

问题的TLDR:我怎样才能从第一张图片(FSM 状态组合爆炸)转到第二张图片(您只需要在继续之前访问所有图片)。

<小时/>

我想构建一个有限状态机(实际上是在Haskell中，但我首先尝试Idris，看看它是否可以指导我的Haskell)，其中有一些必须访问的临时状态在达到最终状态之前。如果我可以在某些状态上使用谓词任意约束 FSM，那就太好了。

在下图中，有一个 Initial 状态、3 个中间状态 A、B、C 和一个 Final 状态。如果我没记错的话，在“正常”FSM 中，您将始终需要 n! 临时状态来表示可能路径的每种组合。

这是不可取的。

相反，使用类型族，也许依赖类型，我认为应该有可能拥有一种随身携带的状态，并且仅当它通过时某些谓词将允许您进入最终状态。 (这是否使它下推自动机而不是FSM？)

到目前为止，我的代码(idris)，以此类推，正在添加成分来制作沙拉，顺序并不重要，但它们都需要将其放入:

data SaladState = Initial | AddingIngredients | ReadyToEat

record SaladBowl where
       constructor MkSaladBowl
       lettuce, tomato, cucumber : Bool

data HasIngredient : (ingredient : SaladBowl -> Bool) -> (bowl : SaladBowl ** ingredient bowl = True) -> Type where
     Bowl : HasIngredient ingredient bowl

data HasIngredients : (ingredients : List (SaladBowl -> Bool))
                     -> (bowl : SaladBowl ** (foldl (&&) True (map (\i => i bowl) ingredients) = True)) 
                     -> Type where
     Bowlx : HasIngredients ingredients bowl

data SaladAction : (ty : Type) -> SaladState -> (ty -> SaladState) -> Type where
     GetBowl     : SaladAction SaladBowl Initial (const Initial)
     AddLettuce  : SaladBowl -> SaladAction (bowl ** HasIngredient lettuce bowl)  st (const AddingIngredients)
     AddTomato   : SaladBowl -> SaladAction (bowl ** HasIngredient tomato bowl)   st (const AddingIngredients)
     AddCucumber : SaladBowl -> SaladAction (bowl ** HasIngredient cucumber bowl) st (const AddingIngredients)
     MixItUp     : SaladBowl -> SaladAction (bowl ** (HasIngredients [lettuce, tomato, cucumber] bowl)) AddingIngredients (const ReadyToEat)
     Pure : (res : ty) -> SaladAction ty (state_fn res) state_fn
     (>>=) : SaladAction a state1 state2_fn
           -> ((res : a) -> SaladAction b (state2_fn res) state3_fn)
           -> SaladAction b state1 state3_fn

emptyBowl : SaladBowl
emptyBowl = MkSaladBowl False False False

prepSalad1 : SaladAction SaladBowl Initial (const ReadyToEat)
prepSalad1 = do
           (b1 ** _) <- AddTomato emptyBowl
           (b2 ** _) <- AddLettuce b1
           (b3 ** _) <- AddCucumber b2
           MixItUp b3

以及编译器应该出错的反示例程序:

BAD : SaladAction SaladBowl Initial (const ReadyToEat)
BAD = do
           (b1 ** _) <- AddTomato emptyBowl
           (b2 ** _) <- AddTomato emptyBowl
           (b3 ** _) <- AddLettuce b2
           (b4 ** _) <- AddCucumber b3
           MixItUp b4

BAD' : SaladAction SaladBowl Initial (const ReadyToEat)
BAD' = do
           (b1 ** _) <- AddTomato emptyBowl
           MixItUp b1

我最终希望“成分”是 Sums 而不是 Bools (data Lettuce = Romaine | Iceberg | Butterhead)，以及更强大的语义，我可以说“你必须首先添加生菜” ，或菠菜，但不能两者兼而有之”。

真的，我感觉完全迷失了，我想我上面的代码已经走向了完全错误的方向......我怎样才能构建这个FSM(PDA？)来排除坏程序？我特别想使用 Haskell 来实现它，也许使用索引 Monad？

Answer 1

索引状态单子(monad)正是这样做的。

常规的 State s monad 模拟一个状态机(具体来说是一个 Mealy 机)，其状态字母表是 s 类型。这种数据类型实际上只是一个函数:

newtype State s a = State { run :: s -> (a, s) }

a -> State s b 类型的函数是一个具有输入字母 a 和输出字母 b 的机器。但它实际上只是一个 (a, s) -> (b, s) 类型的函数。

将一台机器的输入类型和另一台机器的输出类型对齐，我们可以组成两台机器:

(>>=) :: State s a -> (a -> State s b) -> State s b
m >>= f = State (\s1 -> let (a, s2) = run m s1 in run (f a) s2)  

换句话说，State s是一个monad。

但有时(如您的情况)，我们需要改变中间状态的类型。这就是索引状态单子(monad)的用武之地。它有两个状态字母表。 IxState i j a 模拟一台机器，其起始状态必须为 i，结束状态为 j:

newtype IxState i j a = IxState { run :: i -> (a, j) }

常规的 State s monad 就相当于 IxState s 。我们可以像编写 State 一样轻松地编写 IxState。实现与以前相同，但类型签名更通用:

(>>>=) :: IxState i j a -> (a -> IxState j k b) -> IxState i k b
m >>>= f = IxState (\s1 -> let (a, s2) = run m s1 in run (f a) s2)  

IxState 并不完全是一个 monad，而是一个索引 monad。

我们现在只需要一种指定状态类型约束的方法。对于沙拉示例，我们想要这样的东西:

mix :: IxState (Salad r) Ready ()

这是一台机器，其输入状态是一些不完整的Salad，由成分r组成，其输出状态是Ready，表明我们的沙拉可以吃了。

使用类型级列表，我们可以这样说:

data Salad xs = Salad
data Ready = Ready
data Lettuce
data Cucumber
data Tomato

空沙拉的配料表是空的。

emptyBowl :: IxState x (Salad '[]) ()
emptyBowl = iput Salad

我们可以将生菜添加到任何沙拉中:

addLettuce :: IxState (Salad r) (Salad (Lettuce ': r)) ()
addLettuce = iput Salad

我们可以对番茄和 cucumber 重复相同的操作。

现在 mix 的类型只需为:

mix :: IxState (Salad '[Lettuce, Cucumber, Tomato]) Ready ()
mix = const Ready

如果我们尝试混合任何未添加生菜、 cucumber 和番茄的沙拉，我们会收到类型错误到，按这个顺序。例如。这将是一个类型错误:

emptyBowl >>>= \_ -> addLettuce >>>= \_ -> mix

但理想情况下，我们希望能够以任何顺序添加成分。因此，我们需要对类型级别列表进行限制，要求提供证据证明沙拉中存在某种特定成分:

class Elem xs x

instance {-# OVERLAPS #-} Elem (x ': xs) x
instance Elem xs x => Elem (y ': xs) x

Elem xs x 现在是类型 x 位于类型级列表 xs 中的证据。第一个实例(基本情况)表明 x 显然是 x ': xs 的元素。第二个实例表示，如果类型 x 是 xs 的元素，那么它也是任何类型 y ': xs 的元素 y。 OVERLAPS 对于确保 Haskell 知道首先检查基本情况是必要的。

以下是完整列表:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

import Control.Monad.Indexed
import Control.Monad.Indexed.State

data Lettuce
data Tomato
data Cucumber

data Ready = Ready

class Elem xs x

instance {-# OVERLAPS #-} Elem (x ': xs) x
instance Elem xs x => Elem (y ': xs) x

data Salad xs = Salad

emptyBowl :: IxState x (Salad '[]) ()
emptyBowl = iput Salad

addLettuce :: IxState (Salad r) (Salad (Lettuce ': r)) ()
addLettuce = iput Salad

addTomato :: IxState (Salad r) (Salad (Tomato ': r)) ()
addTomato = iput Salad

addCucumber :: IxState (Salad r) (Salad (Cucumber ': r)) ()
addCucumber = iput Salad

mix :: (Elem r Lettuce, Elem r Tomato, Elem r Cucumber)
    => IxState (Salad r) Ready ()
mix = imodify mix'
  where mix' = const Ready

x >>> y = x >>>= const y

-- Compiles
test = emptyBowl >>> addLettuce >>> addTomato >>> addCucumber >>> mix

-- Fails with a compile-time type error
fail = emptyBowl >>> addTomato >>> mix