如何在 Idris Interactive 中评估这个递归函数？答案

【问题标题】：How do I evaluate this recursive function in Idris interactive?如何在 Idris Interactive 中评估这个递归函数？
【发布时间】：2017-05-19 20:58:30
【问题描述】：

涉足 Idris，我试图将 this Haskell function 移植到 Idris。我想我成功了，用这段代码......

windowl : Nat -> List a -> List (List a)
windowl size = loop
  where
    loop xs = case List.splitAt size xs of
      (ys, []) => if length ys == size then [ys] else []
      (ys, _) => ys :: loop (drop 1 xs)

但是，当我在交互式 idris 中调用它时，似乎只评估了对函数的第一次调用，递归的下一步不是。这就是我在控制台上得到的。

*hello> windowl 2 [1,2,3,4,5]
[1, 2] :: Main.windowl, loop Integer 2 [2, 3, 4, 5] : List (List Integer)

有人可以告诉我正在发生的事情以及如何完全评估函数吗？

【问题讨论】：

标签： haskell recursion idris

【解决方案1】：

如manual中所述：

在编译时它 [Idris] 只会评估它知道是全部的东西 ... [跳过] ... 为方便起见，REPL 使用了编译时的求值概念。

total checker 无法发现windowl 函数实际上是total，因此我们可以使用assert_smaller construction 作弊：

total
windowl : Nat -> List a -> List (List a)
windowl size = loop
  where
    loop : List a -> List (List a)
    loop xs = case List.splitAt size xs of
      (ys, []) => if length ys == size then [ys] else []
      (ys, _) => ys :: loop (assert_smaller xs $ drop 1 xs)

或更改loop 以使整体检查器可以清楚地看到整体：

total
windowl : Nat -> List a -> List (List a)
windowl size = loop
  where
    loop : List a -> List (List a)
    loop [] = []
    loop xs@(x :: xs') = case List.splitAt size xs of
      (ys, []) => if length ys == size then [ys] else []
      (ys, _) => ys :: loop xs'

是的，我在这里偷工减料，用模式匹配替换硬编码的drop 1 来说明这个想法。更一般的情况可能需要更多的工作。

此时，REPL 完全计算表达式：

λΠ> windowl 2 [1,2,3,4,5]
[[1, 2], [2, 3], [3, 4], [4, 5]] : List (List Integer)

【讨论】：

步步高，安东 :)