list - 为什么 GHC 不能对一些无限列表进行推理？

Question

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

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

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

@user2297560 在评论中写道:

Pretend you're GHCI. Your user gives you an infinite list and asks you to find all the values in that list that are less than or equal to 4. How would you go about doing it? (Keep in mind that you don't know that the list is in order.)

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

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

For the types Int and Integer, the enumeration functions have the following meaning:

• The sequence enumFrom e1 is the list [e1,e1 + 1,e1 + 2,…].

在他对另一个问题的回答中，@chepner 写道:

You know that the list is monotonically increasing, but Haskell does not.

这些用户所做的陈述对我来说似乎不符合标准。 Haskell 使用单调递增以有序的方式创建列表。 Haskell 应该知道该列表是有序且单调的。那么为什么不能把这个无限列表推到 [x | x <- list1, x <= 4]进入 takeWhile (<= 4) list1自动地？

Answer 1

从理论上讲，人们可以想象一种重写规则，例如

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

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

归根结底，为了执行更高级的分析，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

这最终可能更容易优化。