为什么GHC不能推理一些无限的名单？

Question

这个最近的问题让我想到了Haskell使用无限列表的能力.有大量 的 其他问题,并约在计算器上无限列表答案,我明白了为什么我们不能对所有无限列表的通用解决方案,但为什么不能哈斯克尔推理一些无限列表？

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

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

@ user2297560在评论中写道:

假装你是GHCI.您的用户会为您提供无限列表,并要求您查找该列表中小于或等于4的所有值.您将如何进行此操作？(请记住,您不知道列表是否有序.)

在这种情况下,用户没有给你一个无限的列表.GHC产生了它!实际上,它是按照自己的规则生成的.该哈斯克尔2010标准规定如下:

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呢？

Answer 1

从理论上讲,人们可以想象一个重写规则,如

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

而自动将表达式转换如filter (< 4) (enumFrom 1)要[1..3].所以有可能.但是有一个明显的问题:这种确切的句法模式的任何变化都不会起作用.结果是你最终定义了一堆规则,你可以更长时间地确定它们是否在触发.如果你不能依赖规则,你最终只是不使用它们.(另外,请注意我已经将规则专门用于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

这可能最终更容易优化.

Answer 2

那么为什么不能将这个无限列表自动[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-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..]