The `x + 1` that is evaluated to give the value that `y` gets bound to uses the (more local) binding of `x` to `5`, not the (previous, less local) binding of `x` to `0`. By the way, the parentheses in that displayed expression were just to focus your attention. It would have parsed and meant the same without them.
-Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.
+Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument `M` to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.
If we restricted ourselves to only that usage of λ-expressions, that is when they were applied to all the arguments they're expecting, then we wouldn't have moved very far from the decidable fragment of arithmetic we began with.
For the time being, these are the only patterns we'll allow. But since the definition of patterns is recursive, this permits very complex patterns. What would this evaluate to:
let
- ([x, y], [z:zs, w]) match ([[], 'true], [[10, 20, 30], 'false])
- in (z, y)
+ ([xs, ys], [z:zs, ws]) match ([[], [1]], [[10, 20, 30], [0]])
+ in z & ys
Also, we will permit complex patterns in λ-expressions, too. So you can write:
`factorial match` λ `n. case n of 0 then 1; _ then n * factorial (n - 1) end`
`in factorial`
-But there's a problem here. What value does `factorial` have when evaluating the expression `factorial (n - 1)`?
+But there's a problem here. What value does `factorial` have when evaluating the subexpression `factorial (n - 1)`?
As we said in class, the natural precedent for this with non-function variables would go something like this:
`length match` λ `xs. case xs of [] then 0; _:ys then 1 + length ys end`
`in length`
-This function accept a sequence `xs`, and if its empty returns `0`, else it says that its length is `1` plus whatever is the length of its remainder when you take away the first element. In programming circles, this remainder is commonly called the sequence's "tail" (and the first element is its "head").
+This function accept a sequence `xs`, and if it's empty returns `0`, else it says that its length is `1` plus whatever is the length of its remainder when you take away the first element. In programming circles, this remainder is commonly called the sequence's "tail" (and the first element is its "head").
Thus if we evaluated `length [10, 20, 30]`, that would give the same result as `1 + length [20, 30]`, which would give the same result as `1 + (1 + length [30])`, which would give the same result as `1 + (1 + (1 + length []))`. But `length []` is `0`, so our original expression evaluates to `1 + (1 + (1 + 0))`, or `3`.
This was a lot of material, and you may need to read it carefully and think about it, but none of it should seem profoundly different from things you're already accustomed to doing. What we worked our way up to was just the kind of recursive definitions of `factorial` and `length` that you volunteered in class, before learning any programming.
-You have all the materials you need now to do this week's [[assignment|assignment1]]. Some of you may find it easy. Many of you will not. But if you understand what we've done here, and give it your time and attention, we believe you can do it.
+You have all the materials you need now to do this week's [[assignment|/exercises/assignment1]]. Some of you may find it easy. Many of you will not. But if you understand what we've done here, and give it your time and attention, we believe you can do it.
There are also some [[advanced notes|week1 advanced notes]] extending this week's material.
+### Summary ###
+
+Here is the hierarchy of **values** that we've talked about so far.
+
+* Multivalues
+* Singular values, including:
+ * Atoms, including:
+ * Numbers: these are among the **literals**
+ * Symbolic atoms: these are also among the **literals**, and include:
+ * Booleans (or truth-values)
+ * Functions: these are not literals, but instead have to be generated by evaluating complex expressions
+ * Containers, including:
+ * the **literal containers** `[]` and `{}`
+ * Non-empty sequences, built using `&`
+ * Non-empty sets, built using `&`
+ * Tuples proper and other containers, to be introduced later
+
+We've also talked about a variety of **expressions** in our language, that evaluate down to various values (if their evaluation doesn't "crash" or otherwise go awry). These include:
+
+* All of the literal atoms and literal containers
+* Variables
+* Complex expressions that apply `&` or some variable understood to be bound to a function to some arguments
+* Various other complex expressions involving λ or `let` or `letrec` or `case`
+
+The special syntaxes `[10, 20, 30]` are just shorthand for the more offical syntax using `&` and `[]`, and likewise for `{10, 20, 30}`. The `if ... then ... else ...` syntax is just shorthand for a `case`-construction using the literal patterns `'true` and `'false`.
+
+We also talked about **patterns**. These aren't themselves expressions, but form part of some larger expressions.
+