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

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可用于强制执行正确的排序,但我无法使用"更好"的标记.

我怎么能写这段代码才能使用do-notation,例如防止Commands的无效序列？

Answer 1

您正在寻找的确实是Atkey的参数化monad,现在通常被称为索引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 -> * -> *通过属于该类型的有向图来描述路径k.>>>=结合一个计算这需要从类型电平状态i,以j成一个计算这需要从它j到k,从返回一个更大的计算i来k.ireturn允许您将纯值提升为不会更改类型级别状态的monadic计算.

我将使用索引的免费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语言扩展意味着我们可以用Monad自己的自定义替换标准类IMonad.

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

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

但是我注意到你并没有真正使用monad的绑定结构.没有你的构建块Open,Close或Ring返回一个值.所以我认为你真正需要的是以下更简单的类型对齐列表类型:

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到j并从路径j到k,你可以将它们结合起来,使从路径i到k.它被称为类型对齐列表,因为一个元素的结束类型必须与下一个元素的起始类型匹配.

在Curry-Howard Street的另一边,if g是一个二元逻辑关系,然后Path g构造它的自反传递闭包.或者,断然地,Path g是图的自由类别中的态射类型g.在自由类别中组合态射只是(翻转)附加类型对齐列表.

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

然后,我们可以写Door在以下方面Path:

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的复杂性.