重新绑定索引monad的表示法

Question

我正在关注Conor McBride的"Kleisli箭头的令人发指的财富"论文,我在这里发布了我的代码实现.简而言之,他定义了以下类型和类:

type a :-> b = forall i . a i -> b i

class IFunctor f where imap :: (a :-> b) -> (f a :-> f b)

class (IFunctor m) => IMonad m where
    skip :: a :-> m a
    bind :: (a :-> m b) -> (m a :-> m b)

data (a := i) j where
    V :: a -> (a := i) i

然后他定义了两种类型的绑定,后者(:=)用于限制初始索引:

-- Conor McBride's "demonic bind"
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(?>=) = flip bind

-- Conor McBride's "angelic bind"   
(>>=) :: (IMonad m) => m (a := j) i -> (a -> m b j) -> m b i
m >>= f = bind (\(V a) -> f a) m

后者绑定工作重新绑定完全正常do使用的符号索引的单子与RebindableSyntax扩展,使用下面的相应定义为return和fail:

return :: (IMonad m) => a -> m (a := i) i
return = skip . V

fail :: String -> m a i
fail = error

...但问题是我不能让前绑定(即(?>=))工作.我试着定义(>>=)并return成为:

(>>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(>>=) = (?>=)

return :: (IMonad m) => a :-> m a
return = skip

然后我创建了一个保证存在特定索引的数据类型:

data Unit a where
    Unit :: Unit ()

但是,当我尝试重新绑定do使用新定义的符号(>>=)和return,这是行不通的,如下面的例子演示:

-- Without do notation
test1 = skip Unit >>= \Unit -> skip Unit

-- With do notation
test2 = do
    Unit <- skip Unit
    skip Unit

test1类型检查,但test2没有,这是奇怪的,因为我觉得所有RebindableSyntax所做的就是让do符号desugar test2到test1,因此,如果test1类型检查,那么为什么不test2？我得到的错误是:

Couldn't match expected type `t0 -> t1'
            with actual type `a0 :-> m0 b0'
Expected type: m0 a0 i0 -> (t0 -> t1) -> m Unit ()
  Actual type: m0 a0 i0 -> (a0 :-> m0 b0) -> m0 b0 i0
In a stmt of a 'do' block: Unit <- skip Unit
In the expression:
  do { Unit <- skip Unit;
       skip Unit }

即使我使用显式forall语法而不是:->类型运算符,错误仍然存​​在.

现在,我知道使用"恶魔绑定"还有另一个问题,那就是你无法定义(>>),但我仍然想知道我能走多远.谁能解释为什么我不能让GHC去除"恶魔绑定",即使它通常会进行类型检查？

Answer 1

IIUC,GHC desugarer实际上运行在 typechecker (源)之后.这就解释了为什么你观察到的情况在理论上是可能的.类型检查器可能有一些特殊的输入规则,这些规则可能与类型检查器对desugarred代码的处理方式不一致.

当然,期望它们保持一致是合理的,所以我建议提交GHC错误.