The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

372148 (1) [Avatar] Offline
When you explain how expressions are substituted there are, I think, multiple mistakes. I've commented those on each line. (I had to format it as code to make it clear what I corrected ...)


This means whenever the Idris evaluator encounters 
an expression of the form double x, with some expression 
standing for x, it should be rewritten to x * 2. So, in the 
example double (double 15):

Expression is now double (15 * 15)                                  // 2 * 15
Expression is now double 30
Expression is now 30 * 30                                           // 2 * 30
First, the inner double 15 is rewritten to 15 * 15                  // 2 * 15
15 * 15 is rewritten to 30                                          // 2 * 15
double 30 is rewritten to 30 * 30                                   // 2 * 30
30 * 30 is rewritten to 60                                          // 2 * 30

You might have noticed that instead of choosing to
evaluate the inner double 15 first, we could have 
chosen the outer double (double 15), which would 
have reduced to double 15 * double 15. Either order                 // (double 15) * 2 
is possible, and each would lead to the same result. 
Idris, by default, will evaluate the innermost expression 
first. In other words, it will evaluate function arguments 
before function definitions.
Anonymous (122) [Avatar]
Yes, they should all be x * 2, and this'll be fixed on the next revision. (This has already been reported here:
Norbert Melzer (1) [Avatar] Offline
It is not completely solved. There are still definitions and explanations left which assume double x = x * x instead of double x = 2 * x:

  • Page 35, In the NOTE block about evaluation order the example is expanded to (double 15) * (double 15) instead of the more correct 2 * (double 15)

  • Page 39, when giving the compilable and incompilable examples of double, both are given as x * x

  • Page numbers correspond to the numbers on the upper outside corner of the pdf-version from May 31st, 2016
    bobgus (17) [Avatar] Offline
    Why not use:
    double x = x + x

    Using addition instead of multiplication seems a bit faster. (My machine code roots are showing..)

    Perhaps this is what you had in mind when the example was originally written.