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,54 +24,87 @@ 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", #"e"], ##"f"]
+```
+
+- 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`. 
+
+The type of the program above is:
 
 ```javascript
-["a", [#"b", #[#"c", ##"d"]]]
+[:String, :!String, :String, :![:String, !String], !!String]
 ```
 
-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`. 
+### 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.
+## Applications
 
-## Implementing Loops and Recursion
+### Copying "static" data
 
-While Formality has a built-in syntax for recursion, it can be insightful to understand how it is implemented under the hoods. To understand it, mind the following program:
+In general of this, boxes aren't very useful for copying data. That's because information can only flow from lower to higher levels. So, for example, if some piece of data is generated on level `2`, you can copy it on level `3`, but you can't use it again on level `2`. Generally, your program's logic should stay on the highest level, with the lower levels being used to copy static data and generate bounded-depth recursive functions. In fact, Formality's syntax sugars and standard libraries are designed to be used with two levels only: the level `0`, where recursive functions are created and static data is duplicated, and the level 1, where everything is used. So, for example, the `Data.List/map` function on `Base` uses level `0` to make multiple copies of `f`, which are used on level `1`:
+
+```javascript
+#map*n : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
+| cons => cons(~B, f(list.head), map(list.tail))
+| nil  => nil(~B)
+halt: nil(~B)
+```
+
+### Implementing loops/recursion
+
+While Formality has a built-in syntax for recursion, it can be insightful to understand how it is implemented under the hoods. Mind the following program:
 
 ```javascript
 ten_times : {~T : Type, f : !{x : T} -> T, x : !T} -> !T
@@ -107,5 +140,28 @@ main : !Word
   # fact(6)
 ```
 
-We "emulate" a recursive function by using `ten_times` to "build" the recursion tree of "fact" up to 10 layers deep. As such, it only works for inputs up to 10; after that, it hits the "halt" case and returns 0. The good thing about this way of doing recursion is that we're not limited to recurse on structurally smaller arguments. The bad thing is that it is a little bit verbose, requiring an explicit bound, and a halting case for when the function "runs out of gas". Moreover, since we used `ten_times` to make the function, it comes inside a box, on `level 1`. In other words, it is impossible to use it on `level 0`! Instead, we must use the `level 0` to unbox it (with a `dup`), and then use it on `level 1`.
+We "emulate" a recursive function by using `ten_times` to "build" the recursion tree of "fact" up to 10 layers deep. As such, it only works for inputs up to 10; after that, it hits the "halt" case and returns 0. The good thing about this way of doing recursion is that we're not limited to recurse on structurally smaller arguments. The bad thing is that it is a little bit verbose, requiring an explicit bound, and a halting case for when the function "runs out of gas". Moreover, since we used `ten_times` to make the function, it comes inside a box, on `level 1`. In other words, it is impossible to use it on `level 0`! Instead, we must use the `level 0` to unbox it (with a `dup`), and then use it on `level 1`. As usual, you could simplify it with a boxed definition:
+
+```javascript
+#main : !Word
+  <fact>(6)
+```
+
+Formality's recursion syntax builds a similar program, except: 
+
+1. Instead of a hard-coded max call limit, it is configurable `*N`.
+
+2. Instead of simple repetition, it uses Nat induction, allowing you to use the call count, `N`, in types.
+
+So, for example, when you write:
+
+```javascript
+#fact*N : ! {i : Word} -> Word
+  if i .= 0:
+    1
+  else:
+    i * fact(i - 1)
+halt: 0
+```
 
+It gives you a `fact : {N : Ind} -> !{n : Word} -> Word`, instead of a `fact : !{n : Word} -> Word`. You can call it inside a boxed definition with `<fact*MAX_CALLS>(x)`.

docs/source/tutorials/Recursion.md

@@ -43,14 +43,24 @@ Formality allows you to turn a boxed definition into a recursive function by app
   else:
     i * fact(i - 1)
 halt: 0
-
-#main : !Word
-  <fact*100>(12) // 100 is the call limit; write `<fact*>` to use 2^256-1
 ```
 
-This is not much different from the usual `fact` definition, except we explicitly set the "halt-case" to be `0` on the last line. That means that, if the function "runs out of gas", it will stop and return `0` instead. As a shortcut, if your "halt-case" is simply one of the function's argument, you can write the `*` on it instead, as in, `fact*N ! {*i : Word} -> Word`. 
+This is not much different from the usual `fact` definition, except we explicitly set the "halt-case" to be `0` on the last line. That means that, if the function "runs out of gas", it will stop and return `0` instead. As a shortcut, if your "halt-case" is simply one of the function's argument, you can write the `*` on it instead, as in, `fact*N ! {*i : Word} -> Word`. To call it, you must set an explicit max call limit with `*N`:
+
+```javascript
+main : !Word
+  dup f = fact*100
+  # f(12)
+```
+
+Or, with boxed definitions:
+
+```javascript 
+#main : !Word
+  <fact*100>(12)
+```
 
-The maximum recursion depth of the `Ind` defined by the base library is `2^256-1`. In other words, despite being terminating, in practice, Formality is capable of doing anything a Turing-complete language could do. After all, no language could perform more than `2^256-1` calls without getting a stack-overflow, or exhausting your computer's CPU/memory.
+The `f*N` syntax configures the call limit of a recursive function. Here, we used `100`. Note this is actually just a shortcut for a function application: we could have written `fact(*100)` instead. We could also have omitted the number, as in, `<fact*>(x)`, which would default to `2^256-1`. This limit is so absurdly large that, for all practical purposes, our functions are no less powerful than the ones found in other languages. After all, `2^256-1` is so large that no real computer could reach this amount of calls anyway. In fact, the entire observable universe has less particles than that!
 
 ## (TODO)