在生产中使用索引monad体验报告？

Question

在之前的一个问题中,我发现Conor McBride的Kleisli的Outrageous Fortune箭头的存在,同时寻找在Haskell中编码Idris示例的方法.我努力理解McBride的代码并使其在Haskell中编译导致了这个要点:https://gist.github.com/abailly/02dcc04b23d4c607f33dca20021bcd2f

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

人们将这些代码投入生产有什么经验？特别是,IRL实际发生了预期的好处(运行时安全性,自我指导使用)吗？如何随着时间的推移维护这种代码并加入新手？

编辑:我更改了标题,以更明确地了解我正在寻找的东西:在野外真实使用索引monad.我有兴趣使用它们,我有几个用例,只是想知道其他人是否已经在"生产"代码中使用过它们.

编辑2:由于到目前为止提供了很好的答案和有用的评论,我再次编辑了该问题的标题和描述,以更准确地反映我期望的答案,例如经验报告.

Answer 1

我认为下面应该算作一个实际的例子：在编译器中静态地强制执行“well-stackedness”。首先是样板：

{-# LANGUAGE GADTs, KindSignatures #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE RebindableSyntax #-}

import qualified Prelude
import Prelude hiding (return, fail, (>>=), (>>))

然后是一个简单的堆栈语言：

data Op (i :: [*]) (j :: [*]) where
    IMM :: a -> Op i (a ': i)
    BINOP :: (a -> b -> c) -> Op (a ': b ': i) (c ': i)
    BRANCH :: Label i j -> Label i j -> Op (Bool ': i) j

我们不会打扰真正的Labels：

data Label (i :: [*]) (j :: [*]) where
    Label :: Prog i j -> Label i j

ramsProg只是 s 的类型对齐列表Op：

data Prog (i :: [*]) (j :: [*]) where
    PNil :: Prog i i
    PCons :: Op i j -> Prog j k -> Prog i k

所以在这种设置下，我们可以很容易地制作一个编译器，它是一个索引编写器单子；也就是说，一个索引单子：

class IMonad (m :: idx -> idx -> * -> *) where
    ireturn :: a -> m i i a
    ibind :: m i j a -> (a -> m j k b) -> m i k b

-- For RebindableSyntax, so that we get that sweet 'do' sugar
return :: (IMonad m) => a -> m i i a
return = ireturn
(>>=) :: (IMonad m) => m i j a -> (a -> m j k b) -> m i k b
(>>=) = ibind
m >> n = m >>= const n
fail = error

允许累积一个（n索引）幺半群：

class IMonoid (m :: idx -> idx -> *) where
    imempty :: m i i
    imappend :: m i j -> m j k -> m i k

就像常规的一样Writer：

newtype IWriter w (i :: [*]) (j :: [*]) (a :: *) = IWriter{ runIWriter :: (w i j, a) }

instance (IMonoid w) => IMonad (IWriter w) where
    ireturn x = IWriter (imempty, x)
    ibind m f = IWriter $ case runIWriter m of
        (w, x) -> case runIWriter (f x) of
            (w', y) -> (w `imappend` w', y)

itell :: w i j -> IWriter w i j ()
itell w = IWriter (w, ())

所以我们只是将这个机制应用到Prog公羊上：

instance IMonoid Prog where
    imempty = PNil
    imappend PNil prog' = prog'
    imappend (PCons op prog) prog' = PCons op $ imappend prog prog'

type Compiler = IWriter Prog

tellOp :: Op i j -> Compiler i j ()
tellOp op = itell $ PCons op PNil

label :: Compiler i j () -> Compiler k k (Label i j)
label m = case runIWriter m of
    (prog, ()) -> ireturn (Label prog)

然后我们可以尝试编译一个简单的表达式语言：

data Expr a where
    Lit :: a -> Expr a
    And :: Expr Bool -> Expr Bool -> Expr Bool
    Plus :: Expr Int -> Expr Int -> Expr Int
    If :: Expr Bool -> Expr a -> Expr a -> Expr a

compile :: Expr a -> Compiler i (a ': i) ()
compile (Lit x) = tellOp $ IMM x
compile (And x y) = do
    compile x
    compile y
    tellOp $ BINOP (&&)
compile (Plus x y) = do
    compile x
    compile y
    tellOp $ BINOP (+)
compile (If b t e) = do
    labThen <- label $ compile t
    labElse <- label $ compile e
    compile b
    tellOp $ BRANCH labThen labElse

如果我们省略了例如 的参数之一BINOP，类型检查器将检测到这一点：

compile (And x y) = do
    compile x
    tellOp $ BINOP (&&)

• 无法i ~ (Bool : i) 从上下文中推断出：a ~ Bool