为什么GHC不能推理一些无限列表？
最近的这个问题让我想到了Haskell使用无限列表的能力。 关于StackOverflow的无限列表还有很多其他问题和答案，我明白为什么我们不能为所有无限列表提供一个通用解决方案，但为什么Haskell无法推导出一些无限列表？
我们使用第一个链接问题的例子：
list1 = [1..]
list2 = [x | x <- list1, x <= 4]
print list2
$ [1,2,3,4
@ user2297560在评论中写道：
假装你是GHCI。 你的用户给你一个无限的列表，并要求你找到列表中小于或等于4的所有值。你会怎么做呢？ （请记住，你不知道该列表是按顺序的。）
在这种情况下，用户并没有给你一个无限的列表。 GHC生成它！ 事实上，它是按照自己的规则生成的。 Haskell 2010标准声明如下：
enumFrom :: a -> [a] -- [n..]
对于Int和Integer类型，枚举函数具有以下含义：
e1是列表[ e1 ， e1 + 1， e1 + 2，...]。 @chepner在回答另一个问题时写道：
你知道列表单调递增，但Haskell没有。
这些用户所做的陈述似乎并不符合我的标准。 Haskell使用单调增加以有序方式创建列表。 Haskell 应该知道该列表是有序的和单调的。 那么，为什么不能将这个无限列表转化为[x | x <- list1, x <= 4] [x | x <- list1, x <= 4]转换为takeWhile (<= 4) list1 ？
理论上，可以想象一个重写规则，如
{-# RULES
"filterEnumFrom" forall (n :: Int) (m :: Int).
filter (< n) (enumFrom m) = [m..(n-1)]
#-}
这会自动将诸如filter (< 4) (enumFrom 1)表达式转换为[1..3] 。 所以这是可能的。 虽然有一个明显的问题：从这个确切的语法模式的任何变化都不起作用。 其结果是，你最终定义了一系列规则，你可以更长时间地确定它们是否触发。 如果你不能依靠规则，你最终只是不使用它们。 （另外，请注意，我已经将规则专门化为Int - 正如简单发布的注释，这可能会以其他类型细微的方式分解。）
在一天结束时，为了执行更高级的分析，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
这可能最终更容易优化。
那么，为什么不能将这个无限列表转化为[x | x <- list1, x <= 4] [x | x <- list1, x <= 4]转换为takeWhile (<= 4) list1 ？
答案并不比“它不使用takeWhile因为它不使用takeWhile ”更具体。 规范说：
翻译 ：列表理解满足这些身份，这些身份可以用作向内核的翻译：
[ 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 concatMap和concatMap调用翻译成更简单的语言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..]
上一篇: Why can't GHC reason about some infinite lists?
下一篇: Profile only a single function (or cost center) with GHC