Czy Idris naprawdę jest "ściśle oceniany?"

Question

Pochodzę z Haskell, czytałem o historii Idris na temat lenistwa (nie-surowość). I trolled niedawne informacje o wersji i found code podobny do poniższego

myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a 
myIf True t e = t 
myIf False t e = e 

napisałem prostą funkcję silni, aby go przetestować

myFact : Int -> Int 
myFact n = myIf (n == 1) 1 (n * myFact (n-1)) 

Pobiegłem i to działa!

> myFact 5 
120 : Int 

postanowiłem podzielić go przez zmianę typu podpis z myIf do

myIf : (b : Bool) -> a -> a -> a 

I Reaktywacja idris repl i pobiegł myFact 5 ponownie oczekując nieskończonej rekurencji. Ku mojemu zaskoczeniu, wciąż działało tak samo!

Czy idiota może wymyślić, kiedy należy unikać ścisłości? Dlaczego to się nie powtórzyło na zawsze?

Używam Idris 0.9.15 i żadnych uwag do wydania od teraz do połączonych notatek, wspomnij o wszelkich zmianach.

Answer 1

Wyjaśnienie jest tutaj: http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on

czasie kompilacji i uruchamiania semantyka oceny czasowe są różne (niekoniecznie tak, ponieważ w czasie kompilacji sprawdzania typu musi ocenić wyrażenia w obecności nieznanych wartościach) i REPL jest używając pojęcia czasu kompilacji, zarówno dla wygody, jak i dlatego, że warto zobaczyć, jak wyrażenia zmniejszają się w sprawdzaniu typu.

Jednak dzieje się tu trochę więcej. Idris zauważył, że myIf jest bardzo małą funkcją i postanowił ją wbudować. Więc gdy kompilowany myFact faktycznie ma definicję, która wygląda trochę jak:

myFact x = case x == 1 of 
       True => 1 
       False => x * myFact (x - 1) 

więc ogólnie można napisać struktur kontrolnych, takich jak myIf bez martwienia się o tworzenie rzeczy Lazy, ponieważ Idris będzie kompilować je do struktury kontrolnej chciałeś tak. To samo dotyczy np. && i || i zwarcie.