372148 (1) [Avatar] Offline
#1
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]
#2
Yes, they should all be x * 2, and this'll be fixed on the next revision. (This has already been reported here: https://forums.manning.com/posts/list/36789.page)
Norbert Melzer (1) [Avatar] Offline
#3
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
    #4
    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.