haskell - 弱化对 2 级类型的约束

Question

{-# LANGUAGE RankNTypes #-}

从 previous series of questions 继续, 我有一个通用的函数
量化函数作为参数，如下所示:

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 的签名|本身，但我看不到任何其他方法来解决这个问题。

我不确定如何解决这个问题，但我可以看到一些可用的选项。

在 bind 的签名周围添加约束这样才能快乐
类型检查。

创建另一个函数 emap'与约束，并实现 emap'按照emap反之亦然( emap 是一个无聊的机械定义，它不会使
感觉有两个相同的函数体，只是签名不同)。

将我正在尝试做的事情识别为代码异味并继续进行替代
解决方案。 (???)

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期望类型为 T 的值;但是你给了它一个 Expression a -> Expression a 类型的值.当心!这些类型并不相同，因为在后一种情况下，forall a在左边的某个地方； postmap期待一个可以选择 a 的函数，但它被赋予了一个函数是 a已经被别人选中了。假设您的示例是类型检查，然后您调用 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 是你的答案。