削弱排名2类型的约束

Question

{-# LANGUAGE RankNTypes #-}

继续前一系列问题,我有一个带有通用量化函数作为参数的函数,如下所示:

emap :: (forall a. Expression a -> Expression a) -> Expression b -> Expression b

对于不需要额外约束的函数,可以使用哪个,例如:

postmap :: (forall a. Expression a -> Expression a) -> Expression b -> Expression b
postmap f = f . emap (postmap f)

reduce = postmap step

但是,我现在想要将此函数与带有附加约束的函数一起使用,但以下内容不进行类型检查.

substitute :: Pack a => Identifier -> a -> Expression a -> Expression a
substitute i v (Var x) | x == i = pack v
substitute _ _ x = x


bind :: Pack a => Identifier -> a -> Expression a -> Expression a
bind ident value = postmap (subsitute ident value)

所以我似乎需要以某种方式" forall a约束"或"专门化" 约束的 forall a. Pack a约束.这似乎是不必要的约束添加到签名emap本身,但我看不到任何其他的方法来解决这一点.

我不知道如何解决这个问题,但我可以看到一些选项.

1. 在签名周围添加约束bind,以便可以愉快地进行类型检查.
2. emap'使用约束创建另一个函数,并emap'以 emap反之亦然的方式实现(emap是一个无聊的机械定义,并且只有两个相同的函数体仅通过签名区分是没有意义的).
3. 认识到我正在尝试做的代码气味并继续使用替代解决方案.(???)

Answer 1

假设你重写了所有这些type T = forall a . Expression a -> Expression a和postmap' :: T -> T.我认为应该清楚的是,它的类型postmap是相同的.(你可以试试>:t [postmap', postmap]).鉴于此substitute :: Pack a => Identifier -> a -> Expression a -> Expression a,请考虑您的定义bind:您传递postmap一个期望值为type的参数T; 但是你给它一个类型的值Expression a -> Expression a.小心!这些类型不一样,因为在后一种情况下,它forall a在左边的某个地方; postmap期待它可以选择的功能a,但它已被赋予功能,a已经被其他人选择.假设您的示例是针对typecheck,然后您打电话bind给a ~ ().赋予的函数类型postmap 必须是Expression () -> Expression (),但这显然是无稽之谈.

如果我不是很清楚,请考虑"工作"版本:

type T = forall a . Expression a -> Expression a 

postmap :: T -> T 
postmap = undefined

-- These two substitutes have different types!
substitute :: Pack a => Identifier -> a -> Expression a -> Expression a
substitute = undefined

substitute' :: Pack a => Identifier -> a -> T
substitute' = undefined

-- Doesn't compile 
bind :: Pack a => Identifier -> a -> Expression a -> Expression a
bind ident value = postmap (substitute ident value)

-- Does compile!
bind' :: Pack a => Identifier -> a -> T
bind' ident value = postmap (substitute' ident value)

需要注意的重要事项是:无论您是如上定义还是type T = forall a . Pack a => ...,错误都是一样的.所以你的问题与你认为的不同.

调试这些问题的简单方法是使用

newtype T = T (forall a . Expression a -> Expression a)

错误通常更清楚(虽然不是在这种情况下).我很抱歉我无法提供真正的解决方案,因为我不确切知道这些功能究竟在做什么.但我怀疑#3是你的答案.