5 ms·

Shouldn't the then- and else-"branches" be made lazy?

• eru 12y ago
  They probably are already. (In Haskell, they would be by default. I don't know enough about Agda.)
  • 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 ago
      I'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.
      • Peaker 12y ago
        Identical up to one algorithm taking a few seconds, and another taking as long as the universe has been alive :)
        • tel 12y ago
          Who runs Agda code anyway? :)
      • eru 12y ago
        Not only CBV and CBN, but also strict evaluation.
  • Dewie 12y ago
    Huh, for some reason I assumed that we were talking about Idris. I didn't read the post well enough.