haskell - 在生产中使用索引单子(monad)的经验报告？

Question

在上一个问题中，我发现了 Conor McBride 的 Kleisli arrows of Outrageous Fortune 的存在。在寻找编码方式时Idris examples in Haskell .我努力理解 McBride 的代码并使其在 Haskell 中编译得到了这个要点:https://gist.github.com/abailly/02dcc04b23d4c607f33dca20021bcd2f

在搜索 Hackage 时，我发现了这些概念的几个实现，特别是(猜猜是谁？)Edward Kmett和 Gabriel Gonzalez .

人们将此类代码投入生产有什么经验？特别是，预期的好处(运行时安全性、自我指导使用)是否真的会发生 IRL？随着时间的推移维护这种代码并让新人入职怎么样？

编辑:我将标题更改为更明确地说明我在寻找什么:在野外使用索引单子(monad)的真实世界。我对使用它们很感兴趣，并且我想到了几个用例，只是想知道其他人是否已经在“生产”代码中使用过它们。

编辑 2:感谢迄今为止提供的出色答案和有用的评论，我再次编辑了该问题的标题和描述，以更准确地反射(reflect)我期望的答案类型，例如经验报告。

Answer 1

session 类型试图为网络协议(protocol)提供类型级别的描述。这个想法是，如果客户端发送一个值，服务器必须准备好接收它，反之亦然。

所以这里有一个类型(使用 TypeInType )描述由一系列要发送的值和要接收的值组成的 session 。

infixr 5 :!, :?
data Session = Type :! Session
             | Type :? Session
             | E

a :! s表示“发送类型为 a 的值，然后继续使用协议(protocol) s”。 a :? s表示“接收 a 类型的值，然后继续使用协议(protocol) s”。

所以 Session表示一个(类型级别的) Action 列表。我们的一元计算将沿着这个列表工作，根据类型的需要发送和接收数据。更具体地说，类型为 Chan s t a 的计算从 s 减少为满足协议(protocol)而需要完成的剩余工作至 t .我会 build Chan使用我在回答您的其他问题时使用的索引免费单子(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


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 fx) = IFree (imap (imap f) fx)

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

我们在 Chan 中的基本操作monad 将简单地发送和接收值。

data ChanF s t r where
    Send :: a -> r -> ChanF (a :! s) s r
    Recv :: (a -> r) -> ChanF (a :? s) s r

instance IFunctor ChanF where
    imap f (Send x r) = Send x (f r)
    imap f (Recv r) = Recv (fmap f r)

send :: a -> Chan (a :! s) s ()
send x = IFree (Send x (IReturn ()))

recv :: Chan (a :? s) s a
recv = IFree (Recv IReturn)

type Chan = IFree ChanF
type Chan' s = Chan s E  -- a "complete" Chan

send从 a :! s 获取 session 的当前状态至 s ，履行发送 a的义务.同样， recv从 a :? s 转换 session 至 s .

这是有趣的部分。当协议(protocol)的一端发送一个值时，另一端必须准备好接收它，反之亦然。这导致了 session 类型对偶的想法:

type family Dual s where
    Dual (a :! s) = a :? Dual s
    Dual (a :? s) = a :! Dual s
    Dual E = E

总语言 Dual (Dual s) = s将是可证明的，但唉，Haskell 不是完全的。

如果它们的类型是双 channel ，您可以连接一对 channel 。 (我猜你会称之为连接客户端和服务器的内存模拟。)

connect :: Chan' s a -> Chan' (Dual s) b -> (a, b)
connect (IReturn x) (IReturn y) = (x, y)
connect (IReturn _) (IFree y) = case y of {}
connect (IFree (Send x r)) (IFree (Recv f)) = connect r (f x)
connect (IFree (Recv f)) (IFree (Send y r)) = connect (f y) r

例如，这是一个用于测试数字是否大于 3 的服务器协议(protocol)。服务器等待接收 Int。 , 发回 Bool , 然后结束计算。

type MyProtocol = Int :? Bool :! E

server :: Chan' MyProtocol ()
server = do  -- using RebindableSyntax
    x <- recv
    send (x > 3)

client :: Chan' (Dual MyProtocol) Bool
client = do
    send 5
    recv

并对其进行测试:

ghci> connect server client
((),True)

session 类型是一个活跃的研究领域。这种特殊的实现对于非常简单的协议(protocol)来说是很好的，但是你不能描述通过线路发送的数据类型取决于协议(protocol)状态的协议(protocol)。为此，您需要惊喜、依赖类型。见 this talk by Brady快速演示最先进的 session 类型。