phoe · February 7, 2020 13:22 · Nov 2, 2019 · Nov 2, 2019 · Nov 2, 2019 · Nov 2, 2019
diff --git a/text.md b/text.md
@@ -46,6 +46,8 @@ This means that it is impossible for the value of `i` to be `(1+ most-positive-f
 [CLHS 1.5.2](http://www.lispworks.com/documentation/HyperSpec/Body/01_eb.htm) states:
 > Conforming code shall not depend on the consequences of undefined or unspecified situations. 
 
-This implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not, I argue that it is conforming, since the values that the variable is permitted to take inside the iteration are fully within the `fixnum` type. (This agrees with the likely user intent of this `LOOP` call - that the user wants to evaluate some code for every fixnum.)
+The implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not. I argue that it is conforming, since the values that the variable is permitted to take and meant to be taken inside the iteration are fully within the `fixnum` type; the implementation is not required to assign a non-`fixnum` value to the variable `i` in order to successfully perform the iteration. (This agrees with the likely user intent of this `LOOP` call - that the user wants to evaluate some code for every fixnum.)
 
-If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. **This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.**
+If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. 
+
+**This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned, which completes the proof.**
diff --git a/text.md b/text.md
@@ -46,6 +46,6 @@ This means that it is impossible for the value of `i` to be `(1+ most-positive-f
 [CLHS 1.5.2](http://www.lispworks.com/documentation/HyperSpec/Body/01_eb.htm) states:
 > Conforming code shall not depend on the consequences of undefined or unspecified situations. 
 
-This implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not; I argue that it is conforming, since the user wants to perform an iteration for every fixnum. (*@dkochmanski mentioned on `#lisp` that "kinda makes sense" and "is the least surprising behavior" - again - is a good argument for unifying behavior, but not for declaring code conforming. The behavior is undefined, but the least surprising thing to do is the following. hence all implementations should adopt it for the abovementioned reasons.*)
+This implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not, I argue that it is conforming, since the values that the variable is permitted to take inside the iteration are fully within the `fixnum` type. (This agrees with the likely user intent of this `LOOP` call - that the user wants to evaluate some code for every fixnum.)
 
-If this code ~~conforms~~ *is supposed to be unsurprising*, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. **This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.**
+If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. **This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.**
diff --git a/text.md b/text.md
@@ -27,7 +27,7 @@ This is true, since, according to the standard, `The type fixnum is required to
 (loop for i of-type fixnum from most-negative-fixnum to most-positive-fixnum finally (return i))
 ```
 
-This `LOOP` form is logically consistent, since the value of `i` is between `most-negative-fixnum` and `most-positive-fixnum`, and therefore falls within the range of `fixnum`. The intent is also clear - the user wants to iterate over all fixnums.
+This `LOOP` form is logically consistent, since the value of `i` is between `most-negative-fixnum` and `most-positive-fixnum`, and therefore falls within the range of `fixnum`. (The intent is also clear - the user wants to iterate over all fixnums.)
 
 In the `LOOP` epilogue, we have the form `(return i)`. Therefore the variable `i` is accessed which is of type `fixnum`. Its value therefore must be of type `fixnum`, due to the `OF-TYPE` declaration.
 
@@ -46,6 +46,6 @@ This means that it is impossible for the value of `i` to be `(1+ most-positive-f
 [CLHS 1.5.2](http://www.lispworks.com/documentation/HyperSpec/Body/01_eb.htm) states:
 > Conforming code shall not depend on the consequences of undefined or unspecified situations. 
 
-This implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not; I argue that it is conforming, since the user wants to perform an iteration for every fixnum. 
+This implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not; I argue that it is conforming, since the user wants to perform an iteration for every fixnum. (*@dkochmanski mentioned on `#lisp` that "kinda makes sense" and "is the least surprising behavior" - again - is a good argument for unifying behavior, but not for declaring code conforming. The behavior is undefined, but the least surprising thing to do is the following. hence all implementations should adopt it for the abovementioned reasons.*)
 
-If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. **This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.**
+If this code ~~conforms~~ *is supposed to be unsurprising*, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. **This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.**
diff --git a/text.md b/text.md
@@ -31,7 +31,7 @@ This `LOOP` form is logically consistent, since the value of `i` is between `mos
 
 In the `LOOP` epilogue, we have the form `(return i)`. Therefore the variable `i` is accessed which is of type `fixnum`. Its value therefore must be of type `fixnum`, due to the `OF-TYPE` declaration.
 
-This means that it is impossible for the value of `i` to be `(1+ most-positive-fixnum)`, since this value is not of type `fixnum`. It would also mean that this value was assigned to the variable `i` accessible in the loop prologue, which is a type violation.
+This means that it is impossible for the value of `i` to be `(1+ most-positive-fixnum)`, since this value is not of type `fixnum`. It would also mean that this value was assigned to the variable `i` accessible in the loop epilogue, which is a type violation.
 
 **A `TYPE` declaration is not allowed to change the semantics of the program** since [CLHS 3.3.1](http://clhs.lisp.se/Body/03_ca.htm) states:
 > In general, an implementation is free to ignore declaration specifiers except for the declaration, notinline, safety, and special declaration specifiers. 

diff --git a/text.md b/text.md
@@ -33,8 +33,10 @@ In the `LOOP` epilogue, we have the form `(return i)`. Therefore the variable `i
 
 This means that it is impossible for the value of `i` to be `(1+ most-positive-fixnum)`, since this value is not of type `fixnum`. It would also mean that this value was assigned to the variable `i` accessible in the loop prologue, which is a type violation.
 
-**Accessing `i` in the loop prologue is valid**, as the forms inside the `LOOP` form (in particular, the epilogue) are in scope of the bindings, so they have access to the variables. According to [CLHS 6.1.1.4](http://www.lispworks.com/documentation/HyperSpec/Body/06_aad.htm):
+**A `TYPE` declaration is not allowed to change the semantics of the program** since [CLHS 3.3.1](http://clhs.lisp.se/Body/03_ca.htm) states:
+> In general, an implementation is free to ignore declaration specifiers except for the declaration, notinline, safety, and special declaration specifiers. 
 
+**Accessing `i` in the loop prologue is valid**, as the forms inside the `LOOP` form (in particular, the epilogue) are in scope of the bindings, so they have access to the variables. According to [CLHS 6.1.1.4](http://www.lispworks.com/documentation/HyperSpec/Body/06_aad.htm):
 > A loop macro form expands into a form containing one or more binding forms (that establish bindings of loop variables) and a block and a tagbody (that express a looping control structure). The variables established in loop are bound as if by let or lambda.
 
 [CLHS Declaration TYPE](http://clhs.lisp.se/Body/d_type.htm) states:

diff --git a/text.md b/text.md
@@ -44,6 +44,6 @@ This means that it is impossible for the value of `i` to be `(1+ most-positive-f
 [CLHS 1.5.2](http://www.lispworks.com/documentation/HyperSpec/Body/01_eb.htm) states:
 > Conforming code shall not depend on the consequences of undefined or unspecified situations. 
 
-This implies that that `**LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not; I argue that it is conforming, since the user wants to perform an iteration for every fixnum. 
+This implies that that **`LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not; I argue that it is conforming, since the user wants to perform an iteration for every fixnum. 
 
-If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.
+If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. **This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.**
diff --git a/text.md b/text.md
@@ -0,0 +1,49 @@
+So recently a ~~religious debate~~ intense discussion happened on `#lisp` about whether the following form:
+
+```lisp
+;; Form 1
+(loop for i from 1 to 5 finally (return i))
+```
+
+should return `5` or `6` (or, in other words, `(1+ 5)` - this notation is important as it will be used later).
+
+I argue that it is invalid for it to return `6` and `5` must be returned instead.
+
+**Let us assume that `(declaim (optimize (safety 3)))` is in effect. In other words, we are working on safe code.**
+
+**An `of-type` declaration is allowed in for-as-arithmetic variable bindings in `LOOP`** and it is meant to be used for optimization. Adding a type declaration should not have any change on the meaning of the program, other than the fact that it must signal a type error in safe code. Therefore, form 1 is equivalent to
+
+```lisp
+;; Form 2
+(loop for i of-type fixnum from 1 to 5 finally (return i))
+```
+
+This is true, since, according to the standard, `The type fixnum is required to be a supertype of (signed-byte 16).` Numbers from 1 to 5, and even 6, are therefore all fixnums.
+
+**The intent of the above form is that the user wants to do something five times - for integers from 1 to 5.** Let us modify this loop - for instance, the user might want to do something for all fixnums. This gives us:
+
+```lisp
+;; Form 3
+(loop for i of-type fixnum from most-negative-fixnum to most-positive-fixnum finally (return i))
+```
+
+This `LOOP` form is logically consistent, since the value of `i` is between `most-negative-fixnum` and `most-positive-fixnum`, and therefore falls within the range of `fixnum`. The intent is also clear - the user wants to iterate over all fixnums.
+
+In the `LOOP` epilogue, we have the form `(return i)`. Therefore the variable `i` is accessed which is of type `fixnum`. Its value therefore must be of type `fixnum`, due to the `OF-TYPE` declaration.
+
+This means that it is impossible for the value of `i` to be `(1+ most-positive-fixnum)`, since this value is not of type `fixnum`. It would also mean that this value was assigned to the variable `i` accessible in the loop prologue, which is a type violation.
+
+**Accessing `i` in the loop prologue is valid**, as the forms inside the `LOOP` form (in particular, the epilogue) are in scope of the bindings, so they have access to the variables. According to [CLHS 6.1.1.4](http://www.lispworks.com/documentation/HyperSpec/Body/06_aad.htm):
+
+> A loop macro form expands into a form containing one or more binding forms (that establish bindings of loop variables) and a block and a tagbody (that express a looping control structure). The variables established in loop are bound as if by let or lambda.
+
+[CLHS Declaration TYPE](http://clhs.lisp.se/Body/d_type.htm) states:
+> 1. During the execution of any reference to the declared variable within the scope of the declaration, the consequences are undefined if the value of the declared variable is not of the declared type.
+> 2. During the execution of any setq of the declared variable within the scope of the declaration, the consequences are undefined if the newly assigned value of the declared variable is not of the declared type. 
+
+[CLHS 1.5.2](http://www.lispworks.com/documentation/HyperSpec/Body/01_eb.htm) states:
+> Conforming code shall not depend on the consequences of undefined or unspecified situations. 
+
+This implies that that `**LOOP` with `OF-TYPE` invokes undefined behaviour if the `OF-TYPE` is incorrect**, even in safe code. Therefore the question is whether the code from form 3 is conforming or not; I argue that it is conforming, since the user wants to perform an iteration for every fixnum. 
+
+If this code conforms, then the value of `i` must not exceed the fixnum range, which requires that `(1+ most-positive-fixnum)` must NOT be assigned to the variable `i`, which means that `finally (return i)` must NOT return `(1+ most-positive-fixnum)`, which in turn implies that `most-positive-fixnum` must be returned, which in turn implies that the `LOOP` variable must not be assigned an out-of-range value. This behaviour in turn translates to looping from `1` to `5`, at which point `5` must be returned.