正如其他人所指出的那样,即使在Haskell中,您的简化方式也不清楚。例如,我可以定义以下内容:
newtype NInt = N Int
instance Num NInt where
N a + _ = N a
N b * _ = N b
...
现在 sum . reverse :: Num [a] -> a
不等于 sum :: Num [a] -> a
,因为我可以将它们专门化为 [NInt] -> NInt
,其中显然不满足 sum . reverse == sum
。
这是围绕优化“复杂”操作存在的一般性张力之一——要成功证明某些东西可以进行优化,您实际上需要相当多的信息。这就是为什么在语法级别上存在的编译器优化通常是单态的并与程序的结构相关——通常是这样一个简化的领域,以至于优化“不可能”出错。即使如此,由于领域永远不会完全如此简化和为编译器所知,这也经常是不安全的。
以流融合为例,这是一种非常流行的“高级”语法优化。在这种情况下,编译器提供了足够的信息来表明流融合可以发生,并且基本上是安全的,但即使在这个典型的例子中,我们也需要避开非终止的概念。
那么,需要什么才能将 \x -> sum [0..x]
替换为 \x -> x*(x + 1)/2
?编译器需要内置数字和代数的理论知识。这在 Haskell 或 ML 中不可能,但在依赖类型语言(如 Coq、Agda 或 Idris)中变得可能。在那里,您可以指定像这样的东西:
revCommute :: (_+_ :: a -> a -> a)
-> Commutative _+_
-> foldr _+_ z (reverse as) == foldr _+_ z as
然后,理论上讲,告诉编译器按照
revCommute
重新编写。这仍然很困难和棘手,但至少我们有足够的信息。需要明确的是,我在上面写了一些非常奇怪的内容,一个依赖类型。该类型不仅取决于内联引入类型和参数名称的能力,还取决于您语言中的整个语法结构“在类型层面上”的存在。
然而,我刚才所写的与您在Haskell中所做的事情之间存在很多差异。首先,为了形成一个基础,使得这样的承诺可以被认真对待,我们必须放弃一般递归(因此我们已经不必担心像流融合那样的非终止问题)。我们还必须有足够的结构来创建像承诺Commutative _+_
这样的东西——这可能取决于在语言的标准库中建立运算符和数学的整个理论,否则您将需要自己创建。最后,即使要表达这些理论的丰富类型系统也会给整个系统增加很多复杂性,并且抛弃了您今天所知道的类型推断。
但是,鉴于所有这些结构,我将永远无法为在NInt
上定义的_+_
创建一个承诺Commutative _+_
,因此我们可以确定foldr (+) 0 . reverse == foldr (+) 0
实际上确实成立。
但现在我们需要告诉编译器如何执行该优化。对于流融合来说,编译器规则只有在我们编写了某些完全正确的句法形式时才会启动,以便“清晰地”成为优化redex。同样的限制也适用于我们的sum . reverse
规则。实际上,我们已经失败了,因为
foldr (+) 0 . reverse
foldr (+) 0 (reverse as)
不匹配。由于我们可以证明一些关于
(.)
的规则,它们“显然”是相同的,但这意味着现在编译器必须调用两个内置规则来执行我们的优化。
最终,为了实现你所说的自动优化,你需要一个非常智能的优化搜索,以便在已知法律集合上进行搜索。
因此,我们不仅增加了整个系统的复杂性,需要大量基础工作来构建一些有用的代数理论,并失去了图灵完备性(这可能不是最糟糕的事情),而且只有一个棘手的承诺,除非我们在编译期间执行指数级痛苦的搜索,否则我们的规则甚至无法触发。
噫。
今天存在的妥协往往是,
有时候我们对正在编写的内容具有足够的控制,以
大多数情况下确信可以执行某个
显然的优化。这就是流融合的体制,它需要许多隐藏类型、精心编写的证明、利用参数性和挥手之前的手势,才能成为社区信任并运行其代码的东西。
而且它甚至不总是触发。为了解决这个问题,看看
Vector
的源代码,其中包含所有指定
Vector
流融合优化应启动的常见情况的规则pragma。
所有这些都不是对编译器优化或依赖类型理论的批评。两者都非常令人难以置信。相反,这只是增强引入这种优化所涉及的权衡的放大。这不是轻率地做出的决定。