如何在Haskell/Idris中使用约束有限状态机？

Question

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

问题的TLDR:我怎样才能从FSM表示组合爆炸的第一张图片到第二张图片,在那里您只需要在继续之前访问所有这些图片.

---

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

在下图中,有一个Initial州,3个临时州A, B, C和一个Final州.如果我没有弄错,在"正常"FSM中,您将始终需要n!临时状态来表示可能路径的每个组合.

这是不可取的.

相反,使用Type Families和可能的Dependent类型,我认为应该有一种状态可以随身携带,只有当它通过某些谓词时才允许你进入最终状态.(这是否会使自动推送自动机而不是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,也许使用Indexed Monads？

Answer 1

该索引状态单子正是这样做的.

常规State smonad模拟状态机(特别是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的用武之地.它有两个状态字母表.IxState i j a模拟一个机器,其启动状态必须处于i和结束状态将在j:

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

常规State smonad相当于IxState s s.我们可以IxState轻松地创作State.实现与以前相同,但类型签名更通用:

(>>>=) :: 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

我们可以为番茄和黄瓜重复相同的操作.

现在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 ': 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

Answer 2

Your question is a little vague, but I read it as "how can I incrementally build a heterogeneous 'context' and create a record once I have values of the correct types in scope?" Here's how I'd skin this particular cat: rather than threading input and output types through some monadic context, let's just work with ordinary functions. If you want to use clever type-level machinery, you can use it with the values you pass around, rather than structure your program around a particular notion of computation.

Enough waffling. I'm going to represent a heterogeneous context as a nested tuple. I'll use the unit (()) to represent an empty context, and I'll add types to the context by nesting the context into the left element of a new tuple. So, a context containing an Int, a Bool and a Char looks like this:

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

Hopefully you can see how you'd incrementally add ingredients to a salad bowl:

-- 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

This is not advanced type magic. It'll work in any language with tuples. I've even designed real-world APIs around this idea in C#, to partially compensate for C#'s lack of currying when you might use Applicative syntax in Haskell. Here's an example from my parser combinator library: starting with an empty permutation parser, you Add a number of atomic parsers of different types, and then Build a parser which runs those parsers in an order-insensitive manner, returning a nested tuple of their results which you can then flatten by hand.

The other half of the question was about turning a value of this sort of context into a record.

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

You can generically map nested tuples onto a record like this in an order-insensitive way using the following simple class:

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)

(This is a straightforward generalisation of the HasX classes that lens generates with Template Haskell.)

The only part which requires some type cleverness is automatically instantiating Has for nested tuples. We need to distinguish between two cases: either an item of the type we're looking for is on the right of a pair, or it's somewhere inside the nested tuple on the left of the pair. The problem is that under ordinary circumstances these two cases look the same to the elaborator: instance resolution occurs by a simple-minded process of syntactic type matching; type equalities aren't inspected and backtracking doesn't happen.

The upshot is that we need The Advanced Overlap Trick. Briefly, the trick uses a closed type family to dispatch a type class based on a type equality. We're choosing between two alternatives, so this is one of the few cases when a type-level boolean is acceptable.

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)))

This program will stop the search at the first matching type. If you need two different types of lettuce in your salad, you'll have to wrap one in a newtype. In practice, when you combine this disadvantage with the complexity of the overlapping instances, I'm not convinced the Has abstraction pays its way. I'd just flatten the tuple by hand:

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

You do lose order-insensitivity though.

Here's an example usage:

greekSalad = toSalad $ addGreekSaladIngredients ()

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

And here's the completed program

{-# 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) ()