如何编码类型中可能的状态转换？

Question

我正在尝试在 Haskell 中复制这段 Idris 代码，它通过类型强制执行正确的操作顺序：

 data DoorState = DoorClosed | DoorOpen
 data DoorCmd : Type ->
                DoorState ->
 DoorState ->
                Type where
      Open : DoorCmd     () DoorClosed DoorOpen
      Close : DoorCmd    () DoorOpen   DoorClosed
      RingBell : DoorCmd () DoorClosed DoorClosed
      Pure : ty -> DoorCmd ty state state
      (>>=) : DoorCmd a state1 state2 ->
              (a -> DoorCmd b state2 state3) ->
              DoorCmd b state1 state3

多亏了 (>>=) 运算符的重载，我们可以编写像这样的 monadic 代码：

do Ring 
   Open 
   Close

但编译器会拒绝不正确的转换，例如：

do Ring
   Open 
   Ring
   Open

我已尝试在以下 Haskell 片段中遵循此模式：

 data DoorState = Closed | Opened

 data DoorCommand (begin :: DoorState) (end :: DoorState) a where
   Open  :: DoorCommand 'Closed 'Opened ()
   Close :: DoorCommand 'Opened 'Closed ()
   Ring  :: DoorCommand 'Closed 'Closed ()

   Pure  :: x -> DoorCommand b e x
   Bind  :: DoorCommand b e x -> (x -> DoorCommand e f y) -> DoorCommand b f y

 instance Functor (DoorCommand b e) where
   f `fmap` c = Bind c (\ x -> Pure (f x))

 -- instance Applicative (DoorCommand b e) where
 --    pure    = Pure
 --    f <*> x = Bind f (\ f' -> Bind x (\ x' -> Pure (f' x')))

 -- instance Monad (DoorCommand b e) where
 --   return = Pure
 --   (>>=) = Bind

但这当然失败了：无法正确定义 Applicative 和 Monad 实例，因为它们需要两个不同的实例才能正确排序操作。构造函数 Bind 可用于强制执行正确的排序，但我无法设法使用 "nicer" do-notation。

我如何编写此代码才能使用 do-notation，例如防止 Commands ?

的无效序列

Answer 1

您正在寻找的确实是 Atkey 的 parameterised monad，现在通常称为 indexed monad。

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

IMonad 是类 monad 事物 m :: k -> k -> * -> * 的 class，描述了属于 k 类型的有向图的路径。 >>>= 将类型级状态从 i 到 j 的计算绑定到从 j 到 k 的计算中，return 从 i 到 k 进行更大的计算。 ireturn 允许您将纯值提升到不改变类型级状态的单子计算中。

我将使用 indexed free monad 来捕获这种请求-响应操作的结构，主要是因为我不想弄清楚如何自己为您的类型编写 IMonad 实例：

data IFree f i j a where
    IReturn :: a -> IFree f i i a
    IFree :: f i j (IFree f j k a) -> IFree f i k a

instance IFunctor f => IFunctor (IFree f) where
    imap f (IReturn x) = IReturn (f x)
    imap f (IFree ff) = IFree $ imap (imap f) ff
instance IFunctor f => IMonad (IFree f) where
    ireturn = IReturn
    IReturn x >>>= f = f x
    IFree ff >>>= f = IFree $ imap (>>>= f) ff

我们可以通过以下仿函数免费构建您的 Door monad：

data DoorState = Opened | Closed
data DoorF i j next where
    Open :: next -> DoorF Closed Opened next
    Close :: next -> DoorF Opened Closed next
    Ring :: next -> DoorF Closed Closed next

instance IFunctor DoorF where
    imap f (Open x) = Open (f x)
    imap f (Close x) = Close (f x)
    imap f (Ring x) = Ring (f x)

type Door = IFree DoorF

open :: Door Closed Opened ()
open = IFree (Open (IReturn ()))
close :: Door Opened Closed ()
close = IFree (Close (IReturn ()))
ring :: Door Closed Closed ()
ring = IFree (Ring (IReturn ()))

你可以open一扇门，它会导致当前关闭的门打开，close一扇当前打开的门，或者ring一扇门的铃铛关门了，估计是房主不想见你吧。

最后，RebindableSyntax 语言扩展意味着我们可以用我们自己的自定义 IMonad.

替换标准 Monad class

(>>=) = (>>>=)
m >> n = m >>>= const n
return = ireturn
fail = undefined

door :: Door Open Open ()
door = do
    close
    ring
    open

但是我注意到您并没有真正使用 monad 的绑定结构。 None 您的 Open、Close 或 Ring return 个值。所以我认为您真正需要的是以下更简单的 type-aligned list type:

data Path g i j where
    Nil :: Path g i i
    Cons :: g i j -> Path g j k -> Path g i k

在操作上，Path :: (k -> k -> *) -> k -> k -> * 就像一个链表，但它有一些额外的类型级结构，再次描述了通过节点在 k 中的有向图的路径。列表的元素是边g。 Nil 说你总能找到从节点 i 到它自己的路径，Cons 提醒我们千里之行始于足下：如果你有一条从 i 到它自己的路径=21=] 到 j 和一条从 j 到 k 的路径，你可以将它们组合成一条从 i 到 k 的路径。之所以称为 类型对齐列表，是因为一个元素的结束类型必须与下一个元素的开始类型匹配。

在 Curry-Howard 街的另一边，如果 g 是二元逻辑关系，则 Path g 构造其 自反传递闭包 。或者，明确地说，Path g 是图 g 的 自由范畴 中的态射类型。在自由类别中组合态射只是（翻转）附加类型对齐列表。

instance Category (Path g) where
    id = Nil
    xs . Nil = xs
    xs . Cons y ys = Cons y (xs . ys)

那么我们可以用Path写成Door:

data DoorAction i j where
    Open :: DoorAction Closed Opened
    Close :: DoorAction Opened Closed
    Ring :: DoorAction Closed Closed

type Door = Path DoorAction

open :: Door Closed Opened
open = Cons Open Nil
close :: Door Opened Closed
close = Cons Close Nil
ring :: Door Closed Closed
ring = Cons Ring Nil

door :: Door Open Open
door = open . ring . close

你没有得到 do 符号（虽然我认为 RebindableSyntax 确实允许你重载列表文字），但是用 (.) 看起来像是纯函数的排序，我认为这对你正在做的事情来说是一个很好的类比。对我来说，使用索引 monad 需要额外的脑力——一种稀有和宝贵的自然资源。当一个更简单的结构可以做到时，最好避免 monad 的复杂性。

如何编码类型中可能的状态转换？

How to encode possible state transitions in type?

haskell

types

idris