如何编码类型中可能的状态转换？ [英] How to encode possible state transitions in type?

问题描述

 数据我试图在Haskell中复制这段Idris代码，它通过类型强制执行正确的操作顺序： DoorState = DoorClosed | DoorOpen 
 data DoorCmd：类型 - > 
 DoorState  - > 
 DoorState  - > 
类型其中
打开：DoorCmd（）DoorClosed DoorOpen 
 Close：DoorCmd（）DoorOpen DoorClosed 
 RingBell：DoorCmd（）DoorClosed DoorClosed 
 Pure：ty  - > DoorCmd ty状态状态
（>> =）：DoorCmd a state1 state2  - > 
（a  - > DoorCmd b state2 state3） - > 
 DoorCmd b state1 state3 
  

感谢重载（> > =）运算符，可以写如下一元代码：

  do Ring 
打开
关闭
  

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

 做圆环
打开
圆环
打开
  

我试图在下面的Haskell片段中遵循这个模式：

  data DoorState =关闭|打开
 
数据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 bfy 
 
实例Functor（DoorCommand be）其中
f`fmap` c =绑定c（\ x  - > Pure（fx））
 
  - 实例Applicative（DoorCommand be）其中
  -  pure = Pure 
  -  f * x = Bind f（\ f' - > Bind x（\ x' - > Pure（f'x'）））
 
  -  instance Monad（DoorCommand be）其中
  -  return = Pure 
  - （>> =）=绑定
  

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

我如何编写此代码以便能够使用符号，例如阻止命令 s？

解决方案

无效序列寻找的确是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其中
 ireturn :: a  - > m i i a 
（>>> =）:: m i j a  - > （a  - > m j k b） - > mikb 
  

IMonad 是monad-像 m :: k - > k - > * - > * 通过属于 k 类型的有向图来描述路径。 >>> = 将类型级别的计算从 i 绑定到<$ c $将它从 j 更改为 k ，并返回一个更大的值从 i 到 k 的计算。 ireturn 允许您将一个纯粹的值提升为不会改变类型级别状态的monadic计算。

我将使用索引空闲monad 来捕获这种请求 - 响应操作的结构，主要是因为我不想弄清楚如何编写<$ c

 数据IFree fija其中
 IReturn  $ c> IMonad  :: a  - > IFree f我是a 
 IFree :: f i j（IFree f j k a） - > IFree f i k a 
 
实例IFunctor f => IFunctor（IFree f）其中
 imap f（IReturn x）= IReturn（f x）
 imap f（IFree ff）= IFree $ imap（imap f）ff 
 instance IFunctor f => IMonad（IFree f）其中
 ireturn = IReturn 
 IReturn x>> = f = fx 
 IFree ff>>> = f = IFree $ imap（> >> = f）ff 
  

我们可以建立 code> monad免费获得以下函数：



  data DoorState = Opened |已关闭
数据DoorF i j next其中
打开::下一个 - > DoorF关闭打开下一个
关闭::下一个 - > DoorF开放关闭
 Ring :: next  - > （Fx）
 imap f（关闭x）=关闭（fx）
 imap f（Ring x）= Ring（fx）
 
类型Door = IFree DoorF 
 
 open :: Door Closed Opened（）
 open = IFree（Open IReturn（）））
 close :: Door Closed Closed（）
 close = IFree（Close（IReturn（）））
 ring :: Door Closed Closed（）
 ring = IFree（Ring（IReturn（）））
  

您可以打开一扇门，导致当前关闭的门打开，关闭当前打开的门，或 ring 门的铃铛保持关闭，大概是因为房子的占有者不想看到你。

最后， RebindableSyntax 语言扩展意味着我们可以用我们自己定制的 IMonad 替换标准 Monad 类。 / b>

 （>> =）=（>>> =）
m>> n = m>>> = const n 
 return = ireturn 
 fail = undefined 
 
 door :: Door Open Open（）
 door = do 
 close 
 ring 
 open 
  

---

但是我注意到你并没有真的使用monad的绑定结构。您的任何积木都不是打开，关闭或戒指返回一个值。所以我认为你真正需要的是以下简单的类型对齐列表类型：

  data Path gij where 
 Nil :: Path gii 
 Cons :: gij  - >路径g j k  - >路径gik 
  

操作上， Path ::（k - > k - > ; *） - > k - > k - > * 就像一个链表，但它有一些额外的类型级别的结构，再次通过一个有向图描述一个路径，其节点在 k 。列表中的元素是边 g 。 Nil 表示您始终可以从节点 i 自身找到路径， Cons 提醒我们，千里之行始于一步：如果你的边缘从 i 到 j 和一个从 j 到 k 的路径，您可以将它们合并为一个从 i 至 k 。它被称为类型对齐列表，因为一个元素的结束类型必须与下一个元素的开始类型相匹配。

另一方面Curry-Howard Street，如果 g 是一个二元逻辑关系，那么 Path g 构造它的反射传递闭包的。或者，断定 Path g 是图的空闲类中的态射的类型 g 。

 实例类别（路径g）其中$ b（自由类型）中的态射只是（翻转的）追加类型对齐的列表。 $ b id =无
 xs。无= xs 
 xs。我们可以写门以路径：
 数据DoorAction ij其中
打开:: DoorAction关闭打开
关闭:: DoorAction打开关闭
 Ring :: DoorAction关闭关闭
 
类型Door =路径DoorAction 
 
开启::关闭开启
开启=缺省开启无
关闭::开启已关闭
关闭=缺省关闭无
响铃::开启关闭
 ring =缺环无b 
 $ b门::开门打开
门=开。环。关闭
  
您不会得到 do  notation （尽管我认为  RebindableSyntax 允许你重载列表文字），但是用（。）看起来像是纯函数的排序，我认为这对你正在做的事情来说是一个很好的类比。对我而言，它需要额外的智力 - 一种罕见而珍贵的自然资源 - 使用索引单子。当一个简单的结构可以做到的时候，避免monad的复杂性会更好。 
I am trying to replicate in Haskell this piece of Idris code, which enforces correct sequencing of actions through types:
 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
Thanks to overloading of (>>=) operator, one can write monadic code like:
do Ring 
   Open 
   Close
but compiler rejects incorrect transitions like:
do Ring
   Open 
   Ring
   Open
I have tried to follow this pattern in the following Haskell fragment:
 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
But of course this fails: The Applicative and Monad instances cannot be defined correctly as they require two different instances to properly sequence operations. The constructor Bind can be used to enforce proper sequencing but I cannot manage to use the "nicer" do-notation. 

How could I write this code to be able to use do-notation, e.g. to prevent invalid sequences of Commands ?
解决方案
What you're looking for is indeed Atkey's parameterised monad, now more commonly known as the 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 is the class of monad-like things m :: k -> k -> * -> * describing paths through a directed graph of types belonging to the kind k. >>>= binds a computation which takes the type-level state from i to j into a computation which takes it from j to k, returning a bigger computation from i to k. ireturn allows you to lift a pure value into a monadic computation which doesn't change the type-level state.

I'm going to use the indexed free monad to capture the structure of this sort of request-response action, largely because I don't want to have to figure out how to write the IMonad instance for your type myself:
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
We can build your Door monad for free from the following functor:
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 ()))
You can open a door, which causes a currently-closed door to become open, close a currently-open door, or ring the bell of a door which remains closed, presumably because the house's occupant doesn't want to see you.

Finally, the RebindableSyntax language extension means we can replace the standard Monad class with our own custom IMonad.
(>>=) = (>>>=)
m >> n = m >>>= const n
return = ireturn
fail = undefined

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




However I notice that you're not really using the binding structure of your monad. None of your building blocks Open, Close or Ring return a value. So I think what you really need is the following, simpler 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
Operationally, Path :: (k -> k -> *) -> k -> k -> * is like a linked list, but it has some extra type-level structure, once again describing a path through a directed graph whose nodes are in k. The elements of the list are edges g. Nil says you can always find a path from a node i to itself and Cons reminds us that a journey of a thousand miles begins with a single step: if you have an edge from i to j and a path from j to k, you can combine them to make a path from i to k. It's called a type-aligned list because the ending type of one element must match the starting type of the next.

On the other side of Curry-Howard Street, if g is a binary logical relation then Path g constructs its reflexive transitive closure. Or, categorically, Path g is the type of morphisms in the free category of a graph g. Composing morphisms in the free category is just (flipped) appending type-aligned lists.
instance Category (Path g) where
    id = Nil
    xs . Nil = xs
    xs . Cons y ys = Cons y (xs . ys)
Then we can write Door in terms of 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
You don't get do notation (though I think RebindableSyntax does allow you to overload list literals), but building computations with (.) looks like sequencing of pure functions, which I think is a rather good analogy for what you're doing anyway. For me it requires extra brainpower - a rare and precious natural resource - to use indexed monads. It's better to avoid the complexity of monads when a simpler structure will do.

                        
这篇关于如何编码类型中可能的状态转换？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！