重新绑定为已编入索引的monad创建符号 [英] Rebinding do notation for indexed monads

问题描述

我正在关注Conor McBride的Kleisli愤怒的箭头这篇论文，并且我已经发布了他的代码这里。简而言之，他定义了以下类型和类：

  type a： - > b =全部我。一个i  - > b i 
 
 class IFunctor f where imap ::（a： - > b） - > （f a： - > f b）
 
 class（IFunctor m）=> IMonad m其中
 skip :: a： - > m a 
 bind ::（a： - > m b） - > （a： - > m b）
 
 data（a：= i）j其中
 V :: a  - > （a：= i）然后他定义了两种类型的绑定，后者使用  

code>（：=）来限制初始索引：

   -  Conor McBride's 恶魔绑定
（？> =）::（IMonad m）=> m a i  - > （a： - > m b） - > m b i 
（？> =）=翻转绑定
 
  -  Conor McBride的天使绑定
（>> =）::（IMonad m）=> m（a：= j）i  - > （a  - > m b j） - > mbi 
m>> = f = bind（\（V a） - > fa）m 
  

后面的绑定对于重新绑定 do 表示法使用带有 RebindableSyntax 扩展名的索引monad，对 return 和失败使用以下相应的定义：

  return ::（IMonad m）=> a  - > m（a：= i）i 
 return = skip。 V 
 
 fail :: String  - > mai 
 fail =错误
  

...但问题是我无法获得前者绑定（即（？> =））才能正常工作。我尝试将（>> =）和 return 定义为：

 （>> =）::（IMonad m）=> m a i  - > （a： - > m b） - > （b>> =）=（> =）
 
 return ::（IMonad m）=> a： - > ma 
 return = skip 
  

然后我创建了一个数据类型来保证特定的索引：

  data单元a其中
单元::单元（）
  

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

   - 无标记
 test1 =跳过单位>> = \单位 - >跳过单位
 
  - 带符号
 test2 = do 
单位<  - 跳过单位
跳过单位
  

test1 类型检查，但 test2 不，这很奇怪，因为我认为所有 RebindableSyntax 都是让 do notation desugar test2 到 test1 ，所以如果 test1 类型检查，那么为什么不 TEST2 ？我得到的错误是：

 无法匹配预期的类型`t0  - > t1'
与实际类型`a0： - > m0 b0'
预期类型：m0 a0 i0  - > （t 0  - > t 1） - > m单位（）
实际类型：m0 a0 i0  - > （a0：→m0 b0）→> m0 b0 i0 
在'do'块的单元中：单元<  - 跳过单元
在表达式中：
 do {单元<  - 跳过单元; 
跳过单元} 
  

即使我使用显式 forall 语法，而不是： - > 类型运算符

我知道使用恶魔绑定还有另一个问题，那就是你无法定义（>>），但我仍然想看看有多远我可以随它去。任何人都可以解释为什么我无法让GHC去解除恶魔般的绑定，即使它通常会进行类型检查？解析方案

IIUC，GHC解析器实际上在类型检查器之后运行（源）。这就解释了为什么你观察到的情况在理论上是可能的。 Typechecker可能有一些特殊的键符号输入规则，这些可能与typechecker对于desugarred代码的做法不一致。

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

I was following Conor McBride's "Kleisli arrows of outrageous fortune" paper and I've posted my implementation of his code here. Briefly, he defines the following types and classes:

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

Then he defines two types of binds, the latter of which uses (:=) to restrict the initial index:

-- 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

The latter bind works perfectly fine for rebinding do notation to use indexed monads with the RebindableSyntax extension, using the following corresponding definitions for return and fail:

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

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

... but the problem is that I cannot get the former bind (i.e. (?>=)) to work. I tried instead defining (>>=) and return to be:

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

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

Then I created a data type guaranteed to inhabit a specific index:

data Unit a where
    Unit :: Unit ()

But when I try to rebind do notation using the new definitions for (>>=) and return, it does not work, as demonstrated in the following example:

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

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

test1 type-checks, but test2 does not, which is weird, since I thought all that RebindableSyntax did was let do notation desugar test2 to test1, so if test1 type-checks, then why does not test2? The error I get is:

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 }

The error remains even when I use the explicit forall syntax instead of the :-> type operator.

Now, I know there is another problem with using the "demonic bind", which is that you can't define (>>), but I still wanted to see how far I could go with it. Can anybody explain why I cannot get GHC to desugar the "demonic bind", even when it would normally type-check?

解决方案

IIUC, the GHC desugarer actually runs after the typechecker (source). That explains why the situation you observe is theoretically possible. The typechecker probably has some special typing rules for the do-notation, and those may be inconsistent with what the typechecker would do with the desugarred code.

Of course, it's reasonable to expect them to be consistent, so I would recommend filing a GHC bug.

这篇关于重新绑定为已编入索引的monad创建符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！