Возможно ли сделать сопоставление с образцом ленивым в Idris? - PullRequest
Новая
       11

Возможно ли сделать сопоставление с образцом ленивым в Idris?

0 голосов
/ 03 июня 2018

В Haskell мы можем сделать следующее, не получая ошибки времени выполнения ( ref ): 

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

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

В Idris мы можем сделать аналогичное определение, но поведение отличается:

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

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

В этом случае мы получаем ABORT: Attempt to evaluate hole Main.undefined.Я знаю, что Idris не ленивый язык, но у меня сложилось впечатление, что параметры сопоставления с образцом могут быть отделены от логики для оценки структур данных (которые можно обойти в Idris, например, с помощью Stream).

В дополнение к пониманию, есть ли способ обойти это, я также был бы признателен, если бы знал, почему Идрис ведет себя таким образом.

1 Ответ

0 голосов
/ 04 июня 2018

Ну, если я правильно понимаю, это может сработать 

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)

Но это дает мне странную ошибку при компиляции 

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

Ответ на вторую часть вашего вопроса: Этов основном из-за нетерпеливой оценки более предсказуемо.Этот вопрос находится в неофициальном FAQ

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

...