多态递归如何与无限类型错误相关？

html5 • • 问答

上下文：我遇到了一个问题并在这里得到了帮助，但是我意识到我不理解解决方案。

关键字似乎是polymorphic recursion。我认为这foldr是多态和递归的，但这似乎是一个不同的概念。

这个显式递归有效（基于shell-monad）：

cmdList :: (Param command, Param arg, CmdParams result) =>
    command -> [arg] -> result
cmdList command = go . reverse where
    go :: (Param arg, CmdParams result) => [arg] -> result
    go [] = cmd command
    go (arg:args) = go args arg

但是试图重构我最初尝试使用的答案时，foldr很快就遇到了我最初遇到的问题：无限类型。更换常数cmd command用b：

go :: (Param arg, CmdParams result) => result -> [arg] -> result
go b [] = b
go b (arg:args) = go b args arg

go :: (Param arg, CmdParams result) => result -> [arg] -> result
go b [] = b
go b (arg:args) = go b args arg

    • Occurs check: cannot construct the infinite type:
        result ~ arg -> result
    • In the expression: go b args arg

在我看来，GHC 不再接受result值或函数的多态。

  1. 为什么会这样？

  2. foldr在这种情况下我可以不使用吗？

回答

这是一个简单的递归函数：

ignore :: [a] -> ()
ignore [] = ()
ignore (a:as) = ignore as

它是多态的，并且是递归的。但是，就像几乎所有的递归一样，无论调用者为 选择什么类型a，递归都会使用与 相同的选择a。也就是说，我们可以使用 ScopedTypeVariables 和一些其他扩展来编写它：

ignore :: forall a. [a] -> ()
ignore (a:as) = ignore @a as

术语“多态递归”指的是一种非常特殊的递归，其中递归调用为某些参数选择不同的类型。标准示例是这样的：

data BalancedTree a = Leaf a | Branch (BalancedTree (a, a))

foldBT :: (a -> a -> a) -> BalancedTree a -> a
foldBT f (Leaf a) = a
foldBT f (Branch bt) = uncurry f $ foldBT ((x, y) (x', y') -> (f x x', f y y')) bt

（例如，foldBT (+)将添加树的所有元素。）

这里的特别之处在于对递归调用foldBT是不是递归在BalancedTree a-可是过了BalancedTree (a, a)吧。类型已更改，如下所示：

foldBT :: forall a. (a -> a -> a) -> BalancedTree a -> a
foldBT f (Branch bt) = uncurry f $ foldBT @(a, a) {- N.B. not a! -} ((x, y) (x', y') -> (f x x', f y y')) bt

事实证明，在允许这种事情的设置中进行类型推断非常困难。为了解决这个问题，Haskell 有一个限制：推断类型总是使用单态递归，也就是说，所有递归调用都为所涉及的类型变量选择所有相同的值。您仍然可以通过提供适当的类型签名来获得多态递归，因为不需要推断。

现在，在你的工作情况下，你写

cmdList :: forall command arg result.
    (Param command, Param arg, CmdParams result) =>
    command -> [arg] -> result
cmdList command = go . reverse where
    -- for clarity, I have chosen fresh type variable names
    go :: forall arg' result'. (Param arg', CmdParams result') => [arg'] -> result'
    go [] = cmd command
    go (arg:args) = go args arg

请注意，在递归情况下，go与左侧相比，在等式右侧给出了一个额外的参数！这是多态递归；该result类型正在慢慢积累额外的参数。

go (arg:args) = go @arg' @(arg' -> result') {- N.B. not result'! -} args arg

这意味着在基本情况下，

go [] = cmd command

的类型cmd可能会有所不同，具体取决于列表中有多少个参数！换句话说，您可以认为事件按以下顺序发生：首先，用户选择命令类型、参数类型和结果类型；然后遍历列表并选择接受更多参数的不同结果类型；然后您cmd使用新选择的结果类型调用。

比较不起作用的版本：

在这个版本中，失去了一个选择；首先用户选择一个结果类型，然后遍历列表并选择与用户相同的结果类型；然后你使用他们b的那种类型。但这是一个问题——他们可能没有为该列表选择正确数量的参数，即使他们选择了，期望编译器能够静态地知道这些也是不合理的！

这解释了您遇到的发生检查错误：为了go在此设置中正常工作，其b参数必须能够接受任意数量的参数，并且没有任何单一类型可以做到这一点。

它还解释了为什么不能使用foldr:foldr是用单态递归实现的。可能有可能创建一个foldr使用 RankNTypes的变体，它可以放在这个位置，但我怀疑它的工作量超过了它的价值。

而且，顺便说一句，我认为您可以使重构工作，尽管我不是 100%，因为我还没有安装 shell-monad 来检查这一点。但它看起来像这样：

go :: (Param arg, CmdParams result) => (forall result'. CmdParams result') -> [arg] -> result
-- same implementation as before

这里的关键是把额外的放在forall那里会强制第一个b参数是多态的；这使您可以选择在到达基本情况时result'成为一个合适的多参数变体result。

以上是多态递归如何与无限类型错误相关？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>