3 ms·
That is indeed the case. In Agda, the default is call-by-name, which means that functions are applied before arguments are evaluated. This does not, however, in
by andolanra 12y ago
That is indeed the case. In Agda, the default is call-by-name, which means that functions are applied before arguments are evaluated. This does not, however, include sharing, so evaluating
(λ x → x + x) (fib 2000)
will evaluate `fib 2000` twice. Agda programs can also be compiled to Haskell, in which case they would have Haskell's evaluation strategy, which is generally call-by-need (and so would share the result of fib 2000 above.)
- tel 12y agoI've never been aware of whether Agda is CBN or CBV because it actually doesn't matter (!). In a pure, terminating language like Agda evaluation is "confluent" which means that CBV and CBN evaluations are identical.