22

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

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，使用以下相应的定义returnand 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 ()

但是，当我尝试使用 and 的新定义重新绑定符号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符号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 对“恶魔绑定”进行脱糖，即使它通常会进行类型检查？

4

1 回答 1

10

IIUC，GHC desugarer 实际上在类型检查器（源代码）之后运行。这就解释了为什么你观察到的情况在理论上是可能的。类型检查器可能对 do-notation 有一些特殊的类型规则，这些规则可能与类型检查器对去糖代码的处理方式不一致。

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

于 2012-06-16T00:19:30.863 回答