Improve Boxes

docs/source/tutorials/Boxes.md

@@ -8,11 +8,11 @@ syntax | effect
 `!T` | The type of a boxed term
 `dup x = t; u` | Unboxes `t` and copies it as `x` inside `u`
 
-The `dup` primitive is extremally important, because it performs deep copies of terms lazily, in a way that allows optimal sharing of sub-expressions. It is what makes Formality a great closure evaluator. But, in order to use it properly, you must understand how it is limited: the stratification condition.
+The `dup` primitive is the one responsible for copying, and is is extremelly important, as it performs those copies lazily, in a way that allows optimal sharing of sub-expressions. It is what makes Formality a great closure evaluator. But, in order to use it properly, you must understand how it is limited: the stratification condition.
 
 ## The Stratification Condition
 
-Deep copies, without restriction, would be very dangerous. For example, this program:
+The primitives above, without restriction, would be dangerous. For example, this:
 
 ```javascript
 main
@@ -24,48 +24,64 @@ main
 
 Would loop forever, which should never happen in a terminating language. To solve that, Formality relies on the **stratification condition**. It, in short, enforces the following invariant:
 
-> The level a term can never change during the program evaluation.
+> The level of a term can never change during the program evaluation.
 
-Where the level of a term is the number of boxes (`#`s) wrapping it on the syntax tree. For example, here:
+Where the level of a term is the number of boxes "wrapping" it.
+
+### Counting the level of a term
+
+To understand the restriction above, you must be able to count the level of a term. Let's do it on the following example:
 
 ```javascript
-["a", [#"b", #[#"c", ##"d"]]]
+["a", #"b", "c", #some_func("d", #"e"), ##"f"]
 ```
 
-The string `"a"` isn't wrapped by any box. As such, it is on `level 0`. The string `"b"` is wrapped by one box, so it is on `level 1`. The entire `[#"c", ##"d"]` pair is wrapped by one box, so, `"c"` is wrapped by 2 boxes in total and, thus, is on `level 2`, while `"d"` is wrapped by 3 boxes in total and, thus, is on `level 3`. 
+- The string `"a"` isn't wrapped by any box. It is on `level 0`.
+
+- The string `"b"` is wrapped by one box. It is on `level 1`.
+
+- The string `"c"` isn't wrapped by any box. It is on `level 0`.
+
+- The string `"d"` is wrapped by one box. It is on `level 1`.
+
+- The string `"e"` is wrapped by two boxes (one indirect). It is on `level 2`. 
+
+- The string `"f"` is wrapped by two boxes. It is on `level 2`. 
+
+### Stratification examples
 
-This condition forbids certain programs from being accepted. For example, this one:
+This condition is imposed globally, forbidding certain programs. For example:
 
 ```javascript
 box : {x : Word} -> !Word 
   # x
 ```
 
-Isn't allowed because, if it was, we would be able to increase the level of a word. Similarly, this one:
+This isn't allowed because, otherwise, we would be able to increase the level of a word. Similarly, this:
 
 ```javascript
 main : [:Word, Word]
   dup x = #42
   [x, x]
 ```
 
-Isn't allowed, because `42` would jump from `level 1` to `level 0` during runtime. But this one is fine:
+Isn't allowed too, because `42` would jump from `level 1` to `level 0` during runtime. But this:
 
 ```javascript
 main : ![:Word, Word]
   dup x = #42
   # [x, x]
 ```
 
-Because `42` remains on `level 1` after being copied. This one is fine too:
+Is fine, because `42` remains on `level 1` after being copied. And this:
 
 ```javascript
 main : [:!Word, !Word]
   dup x = #42
   [#x, #x]
 ```
 
-For the same reason.
+Is fine too, for the same reason.
 
 Because of this, boxes aren't really useful for copying data: information can only flow from lower to higher levels. That is, a term triggering a `dup` must be one level below the term copied, it won't be able to read the results of that copy. But boxes are very useful for implementing control structure: bounded loops, recursion, etc. In fact, Formality's recursive functions are actually desugared to an application of inductive Nats, which use boxes internally.