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.
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