0

我正在学习 Idris 语言并决定实施惰性算法来查找所有 Hamming 数，即“n = 2^i 3^j 5^k”形式的数字（仅由 2s、3s 和 5s 组成）。据我了解，我需要大量使用Stream数据类型。我决定采用的方法是从通常的基本递归构造中省略重复项。为此，我将需要以下merge功能：

merge : Stream Integer -> Stream Integer -> Stream Integer
merge a@(x :: xs) b@(y :: ys) = if x < y
                                then x :: merge xs b
                                else y :: merge a ys

和Stream5 的幂（作为起点）：

fives : Inf (Stream Integer)
fives = iterate (5*) 1

汉明数的结果Stream具有以下结构：

hamming : Inf (Stream Integer)
hamming = 1 :: foldr func fives [2,3] where
  func : Integer -> Inf (Stream Integer) -> Inf (Stream Integer)
  func next generated = nextStream where
    nextStream : Inf (Stream Integer)
    nextStream = merge generated (map (next*) (1 :: nextStream))

代码可以加载到 REPL 环境中，但是当我尝试访问时，例如，第 10 个元素

Stream.take 10 hamming

我得到非常奇怪的结果，即它只计算第一个元素，这显然是 1 并写下表达式......

我真的使用“正确”的惰性结构吗？如何以打印出无限序列的第 10 个数字（例如）的方式解决此问题？

4

0 回答 0