相关疑难解决方法(0)

什么是索引monad和这个monad的动机？

我已经读过它有助于跟踪副作用.但类型签名和文档并没有把我带到任何地方.

什么是如何帮助跟踪副作用(或任何其他有效的例子)的例子？

我试图在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 …

类型构造函数生成给定类型的类型.例如,Maybe构造函数

data Maybe a = Nothing | Just a

可能是一个给定的具体类型,如Char,并给出一个具体类型,如Maybe Char.在种类方面,有一个

GHCI> :k Maybe
Maybe :: * -> *

我的问题:是否可以定义一个类型构造函数,在给定Char的情况下产生具体类型,比如说？换句话说,是否可以在类型构造函数的类型签名中混合种类和类型？就像是

GHCI> :k my_type
my_type :: Char -> * -> *