我开始学习函数式编程语言，例如 Haskell、ML，大部分练习都会展示以下内容：
foldr (+) 0 [ 1 ..10]
相当于
sum = 0
for( i in [1..10] )
sum += i
这让我想到，为什么编译器不能知道这是等差数列，并使用O(1)公式进行计算呢？
特别是对于没有副作用的纯FP语言而言？
同样适用于
sum reverse list == sum list
假设a + b = b + a成立且定义了“反转”，编译器/语言能否自动证明它？
{-# RULES
"sum/reverse" forall list . sum (reverse list) = sum list
#-}
reverse list周围的括号 - 你在问题中写的实际上是(sum reverse) list，这会导致类型检查失败。正如其他人所指出的，即使是简单的算术优化在浮点数上也是非常危险的，编译器通常有标志来关闭它们 - 例如Visual C++，gcc。即使是整数运算也不总是明确的，人们偶尔会就如何处理溢出等问题发生大争论。
正如Joachim所指出的，循环中的整数变量是应用稍微复杂的优化的一个地方，因为实际上可以获得显着的收益。Muchnick的书可能是这个主题的最佳通用来源，但它不便宜。维基百科关于强度降低的页面可能是任何一种标准优化的介绍，同时还提供了相关文献的参考。
FFTW是一个例子，它内部执行各种数学优化。其中一些代码是作者专门为此编写的定制编译器生成的。这是值得的，因为作者具有特定领域的优化知识，而且在库的特定上下文中既值得努力又安全。
人们有时使用模板元编程编写“自我优化的库”，这些库可能依赖于算术恒等式，例如Blitz++。Todd Veldhuizen的博士论文有一个很好的概述。
如果你深入到玩具和学术编译器的领域，那么各种各样的事情都会发生。例如我自己的博士论文是关于编写低效函数程序以及解释如何优化它们的小脚本。其中许多例子（参见第6章）依赖于应用算术规则来证明底层优化。
不，编译器不会做那种事情。
对于你的例子来说，这样做甚至是错误的：由于没有给出类型注释，Haskell编译器将推断出最通用的类型，这将是
foldr (+) 0 [ 1 ..10] :: Num a => a
和相似的
(\list -> sum (reverse list)) :: Num a => [a] -> a
而且正在使用的类型的 Num 实例可能无法满足您建议的转换所需的数学规律。编译器首先应避免改变程序的含义（即语义）。
更加实际的是：编译器很少能检测到这种大规模的转换，因此实现它们不值得。
请注意，线性转换在循环中是非常明显的例外。大多数编译器会重新编写
for (int i = 0; i < n; i++) {
... 200 + 4 * i ...
}
到
for (int i = 0, j = 200; i < n; i++, j += 4) {
... j ...
}
或类似的东西，因为这种模式在处理数组的代码中经常出现。
sum list == sum (reverse list)
You still can't replace the expression above with True unless you can rule out the possibility that list or some list element is bottom. Usually, one cannot do this. You can't even do the following "trivial" optimization of f x == f x in all cases
f x `seq` True
考虑到，
f x = (undefined :: Bool, x)
f x `seq` True ==> True
f x == f x ==> undefined
f n = n * foldl (+) 0 [1..10] :: Int
可以想象，通过将表达式移出其上下文并用常量名称替换它，可以优化程序，就像这样：
const1 = foldl (+) 0 [1..10] :: Int
f n = n * const1
foldl、+ 和 enumFromThenTo 的知识。例如，它必须知道计算 foldl (+) 0 [1..10] 是可以的，但计算 foldl (+) 0 [1..maxBound] 则不行。 - Ingonewtype NInt = N Int
instance Num NInt where
N a + _ = N a
N b * _ = N b
... -- etc
现在 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。Int（而不是多态的Num a => a），编译器可以推断出表达式foldr (+) 0 [1 ..10]没有外部依赖，因此它可以在编译时进行评估并被55替换。然而，据我所知，目前没有主流编译器执行这种优化。