CODEWITHSUNDEEP
haskellrecursionidris
flq
flq

Reputation: 22849

How do I evaluate this recursive function in Idris interactive?

Dabbling into Idris, I was trying to port this Haskell function to Idris. I think I succeeded, with this code...

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)

However, when I call it in interactive idris, it appears that only the first call into the function is evaluated, the next step in the recursion is not. This is what I get on the console.

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

Can someone enlighten me as to what is happening and how I can get the function evaluated completely?

Upvotes: 4

Views: 319

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

As explained in the manual:

At compile-time it [Idris] will only evaluate things which it knows to be total ... [skipped]... The REPL, for convenience, uses the compile-time notion of evaluation.

The totality checker is not able to discover that the windowl function is in fact total, so we can either cheat using the 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)

or change loop to make totality obvious to the totality checker:

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'

Yes, I'm cutting corners here, replacing the hardcoded drop 1 with pattern-matching to illustrate the idea. The more general case might require more work.

At this point, REPL fully evaluates the expression:

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

Upvotes: 4

Related Questions