为什么 GHC 不能推理一些无限列表？答案

【问题标题】：Why can't GHC reason about some infinite lists?为什么 GHC 不能推理一些无限列表？
【发布时间】：2017-07-14 06:05:09
【问题描述】：

This recent question 让我想到了 Haskell 处理无限列表的能力。 StackOverflow上有plenty of other关于无限列表的问题和答案，我明白为什么我们不能对所有无限列表都有一个通用的解决方案，但是为什么Haskell不能解释some 无限列表？

让我们使用第一个链接问题中的示例：

list1 = [1..]
list2 = [x | x <- list1, x <= 4]
print list2
$ [1,2,3,4

@user2297560 在 cmets 中写道：

假装你是 GHCI。您的用户给了您一个无限列表，并要求您找到该列表中小于或等于 4 的所有值。您将如何去做？（请记住，您不知道列表是有序的。）

在这种情况下，用户并没有给你一个无限列表。 GHC 生成它！事实上，它是按照自己的规则生成的。 Haskell 2010 Standard 声明如下：

enumFrom       :: a -> [a]            -- [n..]

对于 Int 和 Integer 类型，枚举函数的含义如下：

序列 enumFrom e1 是列表 [e1,e1 + 1,e1 + 2,…]。

@chepner 在回答另一个问题时写道：

你知道列表是单调递增的，但 Haskell 不知道。

在我看来，这些用户的陈述似乎不符合标准。 Haskell 使用单调递增以有序方式创建列表。 Haskell应该知道列表是有序且单调的。那么为什么不能将这个无限列表自动将[x | x <- list1, x <= 4] 变成takeWhile (<= 4) list1 呢？

【问题讨论】：

好。只是想把这个链接在这里。 stackoverflow.com/questions/40145318
Haskell 不会推断任何东西，除非该语言的开发人员对其进行推断。天下没有免费的午餐。显然，您可以设计语言，以便自动将某些列表标记为正在增加，但这会增加已经非常复杂的语言的复杂性。
@JohnColeman 这很公平，这对我来说似乎是管理无限列表的一个合乎逻辑的跳跃。我认为 Haskell 的设计人员/开发人员在语言设计/抽象数学方面更加精通，并且有一个很好的理论理由来解释为什么没有这样做，而不是一个务实的理由。
列表推导对所有类型的列表都适用，并且不考虑任何进一步的结构（即[1..] 的类型为Enum t, Num t => [t] 而不仅仅是[t]）。其次，谓词x <= 4 对过滤机制是不透明的，它只是一个函数t -> Bool，因此随着列表元素的增加，没有关于其行为的信息。
正如其他人所提到的，一旦创建了一个列表，关于它的如何创建的信息就会丢失。你需要以某种方式保存它；典型的方法是创建自己的类型来保留订购信息。使您的类型符合 List 类型类，您可以在任何适合普通 Ord a => List a 的地方使用它。

标签： list haskell ghc compiler-optimization

【解决方案1】：

那么为什么不能将这个无限列表自动转换为[x | x <- list1, x <= 4] 为takeWhile (<= 4) list1 呢？

答案并不比“它不使用takeWhile，因为它不使用takeWhile”更具体。 The spec says:

翻译：列表推导式满足这些身份，这可能用作内核的翻译：

[ e | True ]         = [ e ]
[ e | q ]            = [ e | q, True ]
[ e | b, Q ]         = if b then [ e | Q ] else []
[ e | p <- l, Q ]    = let ok p = [ e | Q ]
                           ok _ = []
                       in concatMap ok l
[ e | let decls, Q ] = let decls in [ e | Q ]

也就是说，列表推导的含义是通过使用if-expressions、let-bindings 和调用concatMap 翻译成更简单的语言来给出的。我们可以通过以下步骤翻译您的示例来弄清楚它的含义：

[x | x <- [1..], x <= 4]

-- apply rule 4 --
let ok x = [ x | x <= 4 ]
    ok _ = []
in concatMap ok [1..]

-- eliminate unreachable clause in ok --
let ok x = [ x | x <= 4 ]
in concatMap ok [1..]

-- apply rule 2 --
let ok x = [ x | x <= 4, True ]
in concatMap ok [1..]

-- apply rule 3 --
let ok x = if x <= 4 then [ x | True ] else []
in concatMap ok [1..]

-- apply rule 1 --
let ok x = if x <= 4 then [ x ] else []
in concatMap ok [1..]

-- inline ok --
concatMap (\x -> if x <= 4 then [ x ] else []) [1..]

【讨论】：

【解决方案2】：

理论上，可以想象一个重写规则，例如

{-# RULES
  "filterEnumFrom" forall (n :: Int) (m :: Int).
                     filter (< n) (enumFrom m) = [m..(n-1)]
  #-}

这会自动将filter (< 4) (enumFrom 1) 等表达式转换为[1..3]。所以它是可能的。但是有一个明显的问题：这种 exact 语法模式的任何变化都不起作用。结果是您最终定义了一堆规则，并且您可以再确定它们是否正在触发。如果你不能依赖规则，你最终只是不使用它们。（另外，请注意我已将规则专门用于 Ints - 正如作为评论简要发布的那样，对于其他类型，这可能会以微妙的方式分解。）

归根结底，为了执行更高级的分析，GHC 必须将一些跟踪信息附加到列表中，以说明它们是如何生成的。这要么使列表的抽象变得不那么轻量，要么意味着 GHC 将有一些特殊的机制在其中只是用于在编译时优化列表。这些选项都不好。

也就是说，您始终可以通过在列表的顶部上创建列表类型来添加自己的跟踪信息。

data List a where
  EnumFromTo :: Enum a => a -> Maybe a -> List a
  Filter :: (a -> Bool) -> List a -> List a 
  Unstructured :: [a] -> List a

这可能最终会更容易优化。

【讨论】：