Is it possible to make pattern matching lazy in Idris?

2
votes

In Haskell we can do the following without getting a runtime error (ref):

mytake  0     _           =  []
mytake  _     []          =  []
mytake  n     (x:xs)      =  x : mytake (n-1) xs

print( mytake 0 (undefined::[Int]) )

In Idris, we can do a similar definition, but the behavior is different:

mytake : Integer -> List a -> List a
mytake  0     _           =  []
mytake  _     []          =  []
mytake  n     (x::xs)      =  x :: mytake (n-1) xs

printLn( mytake {a = Nat} 0 ?undefined )

In this case we get ABORT: Attempt to evaluate hole Main.undefined. I know Idris is not a lazy language, but my impression was that pattern matching parameters might be separate from the logic for evaluation of data structures (which can be sidestepped in Idris, e.g. with Stream).

In addition to understanding if there is a way around this, I'd also appreciate knowing why Idris behaves in this way.

1
idris

1 Answers

1
votes

Well, if I understand right , this could work

module Main

mytake : Integer -> Lazy (List a) -> List a
mytake  0     _          = []
mytake  _     []         = []
mytake  n     (x::xs)    = x :: mytake (n-1) xs


main : IO ()
main = printLn (mytake {a = Nat} 0 ?undefined)

But it gives me strange error while compiling

andrey@linux:~/idris> idris -o test test.idr
idris: src/Idris/Core/CaseTree.hs:(645,1)-(654,51): Non-exhaustive patterns in function varRule

Answering to the second part of your question: This is mostly because of eager evaluation is more predictable. This quesion is in an unofficial FAQ

https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ#why-isnt-idris-lazy