如何評估Idris交互中的遞歸函數？

Question

涉足伊德里斯，我試圖將this Haskell function移植到伊德里斯。我覺得我成功了，有了這個代碼...

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) 

然而，當我把它叫做互動伊德里斯，似乎只有在第一次調用到函數進行評估，在遞歸下一步是不是。這是我在控制檯上得到的。

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

有人能告訴我發生了什麼，我怎麼能完全評估功能？

Answer 1

正如manual解釋說：

在它知道是總 編譯一次[伊德里斯]只會評估的事情...... [跳過] ... 的REPL，爲了方便，使用編譯時評估的概念。

的總和檢查是無法發現，windowl功能其實總的，所以我們可以使用assert_smallerconstruction騙：

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)