如何在Haskell / Idris中实现有限状态机的约束？

Question

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

问题概述：如何从第一张图片（FSM状态组合爆炸）到达第二张图片（在继续前需要访问所有状态）。

---

我想建立一个有限状态机（实际上是在Haskell中，但我首先尝试使用Idris来看看它是否能指导我的Haskell），其中有一些中间状态必须在到达最终状态之前进行访问。如果我可以任意地限制某些状态的谓词，那就太好了。

在下面的图片中，有一个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

我希望最终的“成分”是总和，而不是布尔值 (data Lettuce = Romaine | Iceberg | Butterhead)，并且拥有更强大的语义，例如“您必须先添加生菜或菠菜，但不能同时添加两者”。

实际上，我感到非常迷茫，以至于我想象我的上述代码已经完全走错了方向...如何构建这个FSM (PDA?)来防止出现糟糕的程序？我特别想使用Haskell，也许使用Indexed Monads？

- Josh.F

---

你的代码虽然有点繁琐，但似乎并没有完全错误。你定义了一种行动类型，它以状态对（输入/输出状态）为索引，每个行动指示它可以从哪些状态移动到哪些状态。这部分没问题。由于你希望最多只添加一次每个配料，因此你需要在类型 AddLettuce :: ... -> SaladAction (bowl ** HasIngredient lettuce bowl) st (const AddingIngredients)（其他配料同理）中对 st 加入适当的约束条件——即 lettuce st = False。 - user2407038

Answer 1

< p > 索引状态单子 正好满足这一点。

< p > 常规的 State s 单子模型是一个状态机（具体而言是一个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。

但有时候（比如在你的情况下），我们需要中间状态的类型不同。这就是索引状态单子（Indexed State Monad）发挥作用的地方。它有两个状态字母表。IxState i j a 模拟了一个起始状态必须在 i 中，结束状态在 j 中的状态机：

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

常规的State s单子与IxState s 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 不完全是一个单子，而是一个索引单子。

现在我们只需要一种方法来指定我们状态的类型约束。对于沙拉示例，我们希望得到类似这样的东西：

mix :: IxState (Salad r) Ready ()

这是一台机器，其输入状态为某个不完整的包含成分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

现在我们可以重复以上步骤来处理番茄和黄瓜。

现在，mix 的类型只需要是：

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

如果我们尝试混合任何未按照顺序添加 Lettuce, Cucumber, 和 Tomato 的沙拉，就会出现类型错误。例如，以下内容将会出现类型错误：

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 的 y ': xs 的元素。使用 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

- Apocalisp

---

这看起来是一个很好的答案，但你能再解释一下吗？ - AJF

你能稍微解释一下你想要解释什么吗？ - Apocalisp

什么是索引状态单子（indexed state monad）？它在内部如何工作？这段代码中到底发生了什么？我能看出一些小步骤，但 IxState 仍然不透明。 - AJF

你并没有真正使用你的索引状态单子中的_monad_部分。所有的操作都返回 ()，所以它只是一个混淆的 ->。此外，当你尝试实际使用定义的 Elem 时，我认为你会遇到由于重叠实例而导致的问题，就像我在我的答案中概述的那样。 - Benjamin Hodgson

我这里没有使用单子，但是我假设在一个真正的程序中，你会想要使用 IxStateT 与一些其他依赖于状态的单子一起使用。 - Apocalisp

谢谢@Apocalisp，我曾考虑过IxMonad和Super monads，但没有考虑过更具体的IxState，这打开了全新的世界！ - Josh.F

Answer 2

您的问题有点含糊不清，但我理解为“如何逐步构建异构的'上下文'并在正确类型的值在范围内时创建记录？”这是我如何处理这个问题的方法：与其通过某些单调上下文穿越输入和输出类型，我们只需使用普通函数。如果您想使用聪明的类型级机器，可以将它用于传递的值，而不是围绕特定的计算概念构建程序结构。

够啰嗦了。我将把异构上下文表示为嵌套元组。我将使用单元（()）表示空上下文，并通过将上下文嵌套到新元组的左元素中来向上下文添加类型。因此，包含一个Int，一个Bool和一个Char的上下文看起来像这样：

type IntBoolChar = ((((), Int), Bool), Char)

希望您能够逐步向沙拉碗中添加配料，以下是示例：

-- we will *not* be using this type like a state monad
addLettuce :: a -> (a, Lettuce)
addLettuce = (, Romaine)

addOlives :: a -> (a, Olive)
addOlives = (, Kalamata)

addCheese :: a -> (a, Cheese)
addCheese = (, Feta)

addGreekSaladIngredients :: a -> (((a, Lettuce), Olive), Cheese)
-- yes, i know you also need tomatoes and onions for a Greek salad. i'm trying to keep the example short
addGreekSaladIngredients = addCheese . addOlives . addLettuce

这不是高级类型魔法。它适用于任何使用元组的语言。我甚至在C#中设计了基于这个想法的真实世界API，部分补偿了C#在柯里化方面的不足，当您可能会在Haskell中使用Applicative语法时。这里有一个例子来自我的解析器组合库：从一个空置的排列解析器开始，您Add多个不同类型的原子解析器，然后Build一个以无序方式运行这些解析器的解析器，返回其结果的嵌套元组，然后可以手动展开。

---

另一半问题是如何将这种上下文的值转换为记录。

data Salad = Salad {
    _lettuce :: Lettuce,
    _olive :: Olive,
    _cheese :: Cheese
}

你可以使用以下简单的类，以一种无序的方式将嵌套元组通用地映射到记录中：

您可以使用以下简单的类，以一种无序的方式将嵌套元组通用地映射到记录中：

class Has a s where
    has :: Lens' s a

-- this kind of function can be written generically using TH or Generics
toSalad :: (Has Lettuce s, Has Olive s, Has Cheese s) => s -> Salad
toSalad x = Salad (x^.has) (x^.has) (x^.has)

这是对由Template Haskell生成的lens的HasX类的简单概括。

唯一需要一些类型技巧的部分是自动实例化嵌套元组的Has。我们需要区分两种情况：要查找的类型的项是在一对右侧，还是在左侧的嵌套元组内的某个位置。问题在于，在普通情况下，这两种情况看起来对扩展器是相同的：实例解析通过语法类型匹配的简单过程进行；类型等式不会被检查，也不会发生回溯。

结果是，我们需要高级重叠技巧。简而言之，该技巧使用封闭的类型族根据类型等式分派类型类。我们在两个选择中进行选择，因此这是很少有的几种情况之一，可以接受类型级布尔。

type family Here a as where
    Here a (_, a) = True
    Here a (_, b) = False

class Has' (here :: Bool) a s where
    has' :: Proxy here -> Lens' s a

instance Has' True a (as, a) where
    has' _ = _2
instance Has a as => Has' False a (as, b) where
    has' _ = _1.has

instance Has' (Here a (as, b)) a (as, b) => Has a (as, b) where
    has = has' (Proxy :: Proxy (Here a (as, b)))

这个程序会在第一个匹配类型时停止搜索。如果你的沙拉需要两种不同类型的莴苣，你必须将其中一种包装在newtype中。实际上，当你将这个缺点与重叠实例的复杂性结合起来时，我并不认为Has抽象是值得的。我只会手动展开元组：

toSalad :: (((a, Lettuce), Olive), Cheese) -> Salad
toSalad (((_, l), o), c) = Salad l o c

你会失去对顺序的不敏感性。

以下是一个使用示例：

greekSalad = toSalad $ addGreekSaladIngredients ()

ghci> greekSalad
Salad {_lettuce = Romaine, _olive = Kalamata, _cheese = Feta}  -- after deriving Show

---

这是完成的程序

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Control.Lens hiding (has, has')
import Data.Proxy

data Lettuce = Romaine deriving (Show)
data Olive = Kalamata deriving (Show)
data Cheese = Feta deriving (Show)

data Salad = Salad {
    _lettuce :: Lettuce,
    _olive :: Olive,
    _cheese :: Cheese
} deriving (Show)

-- we will *not* be using this type like a state monad
addLettuce :: a -> (a, Lettuce) -- <<< Tuple Sections
addLettuce = (, Romaine)

addOlives :: a -> (a, Olive)
addOlives = (, Kalamata)

addCheese :: a -> (a, Cheese)
addCheese = (, Feta)

addGreekSaladIngredients :: a -> (((a, Lettuce), Olive), Cheese)
addGreekSaladIngredients = addCheese . addOlives . addLettuce

class Has a s where
  has :: Lens' s a

type family Here a as where
    Here a (_, a) = True
    Here a (_, b) = False

class Has' (here :: Bool) a s where
    has' :: Proxy here -> Lens' s a

instance Has' True a (as, a) where
    has' _ = _2

instance Has a as => Has' False a (as, b) where
    has' _ = _1.has

instance  Has' (Here a (as, b)) a (as, b) => Has a (as, b) where -- <<< Undecidable Instances
    has = has' (Proxy :: Proxy (Here a (as, b)))

toSalad :: (Has Lettuce s, Has Olive s, Has Cheese s) => s -> Salad
toSalad x = Salad (x ^. has) (x ^. has) (x ^. has)

greekSalad = toSalad $ addGreekSaladIngredients ()

-- nonSaladsError = toSalad $ (addCheese . addOlives) ()

- Benjamin Hodgson

---

Haskell社区似乎对布尔类型家族有一种痴迷的情结。不要使用它们！ :) - Apocalisp

哈哈，你用我的话反驳我了！类型级别布尔值（作为证据传递的替代品）的问题在于它们会擦除信息 - 即在这种情况下的类型相等性 - 然后你发现自己需要在这一行中恢复它。但是在这里，我想要擦除那些信息 - 我需要合成一个具体类型以影响实例匹配。换句话说，我只是在两个选择之间做出选择，而不是试图通过系统传播信息。如果我在三个选择之间进行选择，我会使用某些三值类型。 - Benjamin Hodgson

我正在努力复现你的代码，特别是 Has 的最终实例。在一系列 pragma 后，我得到了 "Here is not injective... AllowAmbigousTypes" 的错误提示，如果我这样做，它无法看到类型变量从实例声明传递到 has 函数。我尝试了显式的 forall，但是没有成功... 有什么帮助吗？ - Josh.F

@Josh.F 你打开了ScopedTypeVariables吗？ - Benjamin Hodgson

哦，我之前有过，但现在我再试一次，它可以正常工作了...谢谢，如果你愿意，我在回答的结尾添加了完整的程序（仍需同行评审）。 - Josh.F

@Josh.F 谢谢！已批准。 - Benjamin Hodgson