From: Chris Date: Sun, 1 Feb 2015 19:52:34 +0000 (-0500) Subject: stupid git X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=d7dd23c2ace59bf557f247e57fe75190a4d1e798;hp=247d01832209e40ef4dffa3746fded9f74052674 stupid git --- diff --git a/_applications.mdwn b/_applications.mdwn new file mode 100644 index 00000000..37d06d21 --- /dev/null +++ b/_applications.mdwn @@ -0,0 +1,40 @@ +*This page is not ready to go live; just roughly copying over some material from last year.* + +*Coming, please wait...* + + + +We mentioned a number of linguistic and philosophical applications of the tools that we'd be helping you learn in the seminar. (We really do mean "helping you learn," not "teaching you." You'll need to aggressively browse and experiment with the material yourself, or nothing we do in a few two-hour sessions will succeed in inducing mastery of it.) + +From linguistics +---------------- + +* Generalized quantifiers are a special case of operating on continuations. [[!wikipedia Richard_Montague]] analyzed all NPs, including, e.g., proper names, as sets of properties. + This gives names and quantificational NPs the same semantic type, which explain why we can coordinate them (*John and everyone*, *Mary or some graduate student*). So instead of thinking of a name as refering to an individual, which then serves as the argument to a verb phrase, in the Generalized Quantifier conception, the name denotes a higher-order function that takes the verb phrase (its continuation) as an argument. Montague only continuized +one syntactic category (NPs), but a more systematic approach would continuize uniformly throughout the grammar. +See [a paper by me (CB)](http://dx.doi.org/10.1023/A:1022183511876) for detailed discussion. + +* Computing the meanings of expressions involving focus. Consider the difference in meaning between *John only drinks Perrier*, with main sentence accent on *Perrier*, versus *John only DRINKs Perrier*. Mats Rooth, in his 1995 dissertation, showed how to describe these meanings by having the focussed expression contribute a normal denotation and a focus alternative set denotation. The focus alternative sets had to be propagated upwards through the compositional semantics. One way to implement this idea is by means of delimited continuations, making use of operators similar to fcontrol and run proposed for a scheme-like language by Sitaram and other computer scienticsts. See [another paper by CB](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.9748&rep=rep1&type=pdf). + +* Generalized coordination, as proposed by Partee and Rooth in highly influential papers in the 1980s. The idea is that the way that *John saw Mary or Bill* comes to mean *John saw Mary or John saw Bill* is by cloning the context of the direct object, feeding one of the clones *Mary*, feeding the other clone *Bill*, and disjoining the resulting propositions. See either of the two papers mentioned in the previous two items for discussion. + +* Anaphora, as in *Everyone's mother loves him* (which says that for every person x, x's mother loves x). [A paper by CB and Chung-chieh Shan](http://dx.doi.org/10.1007/s10988-005-6580-7) discusses an implementation in terms of delimited continuations. See also a different implementation in work of [Philippe de Groote](http://ecommons.library.cornell.edu/bitstream/1813/7577/4/salt16_degroote_1_16.pdf). + +* As suggested in class, it is possible to think of the side effects of expressives such as *damn* in *John read the damn book* in terms of control operators such as call/cc in Scheme. +At the end of the seminar we gave a demonstration of modeling [[damn]] using continuations...see the [summary](/damn) for more explanation and elaboration. In the meantime, you can read a new paper about this idea [here](http://tinyurl.com/cbarker/barker-bernardi-shan-interaction.pdf)---comments welcome. + +From philosophy +--------------- + +* the natural semantics for positive free logic is thought by some to have objectionable ontological commitments; Jim says that thought turns on not understanding the notion of a "union type", and conflating the folk notion of "naming" with the technical notion of semantic value. We'll discuss this in due course. + +* those issues may bear on Russell's Gray's Elegy argument in "On Denoting" + +* and on discussion of the difference between the meaning of "is beautiful" and "beauty," and the difference between the meaning of "that snow is white" and "the proposition that snow is white." + +* the apparatus of monads, and techniques for statically representing the semantics of an imperatival language quite generally, are explicitly or implicitly invoked in dynamic semantics + +* the semantics for mutation will enable us to make sense of a difference between numerical and qualitative identity---for purely mathematical objects! + +* issues in that same neighborhood will help us better understand proposals like Kit Fine's that semantics is essentially coordinated, and that `R a a` and `R a b` can differ in interpretation even when `a` and `b` don't + diff --git a/_rosetta.mdwn b/_rosetta.mdwn new file mode 100644 index 00000000..2e6049ca --- /dev/null +++ b/_rosetta.mdwn @@ -0,0 +1,395 @@ +*This page is not ready to go live; just roughly copying over some material from last year.* + + +Rosetta Stone +============= + +Here's how it looks to say the same thing in various of these languages. + +The following site may be useful; it lets you run a Scheme interpreter inside your web browser: [Try Scheme in your web browser](http://tryscheme.sourceforge.net/). See also our links about [[learning Scheme]] and [[learning OCaml]]. + +  + +1. Function application and parentheses + + In Scheme and the lambda calculus, the functions you're applying always go to the left. So you write `(foo 2)` and also `(+ 2 3)`. + + Mostly that's how OCaml is written too: + + foo 2 + + But a few familiar binary operators can be written infix, so: + + 2 + 3 + + You can also write them operator-leftmost, if you put them inside parentheses to help the parser understand you: + + ( + ) 2 3 + + I'll mostly do this, for uniformity with Scheme and the lambda calculus. + + In OCaml and the lambda calculus, this: + + foo 2 3 + + means the same as: + + ((foo 2) 3) + + These functions are "curried". `foo 2` returns a `2`-fooer, which waits for an argument like `3` and then foos `2` to it. `( + ) 2` returns a `2`-adder, which waits for an argument like `3` and then adds `2` to it. For further reading: + +* [[!wikipedia Currying]] + + In Scheme, on the other hand, there's a difference between `((foo 2) 3)` and `(foo 2 3)`. Scheme distinguishes between unary functions that return unary functions and binary functions. For our seminar purposes, it will be easiest if you confine yourself to unary functions in Scheme as much as possible. + + Scheme is very sensitive to parentheses and whenever you want a function applied to any number of arguments, you need to wrap the function and its arguments in a parentheses. So you have to write `(foo 2)`; if you only say `foo 2`, Scheme won't understand you. + + Scheme uses a lot of parentheses, and they are always significant, never optional. Often the parentheses mean "apply this function to these arguments," as just described. But in a moment we'll see other constructions in Scheme where the parentheses have different roles. They do lots of different work in Scheme. + + +2. Binding suitable values to the variables `three` and `two`, and adding them. + + In Scheme: + + (let* ((three 3)) + (let* ((two 2)) + (+ three two))) + + Most of the parentheses in this construction *aren't* playing the role of applying a function to some arguments---only the ones in `(+ three two)` are doing that. + + + In OCaml: + + let three = 3 in + let two = 2 in + ( + ) three two + + In the lambda calculus: + + Here we're on our own, we don't have predefined constants like `+` and `3` and `2` to work with. We've got to build up everything from scratch. We'll be seeing how to do that over the next weeks. + + But supposing you had constructed appropriate values for `+` and `3` and `2`, you'd place them in the ellided positions in: + + (((\three (\two ((... three) two))) ...) ...) + + In an ordinary imperatival language like C: + + int three = 3; + int two = 2; + three + two; + +2. Mutation + + In C this looks almost the same as what we had before: + + int x = 3; + x = 2; + + Here we first initialize `x` to hold the value 3; then we mutate `x` to hold a new value. + + In (the imperatival part of) Scheme, this could be done as: + + (let ((x (box 3))) + (set-box! x 2)) + + In general, mutating operations in Scheme are named with a trailing `!`. There are other imperatival constructions, though, like `(print ...)`, that don't follow that convention. + + In (the imperatival part of) OCaml, this could be done as: + + let x = ref 3 in + x := 2 + + Of course you don't need to remember any of this syntax. We're just illustrating it so that you see that in Scheme and OCaml it looks somewhat different than we had above. The difference is much more obvious than it is in C. + + In the lambda calculus: + + Sorry, you can't do mutation. At least, not natively. Later in the term we'll be learning how in fact, really, you can embed mutation inside the lambda calculus even though the lambda calculus has no primitive facilities for mutation. + + + + +3. Anonymous functions + + Functions are "first-class values" in the lambda calculus, in Scheme, and in OCaml. What that means is that they can be arguments to, and results of, other functions. They can be stored in data structures. And so on. To read further: + + * [[!wikipedia Higher-order function]] + * [[!wikipedia First-class function]] + + We'll begin by looking at what "anonymous" functions look like. These are functions that have not been bound as values to any variables. That is, there are no variables whose value they are. + + In the lambda calculus: + + (\x M) + + ---where `M` is any simple or complex expression---is anonymous. It's only when you do: + + ((\y N) (\x M)) + + that `(\x M)` has a "name" (it's named `y` during the evaluation of `N`). + + In Scheme, the same thing is written: + + (lambda (x) M) + + Not very different, right? For example, if `M` stands for `(+ 3 x)`, then here is an anonymous function that adds 3 to whatever argument it's given: + + (lambda (x) (+ 3 x)) + + In OCaml, we write our anonymous function like this: + + fun x -> ( + ) 3 x + + +4. Supplying an argument to an anonymous function + + Just because the functions we built aren't named doesn't mean we can't do anything with them. We can give them arguments. For example, in Scheme we can say: + + ((lambda (x) (+ 3 x)) 2) + + The outermost parentheses here mean "apply the function `(lambda (x) (+ 3 x))` to the argument `2`, or equivalently, "give the value `2` as an argument to the function `(lambda (x) (+ 3 x))`. + + In OCaml: + + (fun x -> ( + ) 3 x) 2 + + +5. Binding variables to values with "let" + + Let's go back and re-consider this Scheme expression: + + (let* ((three 3)) + (let* ((two 2)) + (+ three two))) + + Scheme also has a simple `let` (without the ` *`), and it permits you to group several variable bindings together in a single `let`- or `let*`-statement, like this: + + (let* ((three 3) (two 2)) + (+ three two)) + + Often you'll get the same results whether you use `let*` or `let`. However, there are cases where it makes a difference, and in those cases, `let*` behaves more like you'd expect. So you should just get into the habit of consistently using that. It's also good discipline for this seminar, especially while you're learning, to write things out the longer way, like this: + + (let* ((three 3)) + (let* ((two 2)) + (+ three two))) + + However, here you've got the double parentheses in `(let* ((three 3)) ...)`. They're doubled because the syntax permits more assignments than just the assignment of the value `3` to the variable `three`. Myself I tend to use `[` and `]` for the outer of these parentheses: `(let* [(three 3)] ...)`. Scheme can be configured to parse `[...]` as if they're just more `(...)`. + + It was asked in seminar if the `3` could be replaced by a more complex expression. The answer is "yes". You could also write: + + (let* [(three (+ 1 2))] + (let* [(two 2)] + (+ three two))) + + It was also asked whether the `(+ 1 2)` computation would be performed before or after it was bound to the variable `three`. That's a terrific question. Let's say this: both strategies could be reasonable designs for a language. We are going to discuss this carefully in coming weeks. In fact Scheme and OCaml make the same design choice. But you should think of the underlying form of the `let`-statement as not settling this by itself. + + Repeating our starting point for reference: + + (let* [(three 3)] + (let* [(two 2)] + (+ three two))) + + Recall in OCaml this same computation was written: + + let three = 3 in + let two = 2 in + ( + ) three two + +6. Binding with "let" is the same as supplying an argument to a lambda + + The preceding expression in Scheme is exactly equivalent to: + + (((lambda (three) (lambda (two) (+ three two))) 3) 2) + + The preceding expression in OCaml is exactly equivalent to: + + (fun three -> (fun two -> ( + ) three two)) 3 2 + + Read this several times until you understand it. + +7. Functions can also be bound to variables (and hence, cease being "anonymous"). + + In Scheme: + + (let* [(bar (lambda (x) B))] M) + + then wherever `bar` occurs in `M` (and isn't rebound by a more local `let` or `lambda`), it will be interpreted as the function `(lambda (x) B)`. + + Similarly, in OCaml: + + let bar = fun x -> B in + M + + This in Scheme: + + (let* [(bar (lambda (x) B))] (bar A)) + + as we've said, means the same as: + + ((lambda (bar) (bar A)) (lambda (x) B)) + + which beta-reduces to: + + ((lambda (x) B) A) + + and that means the same as: + + (let* [(x A)] B) + + in other words: evaluate `B` with `x` assigned to the value `A`. + + Similarly, this in OCaml: + + let bar = fun x -> B in + bar A + + is equivalent to: + + (fun x -> B) A + + and that means the same as: + + let x = A in + B + +8. Pushing a "let"-binding from now until the end + + What if you want to do something like this, in Scheme? + + (let* [(x A)] ... for the rest of the file or interactive session ...) + + or this, in OCaml: + + let x = A in + ... for the rest of the file or interactive session ... + + Scheme and OCaml have syntactic shorthands for doing this. In Scheme it's written like this: + + (define x A) + ... rest of the file or interactive session ... + + In OCaml it's written like this: + + let x = A;; + ... rest of the file or interactive session ... + + It's easy to be lulled into thinking this is a kind of imperative construction. *But it's not!* It's really just a shorthand for the compound `let`-expressions we've already been looking at, taking the maximum syntactically permissible scope. (Compare the "dot" convention in the lambda calculus, discussed above. I'm fudging a bit here, since in Scheme `(define ...)` is really shorthand for a `letrec` epression, which we'll come to in later classes.) + +9. Some shorthand + + OCaml permits you to abbreviate: + + let bar = fun x -> B in + M + + as: + + let bar x = B in + M + + It also permits you to abbreviate: + + let bar = fun x -> B;; + + as: + + let bar x = B;; + + Similarly, Scheme permits you to abbreviate: + + (define bar (lambda (x) B)) + + as: + + (define (bar x) B) + + and this is the form you'll most often see Scheme definitions written in. + + However, conceptually you should think backwards through the abbreviations and equivalences we've just presented. + + (define (bar x) B) + + just means: + + (define bar (lambda (x) B)) + + which just means: + + (let* [(bar (lambda (x) B))] ... rest of the file or interactive session ...) + + which just means: + + (lambda (bar) ... rest of the file or interactive session ...) (lambda (x) B) + + or in other words, interpret the rest of the file or interactive session with `bar` assigned the function `(lambda (x) B)`. + + +10. Shadowing + + You can override a binding with a more inner binding to the same variable. For instance the following expression in OCaml: + + let x = 3 in + let x = 2 in + x + + will evaluate to 2, not to 3. It's easy to be lulled into thinking this is the same as what happens when we say in C: + + int x = 3; + x = 2; + + but it's not the same! In the latter case we have mutation, in the former case we don't. You will learn to recognize the difference as we proceed. + + The OCaml expression just means: + + (fun x -> ((fun x -> x) 2) 3) + + and there's no more mutation going on there than there is in: + + 
∀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 = + # makegray { red = 0; green = 127; blue = 255 };; + - : color = {red = 0; green = 0; blue = 0} + +* Records just give your types a pretty interface; they're entirely dispensable. Instead of: + + type color = { red : int; green : int; blue : int };; + let c = { red = 0; green = 127; blue = 255 };; + let r = c.red;; + + You could instead just use a more familiar data constructor: + + type color = Color of (int * int * int);; + let c = Color (0, 127, 255);; + + and then extract the field you want using pattern-matching: + + let Color (r, _, _) = c;; + (* or *) + match c with Color (r, _, _) -> ... + + (Or you could just use bare tuples, without the `Color` data constructor.) + + The record syntax only exists because programmers sometimes find it more convenient to say: + + ... c.red ... + + than to reach for those pattern-matching constructions. + + + +##Functions## + +* In Haskell functions are assumed to be recursive, and their types and applications to values matching different patterns are each declared on different lines. So we have: + + factorial :: int -> int + factorial 0 = 1 + factorial n = n * factorial (n-1) + + In OCaml you must explicitly say when a function is recursive; and this would be written instead as: + + let rec factorial (n : int) : int = + match n with + | 0 -> 1 + | x -> x * factorial (x-1) + + or: + + let rec factorial : int -> int = + fun n -> match n with + | 0 -> 1 + | x -> x * factorial (x-1) + + or (though we recommend not using this last form): + + let rec factorial : int -> int = + function + | 0 -> 1 + | x -> x * factorial (x-1) + +* Another example, in Haskell: + + length :: [a] -> Integer + length [] = 0 + length (x:xs) = 1 + length xs + + In OCaml: + + let rec length : 'a list -> int = + fun lst -> match lst with + | [] -> 0 + | x::xs -> 1 + length xs + +* Another example, in Haskell: + + sign x | x > 0 = 1 + | x == 0 = 0 + | otherwise = -1 + + In OCaml: + + let sign x = match x with + | x' when x' > 0 -> 1 + | x' when x' = 0 -> 0 + | _ -> -1 + +* In Haskell the equality comparison operator is `==`, and the non-equality operator is `/=`. In OCaml, `==` expresses "physical identity", which has no analogue in Haskell because Haskell has no mutable types. See our discussion of "Four grades of mutation involvement" in the [[Week9]] notes. In OCaml the operator corresponding to Haskell's `==` is just `=`, and the corresponding non-equality operator is `<>`. + +* In both Haskell and OCaml, one can use many infix operators as prefix functions by parenthesizing them. So for instance: + + (+) 1 2 + + will work in both languages. One notable exception is that in OCaml you can't do this with the list constructor `::`: + + # (::) 1 [1;2];; + Error: Syntax error + # (fun x xs -> x :: xs) 1 [1; 2];; + - : int list = [1; 1; 2] + +* Haskell also permits two further shortcuts here that OCaml has no analogue for. In Haskell, in addition to writing: + + (>) 2 1 + + you can also write either of: + + (2 >) 1 + (> 1) 2 + + In OCaml one has to write these out longhand: + + (fun y -> 2 > y) 1;; + (fun x -> x > 1) 2;; + + Also, in Haskell, there's a special syntax for using what are ordinarily prefix functions as infix operators: + + Prelude> elem 1 [1, 2] + True + Prelude> 1 `elem` [1, 2] + True + + In OCaml one can't do that. There's only: + + # List.mem 1 [1; 2];; + - : bool = true + +* In Haskell one writes anonymous functions like this: + + \x -> x + 1 + + In OCaml it's: + + fun x -> x + 1 + +* Haskell uses the period `.` as a composition operator: + + g . f + -- same as + \x -> g (f x) + + In OCaml one has to write it out longhand: + + fun x -> g (f x) + +* In Haskell, expressions like this: + + g $ f x y + + are equivalent to: + + g (f x y) + + (Think of the period in our notation for the untyped lambda calculus.) + +* The names of standard functions, and the order in which they take their arguments, may differ. In Haskell: + + Prelude> :t foldr + foldr :: (a -> b -> b) -> b -> [a] -> b + + In OCaml: + + # List.fold_right;; + - : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b = + +* Some functions are predefined in Haskell but not in OCaml. Here are OCaml definitions for some common ones: + + let id x = x;; + let const x _ = x;; + let flip f x y = f y x;; + let curry (f : ('a, 'b) -> 'c) = fun x y -> f (x, y);; + let uncurry (f : 'a -> 'b -> 'c) = fun (x, y) -> f x y;; + let null lst = lst = [];; + + `fst` and `snd` (defined only on pairs) are provided in both languages. Haskell has `head` and `tail` for lists; these will raise an exception if applied to `[]`. In OCaml the corresponding functions are `List.hd` and `List.tl`. Many other Haskell list functions like `length` are available in OCaml as `List.length`, but OCaml's standard libraries are leaner that Haskell's. + +* The `until` function in Haskell is used like this: + + until (\l -> length l == 4) (1 : ) [] + -- evaluates to [1,1,1,1] + + until (\x -> x == 10) succ 0 + -- evaluates to 10 + + This can be defined in OCaml as: + + let rec until test f z = + if test z then z else until test f (f z) + + +##Lazy or Eager## + +* As we've mentioned several times, Haskell's evaluation is by default *lazy* or "call-by-need" (that's an efficient version of "call-by-name" that avoids computing the same results again and again). In some places Haskell will force evaluation to be *eager* or "strict". This is done in several different ways; the symbols `!` and `seq` are signs that it's being used. + +* Like Scheme and most other languages, OCaml is by default eager. Laziness can be achieved either by using thunks: + + # let eval_later1 () = 2 / 2;; + val eval_later1 : unit -> int = + # let eval_later2 () = 2 / 0;; + val eval_later2 : unit -> int = + # eval_later1 ();; + - : int = 1 + # eval_later2 ();; + Exception: Division_by_zero. + + or by using the special forms `lazy` and `Lazy.force`: + + # let eval_later3 = lazy (2 / 2);; + val eval_later3 : int lazy_t = + # Lazy.force eval_later3;; + - : int = 1 + # eval_later3;; + - : int lazy_t = lazy 1 + + Notice in the last line the value is reported as being `lazy 1` instead of ``. Since the value has once been forced, it won't ever need to be recomputed. The thunks are less efficient in this respect. Even though OCaml will now remember what `eval_later3` should be forced to, `eval_later3` is still type-distinct from a plain `int`. + + +##Monads## + +Haskell has more built-in support for monads, but one can define the monads one needs in OCaml. + +* In our seminar, we've been calling one monadic operation `unit`; in Haskell the same operation is called `return`. We've been calling another monadic operation `bind`, used in prefix form, like this: + + bind u f + + In Haskell, one uses the infix operator `>>=` to express bind instead: + + u >>= f + + If you like this Haskell convention, you can define `>>=` in OCaml like this: + + let (>>=) = bind;; + +* Haskell also uses the operator `>>`, where `u >> v` means the same as `u >>= \_ -> v`. + +* In Haskell, one can generally just use plain `return` and `>>=` and the interpreter will infer what monad you must be talking about from the surrounding type constraints. In OCaml, you generally need to be specific about which monad you're using. So in these notes, when mutiple monads are on the table, we've defined operations as `reader_unit` and `reader_bind`, and so on. + +* Haskell has a special syntax for working conveniently with monads. It looks like this. Assume `u` `v` and `w` are values of some monadic type `M a`. Then `x` `y` and `z` will be variables of type `a`: + + do + x <- u + y <- v + w + let z = foo x y + return z + + This is equivalent in meaning to the following: + + u >>= \ x -> + v >>= \ y -> + w >>= \ _ -> + let z = foo x y + in return z + + which can be translated straightforwardly into OCaml. + + For more details, see: + + * [Haskell wikibook on do-notation](http://en.wikibooks.org/wiki/Haskell/do_Notation) + * [Yet Another Haskell Tutorial on do-notation](http://en.wikibooks.org/wiki/Haskell/YAHT/Monads#Do_Notation) + * [Do-notation considered harmful](http://www.haskell.org/haskellwiki/Do_notation_considered_harmful) + +* If you like the Haskell do-notation, there's [a library](http://www.cas.mcmaster.ca/~carette/pa_monad/) you can compile and install to let you use something similar in OCaml. + +* In order to do any printing, Haskell has to use a special `IO` monad. So programs will look like this: + + main :: IO () + main = do + let s = "hello world" + putStrLn s + + main :: IO String + main = do + let s = "hello world" + putStrLn s + return s + + main :: IO String + main = let s = "hello world" + in putStrLn s >> return s + + OCaml permits you to mix side-effects with regular code, so you can just print, without needing to bring in any monad: + + let main = + let s = "hello world" + in let () = print_endline s + in s;; + + or: + + let main = + let s = "hello world" + in print_endline s ; s;; + diff --git a/_what_is_functional.mdwn b/_what_is_functional.mdwn new file mode 100644 index 00000000..d6b9354e --- /dev/null +++ b/_what_is_functional.mdwn @@ -0,0 +1,271 @@ +*This page is not ready to go live; just roughly copying over some material from last year.* + + +Declarative/functional vs Imperatival/dynamic models of computation +=================================================================== + +Many of you, like us, will have grown up thinking the paradigm of computation is a sequence of changes. Let go of that. It will take some care to separate the operative notion of "sequencing" here from other notions close to it, but once that's done, you'll see that languages that have no significant notions of sequencing or changes are Turing complete: they can perform any computation we know how to describe. In itself, that only puts them on equal footing with more mainstream, imperatival programming languages like C and Java and Python, which are also Turing complete. But further, the languages we want you to become familiar with can reasonably be understood to be more fundamental. They embody the elemental building blocks that computer scientists use when reasoning about and designing other languages. + +Jim offered the metaphor: think of imperatival languages, which include "mutation" and "side-effects" (we'll flesh out these keywords as we proceeed), as the pâté of computation. We want to teach you about the meat and potatoes, where as it turns out there is no sequencing and no changes. There's just the evaluation or simplification of complex expressions. + +Now, when you ask the Scheme interpreter to simplify an expression for you, that's a kind of dynamic interaction between you and the interpreter. You may wonder then why these languages should not also be understood imperatively. The difference is that in a purely declarative or functional language, there are no dynamic effects in the language itself. It's just a static semantic fact about the language that one expression reduces to another. You may have verified that fact through your dynamic interactions with the Scheme interpreter, but that's different from saying that there are dynamic effects in the language itself. + +What the latter would amount to will become clearer as we build our way up to languages which are genuinely imperatival or dynamic. + +Many of the slogans and keywords we'll encounter in discussions of these issues call for careful interpretation. They mean various different things. + +For example, you'll encounter the claim that declarative languages are distinguished by their **referential transparency.** What's meant by this is not always exactly the same, and as a cluster, it's related to but not the same as this means for philosophers and linguists. + +The notion of **function** that we'll be working with will be one that, by default, sometimes counts as non-identical functions that map all their inputs to the very same outputs. For example, two functions from jumbled decks of cards to sorted decks of cards may use different algorithms and hence be different functions. + +It's possible to enhance the lambda calculus so that functions do get identified when they map all the same inputs to the same outputs. This is called making the calculus **extensional**. Church called languages which didn't do this **intensional**. If you try to understand that kind of "intensionality" in terms of functions from worlds to extensions (an idea also associated with Church), you may hurt yourself. So too if you try to understand it in terms of mental stereotypes, another notion sometimes designated by "intension." + +It's often said that dynamic systems are distinguished because they are the ones in which **order matters**. However, there are many ways in which order can matter. If we have a trivalent boolean system, for example---easily had in a purely functional calculus---we might choose to give a truth-table like this for "and": + + true and true = true + true and * = * + true and false = false + * and true = * + * and * = * + * and false = * + false and true = false + false and * = false + false and false = false + +And then we'd notice that `* and false` has a different intepretation than `false and *`. (The same phenomenon is already present with the material conditional in bivalent logics; but seeing that a non-symmetric semantics for `and` is available even for functional languages is instructive.) + +Another way in which order can matter that's present even in functional languages is that the interpretation of some complex expressions can depend on the order in which sub-expressions are evaluated. Evaluated in one order, the computations might never terminate (and so semantically we interpret them as having "the bottom value"---we'll discuss this). Evaluated in another order, they might have a perfectly mundane value. Here's an example, though we'll reserve discussion of it until later: + + (\x. y) ((\x. x x) (\x. x x)) + +Again, these facts are all part of the metatheory of purely functional languages. But *there is* a different sense of "order matters" such that it's only in imperatival languages that order so matters. + + x := 2 + x := x + 1 + x == 3 + +Here the comparison in the last line will evaluate to true. + + x := x + 1 + x := 2 + x == 3 + +Here the comparison in the last line will evaluate to false. + +One of our goals for this course is to get you to understand *what is* that new +sense such that only so matters in imperatival languages. + +Finally, you'll see the term **dynamic** used in a variety of ways in the literature for this course: + +* dynamic versus static typing + +* dynamic versus lexical [[!wikipedia Scope (programming) desc="scoping"]] + +* dynamic versus static control operators + +* finally, we're used ourselves to talking about dynamic versus static semantics + +For the most part, these uses are only loosely connected to each other. We'll tend to use "imperatival" to describe the kinds of semantic properties made available in dynamic semantics, languages which have robust notions of sequencing changes, and so on. + +To read further about the relation between declarative or functional programming, on the one hand, and imperatival programming on the other, you can begin here: + +* [[!wikipedia Declarative programming]] +* [[!wikipedia Functional programming]] +* [[!wikipedia Purely functional]] +* [[!wikipedia Referential transparency (computer science)]] +* [[!wikipedia Imperative programming]] +* [[!wikipedia Side effect (computer science) desc="Side effects"]] + + +Map +=== + + + + + + + + + + + + +
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) +  +
+ + +Declarative/functional vs Imperatival/dynamic models of computation +=================================================================== + +Many of you, like us, will have grown up thinking the paradigm of computation is a sequence of changes. Let go of that. It will take some care to separate the operative notion of "sequencing" here from other notions close to it, but once that's done, you'll see that languages that have no significant notions of sequencing or changes are Turing complete: they can perform any computation we know how to describe. In itself, that only puts them on equal footing with more mainstream, imperatival programming languages like C and Java and Python, which are also Turing complete. But further, the languages we want you to become familiar with can reasonably be understood to be more fundamental. They embody the elemental building blocks that computer scientists use when reasoning about and designing other languages. + +Jim offered the metaphor: think of imperatival languages, which include "mutation" and "side-effects" (we'll flesh out these keywords as we proceeed), as the pâté of computation. We want to teach you about the meat and potatoes, where as it turns out there is no sequencing and no changes. There's just the evaluation or simplification of complex expressions. + +Now, when you ask the Scheme interpreter to simplify an expression for you, that's a kind of dynamic interaction between you and the interpreter. You may wonder then why these languages should not also be understood imperatively. The difference is that in a purely declarative or functional language, there are no dynamic effects in the language itself. It's just a static semantic fact about the language that one expression reduces to another. You may have verified that fact through your dynamic interactions with the Scheme interpreter, but that's different from saying that there are dynamic effects in the language itself. + +What the latter would amount to will become clearer as we build our way up to languages which are genuinely imperatival or dynamic. + +Many of the slogans and keywords we'll encounter in discussions of these issues call for careful interpretation. They mean various different things. + +For example, you'll encounter the claim that declarative languages are distinguished by their **referential transparency.** What's meant by this is not always exactly the same, and as a cluster, it's related to but not the same as this means for philosophers and linguists. + +The notion of **function** that we'll be working with will be one that, by default, sometimes counts as non-identical functions that map all their inputs to the very same outputs. For example, two functions from jumbled decks of cards to sorted decks of cards may use different algorithms and hence be different functions. + +It's possible to enhance the lambda calculus so that functions do get identified when they map all the same inputs to the same outputs. This is called making the calculus **extensional**. Church called languages which didn't do this **intensional**. If you try to understand that kind of "intensionality" in terms of functions from worlds to extensions (an idea also associated with Church), you may hurt yourself. So too if you try to understand it in terms of mental stereotypes, another notion sometimes designated by "intension." + +It's often said that dynamic systems are distinguished because they are the ones in which **order matters**. However, there are many ways in which order can matter. If we have a trivalent boolean system, for example---easily had in a purely functional calculus---we might choose to give a truth-table like this for "and": + + true and true = true + true and * = * + true and false = false + * and true = * + * and * = * + * and false = * + false and true = false + false and * = false + false and false = false + +And then we'd notice that `* and false` has a different intepretation than `false and *`. (The same phenomenon is already present with the material conditional in bivalent logics; but seeing that a non-symmetric semantics for `and` is available even for functional languages is instructive.) + +Another way in which order can matter that's present even in functional languages is that the interpretation of some complex expressions can depend on the order in which sub-expressions are evaluated. Evaluated in one order, the computations might never terminate (and so semantically we interpret them as having "the bottom value"---we'll discuss this). Evaluated in another order, they might have a perfectly mundane value. Here's an example, though we'll reserve discussion of it until later: + + (\x. y) ((\x. x x) (\x. x x)) + +Again, these facts are all part of the metatheory of purely functional languages. But *there is* a different sense of "order matters" such that it's only in imperatival languages that order so matters. + + x := 2 + x := x + 1 + x == 3 + +Here the comparison in the last line will evaluate to true. + + x := x + 1 + x := 2 + x == 3 + +Here the comparison in the last line will evaluate to false. + +One of our goals for this course is to get you to understand *what is* that new +sense such that only so matters in imperatival languages. + +Finally, you'll see the term **dynamic** used in a variety of ways in the literature for this course: + +* dynamic versus static typing + +* dynamic versus lexical [[!wikipedia Scope (programming) desc="scoping"]] + +* dynamic versus static control operators + +* finally, we're used ourselves to talking about dynamic versus static semantics + +For the most part, these uses are only loosely connected to each other. We'll tend to use "imperatival" to describe the kinds of semantic properties made available in dynamic semantics, languages which have robust notions of sequencing changes, and so on. + +To read further about the relation between declarative or functional programming, on the one hand, and imperatival programming on the other, you can begin here: + +* [[!wikipedia Declarative programming]] +* [[!wikipedia Functional programming]] +* [[!wikipedia Purely functional]] +* [[!wikipedia Referential transparency (computer science)]] +* [[!wikipedia Imperative programming]] +* [[!wikipedia Side effect (computer science) desc="Side effects"]] + + +Map +=== + + + + + + + + + + + + +
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) +  +
+ + + +What "sequencing" is and isn't +------------------------------ + +We mentioned before the idea that computation is a sequencing of some changes. I said we'd be discussing (fragments of, and in some cases, entire) languages that have no native notion of change. + +Neither do they have any useful notion of sequencing. But what this would be takes some care to identify. + +First off, the mere concatenation of expressions isn't what we mean by sequencing. Concatenation of expressions is how you build syntactically complex expressions out of simpler ones. The complex expressions often express a computation where a function is applied to one (or more) arguments, + +Second, the kind of rebinding we called "shadowing" doesn't involve any changes or sequencing. All the precedence facts about that kind of rebinding are just consequences of the compound syntactic structures in which it occurs. + +Third, the kinds of bindings we see in: + + (define foo A) + (foo 2) + +Or even: + + (define foo A) + (define foo B) + (foo 2) + +don't involve any changes or sequencing in the sense we're trying to identify. As we said, these programs are just syntactic variants of (single) compound syntactic structures involving `let`s and `lambda`s. + +Since Scheme and OCaml also do permit imperatival constructions, they do have syntax for genuine sequencing. In Scheme it looks like this: + + (begin A B C) + +In OCaml it looks like this: + + begin A; B; C end + +Or this: + + (A; B; C) + +In the presence of imperatival elements, sequencing order is very relevant. For example, these will behave differently: + + (begin (print "under") (print "water")) + + (begin (print "water") (print "under")) + +And so too these: + + begin x := 3; x := 2; x end + + begin x := 2; x := 3; x end + +However, if A and B are purely functional, non-imperatival expressions, then: + + begin A; B; C end + +just evaluates to C (so long as A and B evaluate to something at all). So: + + begin A; B; C end + +contributes no more to a larger context in which it's embedded than C does. This is the sense in which functional languages have no serious notion of sequencing. + +We'll discuss this more as the seminar proceeds. + + + + diff --git a/code/monad_library.mdwn b/code/monad_library.mdwn new file mode 100644 index 00000000..1761e61c --- /dev/null +++ b/code/monad_library.mdwn @@ -0,0 +1,167 @@ +We've written a full-featured [OCaml Monad Library](/code/monads.ml). To use it, download the file and then in your OCaml session or file, write: + + # #use "path/to/monads.ml";; + +That's not the official, preferred way to load OCaml libraries, but it's quick and easy. + +Some comments on the design of this library. + +* First off, the different monads are **encapsulated in modules**. So you won't say `list_bind` and so on. Instead, you'll say `List_monad.bind`. + +* It gets tedious to write things like: + + List_monad.bind (List_monad.unit 1) (fun a -> + List_monad.plus + (List_monad.unit a) + (List_monad.unit (succ a)));; + + So instead, we recommend the following shortcut: + + List_monad.(bind (unit 1) (fun a -> plus (unit a) (unit (succ a))));; + + This is equivalent: + + let open List_monad + in let f = fun a -> plus (unit a) (unit (succ a)) + in bind (unit 1) f;; + + If you know you're only going to be using `bind`s and `unit`s from a single monad, you can also do this: + + open List_monad;; (* now `bind` always refers to List_monad.bind, and so on *) + bind (unit 1) ... + (* later you want to use a different monad's operations, so ... *) + open Maybe_monad;; + ... + + But we recommend using one of the first two forms above, instead. It's easy to lose track of which monad you've loaded at the top level in this way; and if you want to combine operations from different monads in a single expression, you'll have to use the first form, anyway. + +* Some of the monads are parameterized. For instance, to use the Reader monad, you have to first specify what is the type of the `env` you propose to use. You'd do that like this: + + (* we want to implements env as a function from strings to ints *) + module R = Reader_monad(struct type env = string -> int end);; + (* now we can use R as a Reader monad module *) + (R.unit 1, R.unit false, R.unit "string");; + + Similarly, to use a State monad, you have to specify the type of the store: + + module S = State_monad(struct type store = int end);; + S.unit 1;; + S.get;; (* this monadic value would retrieve the current store *) + S.put 20;; (* would install 20 as the new store *) + S.puts succ;; (* would apply succ to the current store, whatever it is *) + let u = S.(unit 1 >>= fun a -> + put 20 >>= fun _ -> + puts succ >>= fun _ -> + get >>= fun b -> + unit [a;b]);; + + The monadic value `u` we've defined here binds a series of operations to an initial `unit 1`. The effect of these operations is to save the wrapped 1 in variable `a`, discard the current store and install 20 in its place, increment the current store, retrieve the current store and make that the wrapped value, and finally deliver a `unit [a;b]` where `b` is the current wrapped value and `a` is the 1 we saved earlier. + + This can be economized somewhat by using the shorthand: + + u >> v + + instead of: + + u >>= fun _ -> v. + + So we'd have: + + let u = S.(unit 1 >>= fun a -> + put 20 >> + puts succ >> + get >>= fun b -> + unit [a;b]);; + + How can we supply an initial store and get this computation started? You do it like this: + + # let initial_store = 0 + in S.run u initial_store;; + - : S.store list * S.store = ([1; 21], 21) + + Our wrapped value at the end is `[1; 21]`, and the current store is `21`. Compare also: + + # S.(run(let u = puts succ >> get in + u >>= fun a1 -> + u >>= fun a2 -> + u >>= fun a3 -> + unit [a1;a2;a3])) 0;; + - : S.store list * S.store = ([1; 2; 3], 3) + # S.(run(let u = puts succ >> get in sequence [u;u;u])) 0;; + - : S.store list * S.store = ([1; 2; 3], 3) + + +* The monads available are: + + * `Identity_monad` + * `Maybe_monad` + * `List_monad` + * `Reader_monad` (has to be parameterized as above) + * `State_monad` (has to be parameterized as above) + * `Ref_monad` (a version of `State_monad` with a structured store, and custom operations for creating new cells in the store, and getting or changing the values of existing cells) + * `Writer_monad` (has to be parameterized on the type of the written data; use `Writer1` as a simple predefined case) + * `Error_monad`, with `throw err` and `catch u handler_function` operations (this has to be parameterized on the type of `err`; use `Failure` as a simple predefined case, where `type err = string`) + * `IO_monad` (you don't need this in OCaml, but it works analagously to the `IO` monad in Haskell, so it's handy for working with Haskell-written algorithms in OCaml) + * `Tree_monad` (leaf-labeled, binary trees) + * and of course, `Continuation_monad`, with `callcc`, `reset`, `shift` and `abort` operations. + +* All of these monads come with [[monad transformers]] too. To get a State monad wrapped around a Maybe monad, do this: + + module S = State_monad(struct type store = int end);; + module SM = S.T(Maybe_monad);; + + To get a Maybe monad wrapped around a State monad, do this instead: + + module MS = Maybe_monad.T(S);; + + Note that those two layered monads will have slightly different behavior. See our discussion of [[monad transformers]] for details. Also, the outermost monad is the one whose operations are most exposed. If you want to use any of the State-specific operations (like `puts succ`) in the `MS` monad, you'll have to "elevate" those operations into the MaybeT interface. The way you do that is like this: + + MS.(... >> elevate (S.puts succ) >> ...) + + The Haskell libraries use `lift` instead of `elevate`. (They use `liftM` and `liftM2` for what we've called `lift` and `lift2`. They also call `liftM` `fmap`.) This name `lift` is already over-loaded enough, so we chose to use `elevate` here. In our usage, `lift` (and `lift2`) bring non-monadic operations into a monad; `elevate` brings monadic operations from a wrapped monad out into the wrapping monad. + +* If you look at the types of the monadic values: + + # let u = S.(unit 1);; + val u : ('_a, int) S.m = + + You'll notice that the monadic type `S.m` is parameterized on *two* type arguments: one of them, `int`, is the type of the wrapped value. What is the other one (`'_a` in the above example)? + + The answer is that for most of the monads this second type argument is an idle wheel. The Continuation monad needs both of the type arguments, though, since its monadic type is implemented as: + + type ('r,'b) m = ('b -> 'r) -> 'r + + and there both `'r` and `'b` need to be free type variables. Since we want to allow you to layer Continuation monads with the others, it vastly simplified the library to make all of the monadic types take two type parameters, even though the second will only be used by a Continuation monad you may have stacked in the monadic bundle you're using. You can pretty much ignore this; think of the `S.(unit 1)` as though it just had the type `int S.m`. + + +* The implementation of most monadic types is **hidden**. Above, when we wanted to supply an `initial_store` to a value `u` of type `('a,'b) S.m`, we did this: + + # let u = S.(unit 10 >>= fun a -> puts succ >> unit a);; + # S.run u 0;; + - : int * S.store = (10, 1) + + This will not work: + + # u 0;; + Error: This expression is not a function; it cannot be applied + + Although the library knows that an `('a,'b) S.m` type is implemented as `store -> ('b * store)`, it doesn't expose that fact to the outside world. To get at the implementation, you have to use the `run` operation. That translates the opaque `('a,'b) S.m` type into `store -> ('b * store)` type that you can use as a function. + + So the `run` operation lets you get from the hidden type to its actual implementation. What about the other way around? By design, there is no way to do this. You can't just hand the libary an arbitrary `store -> ('b * store)` and say it's an `('a,'b) S.m`. Instead, you should use the primitive operations in your `S` module---`unit`, `bind`, `get`, `puts` and so on---to build up the `('a,'b) S.m` you want. + +* The same design is used in the `Ref_monad`. Keys into the store are implemented as `int`s, but their type is kept hidden (the computing community says "abstract"), so that the outside world can't do anything with the keys but +compare them for equality and use them for derefs, and so on. + + +Acknowledgements: Our library is largely based on the mtl library distributed with the Glasgow Haskell Compiler. That in turn was inspired by Mark Jones' 1995 paper +[Functional Programming with Overloading and Higher-Order Polymorphism](http://web.cecs.pdx.edu/~mpj/pubs/springschool.html). + I've also been helped in + various ways by posts and direct feedback from Oleg Kiselyov and + Chung-chieh Shan. The following were also useful: + + * + * Ken Shan "Monads for natural language semantics" + * + * + + diff --git a/exercises/_assignment2.mdwn b/exercises/_assignment2.mdwn new file mode 100644 index 00000000..fa02cb83 --- /dev/null +++ b/exercises/_assignment2.mdwn @@ -0,0 +1,152 @@ +Reduction +--------- + +Find "normal forms" for the following---that is, reduce them until no more reductions are possible. We'll write λ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))) + +
    +
  1. Define a `neg` operator that negates `true` and `false`. + +Expected behavior: + + (((neg true) 10) 20) + +evaluates to 20, and + + (((neg false) 10) 20) + +evaluates to 10. + +
  2. Define an `and` operator. + +
  3. Define an `xor` operator. If you haven't seen this term before, here's a truth table: + + true xor true = false + true xor false = true + false xor true = true + false xor false = false + + +
  4. Inspired by our definition of boolean values, propose a data structure +capable of representing one of the two values `black` or `white`. +If we have +one of those values, call it a "black-or-white value", we should be able to +write: + + the-value if-black if-white + +(where `if-black` and `if-white` are anything), and get back one of `if-black` or +`if-white`, depending on which of the black-or-white values we started with. Give +a definition for each of `black` and `white`. (Do it in both lambda calculus +and also in Racket.) + +
  5. Now propose a data structure capable of representing one of the three values +`red` `green` or `blue`, based on the same model. (Do it in both lambda +calculus and also in Racket.) +
+ + + +Pairs +----- + +Recall our definitions of ordered pairs. + +> the pair **(**x**,**y**)** is defined to be `\f. f x y` + +To extract the first element of a pair p, you write: + + p (\fst \snd. fst) + +Here are some definitions in Racket: + + (define make-pair (lambda (fst) (lambda (snd) (lambda (f) ((f fst) snd))))) + (define get-first (lambda (fst) (lambda (snd) fst))) + (define get-second (lambda (fst) (lambda (snd) snd))) + +Now we can write: + + (define p ((make-pair 10) 20)) + (p get-first) ; will evaluate to 10 + (p get-second) ; will evaluate to 20 + +If you're puzzled by having the pair to the left and the function that +operates on it come second, think about why it's being done this way: the pair +is a package that takes a function for operating on its elements *as an +argument*, and returns *the result of* operating on its elements with that +function. In other words, the pair is a higher-order function. (Consider the similarities between this definition of a pair and a generalized quantifier.) + +If you like, you can disguise what's going on like this: + + (define lifted-get-first (lambda (p) (p get-first))) + (define lifted-get-second (lambda (p) (p get-second))) + +Now you can write: + + (lifted-get-first p) + +instead of: + + (p get-first) + +However, the latter is still what's going on under the hood. (Remark: `(lifted-f ((make-pair 10) 20))` stands to `(((make-pair 10) 20) f)` as `(((make-pair 10) 20) f)` stands to `((f 10) 20)`.) + + +
    +
  1. Define a `swap` function that reverses the elements of a pair. Expected behavior: + + (define p ((make-pair 10) 20)) + ((p swap) get-first) ; evaluates to 20 + ((p swap) get-second) ; evaluates to 10 + +Write out the definition of `swap` in Racket. + + +
  2. Define a `dup` function that duplicates its argument to form a pair +whose elements are the same. +Expected behavior: + + ((dup 10) get-first) ; evaluates to 10 + ((dup 10) get-second) ; evaluates to 10 + +
  3. Define a `sixteen` function that makes +sixteen copies of its argument (and stores them in a data structure of +your choice). + +
  4. Inspired by our definition of ordered pairs, propose a data structure capable of representing ordered triples. That is, + + (((make-triple M) N) P) + +should return an object that behaves in a reasonable way to serve as a triple. In addition to defining the `make-triple` function, you have to show how to extract elements of your triple. Write a `get-first-of-triple` function, that does for triples what `get-first` does for pairs. Also write `get-second-of-triple` and `get-third-of-triple` functions. + +
  5. Write a function `second-plus-third` that when given to your triple, returns the result of adding the second and third members of the triple. + +You can help yourself to the following definition: + + (define add (lambda (x) (lambda (y) (+ x y)))) + + + +
+ diff --git a/index.mdwn b/index.mdwn index 9a696339..c581a3ee 100644 --- a/index.mdwn +++ b/index.mdwn @@ -10,6 +10,8 @@ the Linguistics building at 10 Washington Place, in room 103 (front of the first One student session will be held every Wednesday from XX-YY at WHERE. --> +## [[Jump to content (lecture notes and more)|topics_and_themes.mdwn]] ## + ## Announcements ## @@ -36,9 +38,12 @@ we'll be doing the next week. It would be smart to make a serious start on that week's homework, for instance, before the session. --> -* Here is information about [[How to get the programming languages running on your computer]]. +* Here is information about [[How to get the programming languages running on your computer|installing]]. -* Here are [[Lecture notes for Week 1|topics/week1]]; and [[the homework|exercises/assignment1]]. There are also some [[advanced notes|topics/week1 advanced notes]]. +* Here are lecture notes for week 1: [[order|topics/week1 order]]; +[[the introduction to functional programming|topics/week1]], along +with [[the homework|exercises/assignment1]] and some [[advanced +notes|topics/week1 advanced notes]]. > Topics: Basics of Functional Programming @@ -118,7 +123,7 @@ course is to enable you to make these tools your own; to have enough understanding of them to recognize them in use, use them yourself at least in simple ways, and to be able to read more about them when appropriate. -[[More about the topics and larger themes of the course|topics and themes]] +[[More about the topics and larger themes of the course| topics and themes]] ## Who Can Participate? ## diff --git a/how_to_get_the_programming_languages_running_on_your_computer.mdwn b/installing.mdwn similarity index 100% rename from how_to_get_the_programming_languages_running_on_your_computer.mdwn rename to installing.mdwn diff --git a/readings/coreference-and-modality.pdf b/readings/coreference-and-modality.pdf new file mode 100644 index 00000000..8dc69f53 Binary files /dev/null and b/readings/coreference-and-modality.pdf differ diff --git a/readings/wadler-monads.pdf b/readings/wadler-monads.pdf new file mode 100644 index 00000000..ad23fcd4 Binary files /dev/null and b/readings/wadler-monads.pdf differ diff --git a/topics/_week2.mdwn b/topics/_week2.mdwn new file mode 100644 index 00000000..c614319b --- /dev/null +++ b/topics/_week2.mdwn @@ -0,0 +1,250 @@ +*This page is not ready to go live; just roughly copying over some material from last year.* + + +Here's what we did in seminar on Monday 9/13, + +Sometimes these notes will expand on things mentioned only briefly in class, or discuss useful tangents that didn't even make it into class. This present page expands on *a lot*, and some of this material will be reviewed next week. + +[Linguistic and Philosophical Applications of the Tools We'll be Studying](/applications) +========================================================================== + +[Explanation of the "Damn" example shown in class](/damn) + +Basics of Lambda Calculus +========================= + +The lambda calculus we'll be focusing on for the first part of the course has no types. (Some prefer to say it instead has a single type---but if you say that, you have to say that functions from this type to this type also belong to this type. Which is weird... In fact, though, such types are studied, under the name "recursive type." More about these later in the seminar.) + +Here is its syntax: + +
+Variables: x, y, z... +
+ +Each variable is an expression. For any expressions M and N and variable a, the following are also expressions: + +
+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 . + diff --git a/topics/week1.mdwn b/topics/week1.mdwn index f195b8d9..82e1fa63 100644 --- a/topics/week1.mdwn +++ b/topics/week1.mdwn @@ -610,7 +610,35 @@ The `x` in `F x` and in `H x` are governed by the outermost quantifier, and only 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. + diff --git a/topics/week1_advanced_notes.mdwn b/topics/week1_advanced_notes.mdwn index d843ee72..9bac7eb6 100644 --- a/topics/week1_advanced_notes.mdwn +++ b/topics/week1_advanced_notes.mdwn @@ -51,7 +51,7 @@ I agree it's annoying that these conventions are so diverse. There are plenty ot A function value doesn't have any structure---at least none that's visible to the pattern-matching system. You can only match against simple patterns like `_` or the variable `f`. -When matching a variable against a λ-generated function value in a `let`- or `letrec`-construction, there's an alternative syntax that you may find more convenient. This: +When matching a λ-generated function value against a variable in a `let`- or `letrec`-construction, there's an alternative syntax that you may find more convenient. This: `let`   `f match` λ`x.` φ`;` @@ -99,9 +99,9 @@ If we get to the `y & ys` line in the pattern list, and the pattern-match succee ### As-patterns ### -Sometimes it's useful to bind variables against overlapping parts of a structure. For instance, suppose I'm writing a pattern that is to be matched against multivalues like `([10, 20], 'true)`. And suppose I want to end up with `ys` bound to `[10, 20]`, `x` bound to `10`, and `xs` bound to `[20]`. Using the techniques introduced so far, I have two options. First, I could bind `ys` against `[10, 20]`, and then initiate a second pattern-match to break that up into `10` and [20]`. Like this: +Sometimes it's useful to bind variables against overlapping parts of a structure. For instance, suppose I'm writing a pattern that is to be matched against multivalues like `([10, 20], 'true)`. And suppose I want to end up with `ys` bound to `[10, 20]`, `x` bound to `10`, and `xs` bound to `[20]`. Using the techniques introduced so far, I have two options. First, I could bind `ys` against `[10, 20]`, and then initiate a second pattern-match to break that up into `10` and `[20]`. Like this: - case [10, 20] of + case ([10, 20], 'true) of [ys, _] then case ys of x & xs then ...; ... @@ -111,7 +111,7 @@ Sometimes it's useful to bind variables against overlapping parts of a structure Alternatively, I could directly bind `x` against `10` and `xs` against `[20]`. But then I would have to re-cons them together again to get `ys`. Like this: - case [10, 20] of + case ([10, 20], 'true) of [x & xs, _] then let ys match x & xs in ...; @@ -120,7 +120,7 @@ Alternatively, I could directly bind `x` against `10` and `xs` against `[20]`. B Both of these strategies work. But they are a bit inefficient. I said you didn't really need to worry about efficiency in this seminar. But these are also a bit cumbersome to write. There's a special syntax that enables us to bind all three of `ys`, `x`, and `xs` in the desired way, despite the fact that they will be matching against overlapping, rather than discrete, parts of the value `[10, 20]`. The special syntax looks like this: - case [10, 20] of + case ([10, 20], 'true) of [(x & xs) as ys, _] then ... ... end @@ -165,12 +165,14 @@ Function composition, which mathematicians write as `f` ○ `g`, is defined as We've already come across the `id` function, namely λ `x. x`. -Other common functions are `fst`, which takes two arguments and returns the first of them; `snd`, which takes two arguments and returns the second of them; and `swap`, which takes two arguments and returns them both but with their positions swapped. These functions can be defined like this: +Other common functions are `fst`, which takes two arguments and returns the first of them; `snd`, which takes two arguments and returns the second of them; and `swap`, which takes two arguments and returns them both but with their positions swapped. A fourth function is `dup`, which takes one argument and returns it twice. +These functions can be defined like this: let fst (x, y) = x; snd (x, y) = y; - swap (x, y) = (y, x) - in (fst, snd, swap) + swap (x, y) = (y, x); + dup x = (x, x) + in (fst, snd, swap, dup)