时间戳

首页 > 解决方案 > 多态递归与无限类型错误有何关系？

haskell - 多态递归与无限类型错误有何关系？

问题描述

背景：我遇到了一个问题并在这里得到了帮助，但是我意识到我不明白解决方案。

关键字似乎是多态递归。我认为这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

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

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

  1. 为什么会这样？

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

标签： haskell

解决方案

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

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不是在 a上BalancedTree a递归——而是在 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用新选择的结果类型调用。

比较不起作用的版本：

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

在这个版本中，一个选择已经丢失；首先用户选择一个结果类型，然后遍历列表并选择与用户相同的结果类型；然后你使用他们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

推荐阅读