为索引单子重新绑定 do 表示法

Question

我正在关注 Conor McBride 的“Kleisli arrows of outrageous fortune”论文，并且我已经发布了我对他的代码的实现 here。简而言之，他定义了以下类型和类：

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 扩展名的索引monad，使用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 ()

但是当我尝试使用 (>>=) 和 return 的新定义重新绑定 do 表示法时，它不起作用，如下例所示：

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

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

test1 类型检查，但 test2 没有，这很奇怪，因为我认为 RebindableSyntax 所做的只是让 do 符号脱糖 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 实际上在类型检查器 (source) 之后运行。这就解释了为什么你观察到的情况在理论上是可能的。类型检查器可能对 do-notation 有一些特殊的键入规则，这些规则可能与类型检查器对脱糖代码的处理方式不一致。

当然，期望它们保持一致是合理的，因此我建议提交 GHC 错误。