∀x. (F x or ∀x (not (F x)))
+
+
+ When a previously-bound variable is rebound in the way we see here, that's called **shadowing**: the outer binding is shadowed during the scope of the inner binding.
+
+ See also:
+
+ * [[!wikipedia Variable shadowing]]
+
+
+Some more comparisons between Scheme and OCaml
+----------------------------------------------
+
+* Simple predefined values
+
+ Numbers in Scheme: `2`, `3`
+ In OCaml: `2`, `3`
+
+ Booleans in Scheme: `#t`, `#f`
+ In OCaml: `true`, `false`
+
+ The eighth letter in the Latin alphabet, in Scheme: `#\h`
+ In OCaml: `'h'`
+
+* Compound values
+
+ These are values which are built up out of (zero or more) simple values.
+
+ Ordered pairs in Scheme: `'(2 . 3)` or `(cons 2 3)`
+ In OCaml: `(2, 3)`
+
+ Lists in Scheme: `'(2 3)` or `(list 2 3)`
+ In OCaml: `[2; 3]`
+ We'll be explaining the difference between pairs and lists next week.
+
+ The empty list, in Scheme: `'()` or `(list)`
+ In OCaml: `[]`
+
+ The string consisting just of the eighth letter of the Latin alphabet, in Scheme: `"h"`
+ In OCaml: `"h"`
+
+ A longer string, in Scheme: `"horse"`
+ In OCaml: `"horse"`
+
+ A shorter string, in Scheme: `""`
+ In OCaml: `""`
+
+
+
diff --git a/topics_and_themes.mdwn b/_topics_and_themes.mdwn
similarity index 55%
rename from topics_and_themes.mdwn
rename to _topics_and_themes.mdwn
index ab4a5338..6b4c55fb 100644
--- a/topics_and_themes.mdwn
+++ b/_topics_and_themes.mdwn
@@ -1,4 +1,27 @@
-*Coming, please wait...*
+# Topics #
+
+These topics are organized in two ways: by their content, and by the
+week in which they were introduced.
+
+## Topics by content ##
+
+* [[Basics of functional programming|topics/week1]]
+
+* [[Order: static versus dynamic|topics/week1 order]]
+
+## Topics by week ##
+
+Week 1:
+
+* [[Order in programming languages and natural language|topics/order]]
+This discussion considers conjunction in a language that recognized presupposition failure.
+* [[Introduction to functional programming|topics/week1]]
+Basics of functional programming: `let`, `case`, pattern matching, and
+recursion. Definitions of factorial.
+* [[Homework for week 1|exercises/assignment1]]
+* [[Advanced notes|week1 advanced notes]]
+
+*More coming, please wait...*
+
+ `newtype` and `data` on the other hand, create genuinely new types. `newtype` is basically just an efficient version of `data` that you can use in special circumstances. `newtype` must always take one type argument and have one value constructor. For example:
+
+ newtype PersonalData a = PD a
+
+ You could also say:
+
+ data PersonalData2 a = PD2 a
+
+ And `data` also allows multiple type arguments, and multiple variants and value constructors.
+
+ OCaml just uses the one keyword `type` for all of these purposes:
+
+ type weight = int;;
+ type person = name * address;;
+ type 'a personal_data = PD of 'a;;
+
+* When a type only has a single variant, as with PersonalData, Haskell programmers will often use the same name for both the type and the value constructor, like this:
+
+ data PersonalData3 a = PersonalData3 a
+
+ The interpreter can always tell from the context when you're using the type name and when you're using the value constructor.
+
+* The type constructors discussed above took simple types as arguments. In Haskell, types are also allowed to take *type constructors* as arguments:
+
+ data BarType t = Bint (t Integer) | Bstring (t string)
+
+ One does this for example when defining monad transformers---the type constructor `ReaderT` takes some base monad's type constructor as an argument.
+
+ The way to do this this in OCaml is less straightforward. [See here](/code/tree_monadize.ml) for an example.
+
+* Haskell has a notion of *type-classes*. They look like this:
+
+ class Eq a where
+ (==) :: a -> a -> Bool
+
+ This declares the type-class `Eq`; in order to belong to this class, a type `a` will have to supply its own implementation of the function `==`, with the type `a -> a -> Bool`. Here is how the `Integer` class signs up to join this type-class:
+
+ instance Eq Integer where
+ x == y = ... some definition for the Integer-specific version of that function here ...
+
+ Type expressions can be conditional on some of their parameters belonging to certain type-classes. For example:
+
+ elem :: (Eq a) => a -> [a] -> Bool
+
+ says that the function `elem` is only defined over types `a` that belong to the type-class `Eq`. For such types `a`, `elem` has the type `a -> [a] -> Bool`.
+
+ Similarly:
+
+ instance (Eq a) => Eq (Tree a) where
+ Leaf a == Leaf b = a == b
+ (Branch l1 r1) == (Branch l2 r2) = (l1==l2) && (r1==r2)
+ _ == _ = False
+
+ says that if `a` belongs to the typeclass `Eq`, then so too does `Tree a`, and in such cases here is the implementation of `==` for `Tree a`...
+
+* OCaml doesn't have type-classes. You can do something similar with OCaml modules that take are parameterized on other modules. Again, [see here](/code/tree_monadize.ml) for an example.
+
+
+* Some specific differences in how certain types are expressed. This block in Haskell:
+
+ Prelude> type Maybe a = Nothing | Just a
+ Prelude> let x = [] :: [Int]
+ Prelude> :t x
+ x :: [Int]
+ Prelude> let x = () :: ()
+ Prelude> let x = (1, True) :: (Int, Bool)
+
+ corresponds to this block in OCaml:
+
+ # type 'a option = None | Some of 'a;;
+ type 'a option = None | Some of 'a
+ # let (x : int list) = [];;
+ val x : int list = []
+ # let (x : unit) = ();;
+ val x : unit = ()
+ # let (x : int * bool) = (1, true);;
+ val x : int * bool = (1, true)
+
+* Haskell has a plethora of numerical types, including the two types `Int` (integers limited to a machine-dependent range) and `Integer` (unbounded integers). The same arithmetic operators (`+` and so on) work for all of these. OCaml also has several different numerical types (though not as many). In OCaml, by default, one has to use a different numerical operator for each type:
+
+ # 1 + 2;;
+ - : int = 3
+ # 1.0 + 2.0;;
+ Error: This expression has type float but an expression was expected of type int
+ # 1.0 +. 2.0;;
+ - : float = 3.
+
+ However the comparison operators are polymorphic. You can equally say:
+
+ # 1 = 2;;
+ - : bool = false
+ # 1.0 = 2.0;;
+ - : bool = false
+ # 2 > 1;;
+ - : bool = true
+ # 2.0 > 1.0;;
+ - : bool = true
+
+ But you must still apply these operators to expressions of the same type:
+
+ # 2.0 > 1;;
+ Error: This expression has type int but an expression was expected of type float
+
+* We'll discuss differences between Haskell's and OCaml's record types below.
+
+
+##Lists, Tuples, Unit, Booleans##
+
+* As noted above, Haskell describes the type of a list of `Int`s as `[Int]`. OCaml describes it as `int list`. Haskell describes the type of a pair of `Int`s as `(Int, Int)`. OCaml describes it as `int * int`. Finally, Haskell uses `()` to express both the unit type and a value of that type. In OCaml, one uses `()` for the value and `unit` for the type.
+
+* Haskell describes the boolean type as `Bool` and its variants are `True` and `False`. OCaml describes the type as `bool` and its variants are `true` and `false`. This is an inconsistency in OCaml: other value constructors must always be capitalized.
+
+* As noted above, in Haskell one builds up a list by saying `1 : [2, 3]`. In OCaml one says `1 :: [2; 3]`. In Haskell, one can test whether a list is empty with either:
+
+ lst == []
+ null lst
+
+ In OCaml, there is no predefined `null` or `isempty` function. One can still test whether a list is empty using the comparison `lst = []`.
+
+* In Haskell, the expression `[1..5]` is the same as `[1,2,3,4,5]`, and the expression `[0..]` is a infinite lazily-evaluated stream of the natural numbers. In OCaml, there is no `[1..5]` shortcut, lists must be finite, and they are eagerly evaluated. It is possible to create lazy streams in OCaml, even infinite ones, but you have to use other techniques than the native list type.
+
+* Haskell has *list comprehensions*:
+
+ [ x * x | x <- [1..10], odd x]
+
+ In OCaml, one has to write this out longhand:
+
+ List.map (fun x -> x * x) (List.filter odd [1..10]);;
+
+* In Haskell, the expressions `"abc"` and `['a','b','c']` are equivalent. (Strings are just lists of `char`s.) In OCaml, these expressions have two different types.
+
+ Haskell uses the operator `++` for appending both strings and lists (since Haskell strings are just one kind of list). OCaml uses different operators:
+
+ # "string1" ^ "string2";;
+ - : string = "string1string2"
+ # ['s';'t'] @ ['r';'i';'n';'g'];;
+ - : char list = ['s'; 't'; 'r'; 'i'; 'n'; 'g']
+ # (* or equivalently *)
+ List.append ['s';'t'] ['r';'i';'n';'g'];;
+ - : char list = ['s'; 't'; 'r'; 'i'; 'n'; 'g']
+
+
+##Let and Where##
+
+* Haskell permits both:
+
+ foo x =
+ let result1 = x * x
+ result2 = x + 1
+ in result1 + result2
+
+ and:
+
+ foo x = result1 + result2
+ where result1 = x * x
+ result2 = x + 1
+
+ OCaml permits only:
+
+ let foo x =
+ let result1 = x * x
+ in let result2 = x + 1
+ in result1 + result2;;
+
+##Patterns##
+
+* In OCaml:
+
+ # let (x, y) as both = (1, 2)
+ in (both, x, y);;
+ - : (int * int) * int * int = ((1, 2), 1, 2)
+
+
+ The same in Haskell:
+
+ let both@(x,y) = (1, 2)
+ in (both, x, y)
+
+* In OCaml:
+
+ match list_expression with
+ | y::_ when odd y -> result1
+ | y::_ when y > 5 -> result2
+ | y::_ as whole -> (whole, y)
+ | [] -> result4
+
+ The same in Haskell:
+
+ case list_expression of
+ (y:_) | odd y -> result1
+ | y > 5 -> result2
+ whole@(y:_) -> (whole, y)
+ [] -> result4
+
+
+##Records##
+
+Haskell and OCaml both have `records`, which are essentially just tuples with a pretty interface. We introduced these in the wiki notes [here](/coroutines_and_aborts/).
+
+The syntax for declaring and using these is a little bit different in the two languages.
+
+* In Haskell one says:
+
+ -- declare a record type
+ data Color = Col { red, green, blue :: Int }
+ -- create a value of that type
+ let c = Col { red = 0, green = 127, blue = 255 }
+
+ In OCaml one says instead:
+
+ type color = { red : int; green : int; blue : int };;
+ let c = { red = 0; green = 127; blue = 255 }
+
+ Notice that OCaml doesn't use any value constructor `Col`. The record syntax `{ red = ...; green = ...; blue = ... }` is by itself the constructor. The record labels `red`, `green`, and `blue` cannot be re-used for any other record type.
+
+* In Haskell, one may have multiple constructors for a single record type, and one may re-use record labels within that type, so long as the labels go with fields of the same type:
+
+ data FooType = Constructor1 {f :: Int, g :: Float} | Constructor2 {f :: Int, h :: Bool}
+
+* In Haskell, one can extract a single field of a record like this:
+
+ let c = Col { red = 0, green = 127, blue = 255 }
+ in red c -- evaluates to 0
+
+ In OCaml one says:
+
+ let c = { red = 0; green = 127; blue = 255 }
+ in c.red (* evaluates to 0 *)
+
+* In both languages, there is a special syntax for creating a copy of an existing record, with some specified fields altered. In Haskell:
+
+ let c2 = c { green = 50, blue = 50 }
+ -- evaluates to Col { red = red c, green = 50, blue = 50 }
+
+ In OCaml:
+
+ let c2 = { c with green = 50; blue = 50 }
+ (* evaluates to { red = c.red; green = 50; blue = 50 }
+
+* One pattern matches on records in similar ways. In Haskell:
+
+ let Col { red = r, green = g } = c
+ in r
+
+ In OCaml:
+
+ let { red = r; green = g; _ } = c
+ in r
+
+ In Haskell:
+
+ makegray c@(Col { red = r } ) = c { green = r, blue = r }
+
+ is equivalent to:
+
+ makegray c = let Col { red = r } = c
+ in { red = r, green = r, blue = r }
+
+ In OCaml it's:
+
+ # let makegray ({ red = r; _ } as c) = { c with green=r; blue=r };;
+ val makegray : color -> color = Scheme (functional part) | OCaml (functional part) | C, Java, Python +Scheme (imperative part) +OCaml (imperative part) |
untyped lambda calculus +combinatorial logic | ||
--------------------------------------------------- Turing complete --------------------------------------------------- | ||
+ | more advanced type systems, such as polymorphic types + | + |
+ | simply-typed lambda calculus (what linguists mostly use) + | + |
Scheme (functional part) | OCaml (functional part) | C, Java, Python +Scheme (imperative part) +OCaml (imperative part) |
untyped lambda calculus +combinatorial logic | ||
--------------------------------------------------- Turing complete --------------------------------------------------- | ||
+ | more advanced type systems, such as polymorphic types + | + |
+ | simply-typed lambda calculus (what linguists mostly use) + | + |
λx
as `\x`.
+
+1. `(\x \y. y x) z`
+2. `(\x (x x)) z`
+3. `(\x (\x x)) z`
+4. `(\x (\z x)) z`
+5. `(\x (x (\y y))) (\z (z z))`
+6. `(\x (x x)) (\x (x x))`
+7. `(\x (x x x)) (\x (x x x))`
+
+
+Booleans
+--------
+
+Recall our definitions of true and false.
+
+> **true** is defined to be `\t \f. t`
+> **false** is defined to be `\t \f. f`
+
+In Racket, these can be defined like this:
+
+ (define true (lambda (t) (lambda (f) t)))
+ (define false (lambda (t) (lambda (f) f)))
+
++Variables:+ +Each variable is an expression. For any expressions M and N and variable a, the following are also expressions: + +x
,y
,z
... +
+Abstract: (λa M)
+
+
+We'll tend to write (λa M)
as just `(\a M)`, so we don't have to write out the markup code for the λ
. You can yourself write (λa M)
or `(\a M)` or `(lambda a M)`.
+
+
+Application: (M N)
+
+
+
+Examples of expressions:
+
+ x
+ (y x)
+ (x x)
+ (\x y)
+ (\x x)
+ (\x (\y x))
+ (x (\x x))
+ ((\x (x x)) (\x (x x)))
+
+The lambda calculus has an associated proof theory. For now, we can regard the
+proof theory as having just one rule, called the rule of **beta-reduction** or
+"beta-contraction". Suppose you have some expression of the form:
+
+ ((\a M) N)
+
+that is, an application of an abstract to some other expression. This compound form is called a **redex**, meaning it's a "beta-reducible expression." `(\a M)` is called the **head** of the redex; `N` is called the **argument**, and `M` is called the **body**.
+
+The rule of beta-reduction permits a transition from that expression to the following:
+
+ M [a:=N]
+
+What this means is just `M`, with any *free occurrences* inside `M` of the variable `a` replaced with the term `N`.
+
+What is a free occurrence?
+
+> An occurrence of a variable `a` is **bound** in T if T has the form `(\a N)`.
+
+> If T has the form `(M N)`, any occurrences of `a` that are bound in `M` are also bound in T, and so too any occurrences of `a` that are bound in `N`.
+
+> An occurrence of a variable is **free** if it's not bound.
+
+For instance:
+
+
+> T is defined to be `(x (\x (\y (x (y z)))))`
+
+The first occurrence of `x` in T is free. The `\x` we won't regard as containing an occurrence of `x`. The next occurrence of `x` occurs within a form that begins with `\x`, so it is bound as well. The occurrence of `y` is bound; and the occurrence of `z` is free.
+
+To read further:
+
+* [[!wikipedia Free variables and bound variables]]
+
+Here's an example of beta-reduction:
+
+ ((\x (y x)) z)
+
+beta-reduces to:
+
+ (y z)
+
+We'll write that like this:
+
+ ((\x (y x)) z) ~~> (y z)
+
+Different authors use different notations. Some authors use the term "contraction" for a single reduction step, and reserve the term "reduction" for the reflexive transitive closure of that, that is, for zero or more reduction steps. Informally, it seems easiest to us to say "reduction" for one or more reduction steps. So when we write:
+
+ M ~~> N
+
+We'll mean that you can get from M to N by one or more reduction steps. Hankin uses the symbol →
for one-step contraction, and the symbol ↠
for zero-or-more step reduction. Hindley and Seldin use ⊳_{1}
and ⊳
.
+
+When M and N are such that there's some P that M reduces to by zero or more steps, and that N also reduces to by zero or more steps, then we say that M and N are **beta-convertible**. We'll write that like this:
+
+ M <~~> N
+
+This is what plays the role of equality in the lambda calculus. Hankin uses the symbol `=` for this. So too do Hindley and Seldin. Personally, I keep confusing that with the relation to be described next, so let's use this notation instead. Note that `M <~~> N` doesn't mean that each of `M` and `N` are reducible to each other; that only holds when `M` and `N` are the same expression. (Or, with our convention of only saying "reducible" for one or more reduction steps, it never holds.)
+
+In the metatheory, it's also sometimes useful to talk about formulas that are syntactically equivalent *before any reductions take place*. Hankin uses the symbol ≡
for this. So too do Hindley and Seldin. We'll use that too, and will avoid using `=` when discussing the metatheory. Instead we'll use `<~~>` as we said above. When we want to introduce a stipulative definition, we'll write it out longhand, as in:
+
+> T is defined to be `(M N)`.
+
+We'll regard the following two expressions:
+
+ (\x (x y))
+
+ (\z (z y))
+
+as syntactically equivalent, since they only involve a typographic change of a bound variable. Read Hankin section 2.3 for discussion of different attitudes one can take about this.
+
+Note that neither of those expressions are identical to:
+
+ (\x (x w))
+
+because here it's a free variable that's been changed. Nor are they identical to:
+
+ (\y (y y))
+
+because here the second occurrence of `y` is no longer free.
+
+There is plenty of discussion of this, and the fine points of how substitution works, in Hankin and in various of the tutorials we've linked to about the lambda calculus. We expect you have a good intuitive understanding of what to do already, though, even if you're not able to articulate it rigorously.
+
+* [More discussion in week 2 notes](/week2/#index1h1)
+
+
+Shorthand
+---------
+
+The grammar we gave for the lambda calculus leads to some verbosity. There are several informal conventions in widespread use, which enable the language to be written more compactly. (If you like, you could instead articulate a formal grammar which incorporates these additional conventions. Instead of showing it to you, we'll leave it as an exercise for those so inclined.)
+
+
+**Parentheses** Outermost parentheses around applications can be dropped. Moreover, applications will associate to the left, so `M N P` will be understood as `((M N) P)`. Finally, you can drop parentheses around abstracts, but not when they're part of an application. So you can abbreviate:
+
+ (\x (x y))
+
+as:
+
+ \x (x y)
+
+but you should include the parentheses in:
+
+ (\x (x y)) z
+
+and:
+
+ z (\x (x y))
+
+
+**Dot notation** Dot means "put a left paren here, and put the right
+paren as far the right as possible without creating unbalanced
+parentheses". So:
+
+ \x (\y (x y))
+
+can be abbreviated as:
+
+ \x (\y. x y)
+
+and that as:
+
+ \x. \y. x y
+
+This:
+
+ \x. \y. (x y) x
+
+abbreviates:
+
+ \x (\y ((x y) x))
+
+This on the other hand:
+
+ (\x. \y. (x y)) x
+
+abbreviates:
+
+ ((\x (\y (x y))) x)
+
+
+**Merging lambdas** An expression of the form `(\x (\y M))`, or equivalently, `(\x. \y. M)`, can be abbreviated as:
+
+ (\x y. M)
+
+Similarly, `(\x (\y (\z M)))` can be abbreviated as:
+
+ (\x y z. M)
+
+
+Lambda terms represent functions
+--------------------------------
+
+The untyped lambda calculus is Turing complete: all (recursively computable) functions can be represented by lambda terms. For some lambda terms, it is easy to see what function they represent:
+
+> `(\x x)` represents the identity function: given any argument `M`, this function
+simply returns `M`: `((\x x) M) ~~> M`.
+
+> `(\x (x x))` duplicates its argument:
+`((\x (x x)) M) ~~> (M M)`
+
+> `(\x (\y x))` throws away its second argument:
+`(((\x (\y x)) M) N) ~~> M`
+
+and so on.
+
+It is easy to see that distinct lambda expressions can represent the same
+function, considered as a mapping from input to outputs. Obviously:
+
+ (\x x)
+
+and:
+
+ (\z z)
+
+both represent the same function, the identity function. However, we said above that we would be regarding these expressions as synactically equivalent, so they aren't yet really examples of *distinct* lambda expressions representing a single function. However, all three of these are distinct lambda expressions:
+
+ (\y x. y x) (\z z)
+
+ (\x. (\z z) x)
+
+ (\z z)
+
+yet when applied to any argument M, all of these will always return M. So they have the same extension. It's also true, though you may not yet be in a position to see, that no other function can differentiate between them when they're supplied as an argument to it. However, these expressions are all syntactically distinct.
+
+The first two expressions are *convertible*: in particular the first reduces to the second. So they can be regarded as proof-theoretically equivalent even though they're not syntactically identical. However, the proof theory we've given so far doesn't permit you to reduce the second expression to the third. So these lambda expressions are non-equivalent.
+
+There's an extension of the proof-theory we've presented so far which does permit this further move. And in that extended proof theory, all computable functions with the same extension do turn out to be equivalent (convertible). However, at that point, we still won't be working with the traditional mathematical notion of a function as a set of ordered pairs. One reason is that the latter but not the former permits many uncomputable functions. A second reason is that the latter but not the former prohibits functions from applying to themselves. We discussed this some at the end of Monday's meeting (and further discussion is best pursued in person).
+
+
+
+Booleans and pairs
+==================
+
+Our definition of these is reviewed in [[Assignment1]].
+
+
+It's possible to do the assignment without using a Scheme interpreter, however
+you should take this opportunity to [get Scheme installed on your
+computer](/how_to_get_the_programming_languages_running_on_your_computer), and
+[get started learning Scheme](/learning_scheme). It will help you test out
+proposed answers to the assignment.
+
+
+There's also a (slow, bare-bones, but perfectly adequate) version of Scheme available for online use at