------ Forwarded message from Jim Pryor <jim@jimpryor.net> -----
-
-Some notes on notation
-
-Probably we won't want to explicitly give this to them until week 2 (or
-later), but I jotted it down now so that we might agree about it and
-stick to it.
-
-
-These languages have VALUES of various TYPES. For instance, the number 2
-is a value of the type integer. The string "horse" is a value of the
-type string. Functions are also values. Their type depends on the values
-of their domain and range. For instance, the successor function is a
-value of the type integer -> integer. The plus function is a value of
-the type <two integers> -> integer. I'm fudging a bit here with the <two
-integers>; we'll come back to this and talk about the fudge soon.
-
-We can talk equally of expressions having types: they have the types of the values they express.
-
-(Sometimes the "untyped" lambda calculus is said to be "singly-typed". It may nor may not be helpful to think of it that way. If its expressions do have a type, though, it's a type T such that functions from T -> T are also of type T. Myself I find it easier to think "untyped.")
-
-
-In some of the languages, one refers to (and sometimes quantifies over) the types in the object language itself; so the object language itself has syntax for talking about types. We'll be discussing this later in the course. For now I'm just saying what notation will eventually be so used.
-
-You need to keep straight about the difference between Constants of a
-given sort, Object-language Variables of the same sort, and Metalinguistic Schemas of that sort. I say "sort" here because you have this same three-way divide with BOTH expressions that express values and expressions that express types.
-
-Sticking just to values, here are some examples of constants: 2, 3, +,
-*, "horse", and so on.
-
-Here are some examples of object-language
-variables: x, y10, first, second_place, and so on (you needn't stick to a
-single letter). x', x'', and so on are also typically used as variables.
-All the languages we'll be looking at will permit this syntax.
-
-Conventions for metalinguistic schemas vary. In logic textbooks, one
-often sees lower-case Greek letters used in this way. But in the fields
-we'll be looking at, those are often used specifically as schematic
-letters for TYPES. For schematic letters for VALUES, we'll go with the
-convention that uses Capital Letters. For example:
- E is some expression of the lambda calculus. E may be "x" or "lambda
-x: x" or "(lambda x: x y) (lambda z: w)" or whatever.
- (M N) is another expression of the lambda calculus, where some
-possibly complex expression M is applied to another possibly complex
-expression N.
- and so on.
-
-
-More systematically:
-
- value variables in OCaml: start with lower case letter, can be
-followed by any letter or number or _ or '
- value variables in lambda calculus: no fixed rules, but we'll
-use the OCaml conventions, which is what you commonly see in practice.
- value variables in Scheme: all the OCaml variables are permitted.
-Some Schemes are case-sensitive, others aren't, others let you flip a
-switch to decide. To avoid worrying about it, never use "firstPlace" as a
-variable if you also use "firstplace" as a variable. Scheme also permits
-very funky variable names, like "*add*" and "are-there-three-yet?" and
-so on.
-
- Remember, value variables can be bound to values of various types,
-including functions.
-
- value constants in lambda calculus: some lambda calculi have
-primitive values in them, such as the number 0. But the mainstream ones
-don't have any primitive values of any sort. All you've got are
-variables, lambda abstractions of other stuff you've got, and
-applications of other stuff you've got. If you want numbers or boolean
-constants, you've got to "encode" them or build them yourself out of the
-materials just described. We'll be looking at how that's done.
-
- in Scheme:
- simple values: 2, 3; #t, #f; #\h is a character (the eighth
-letter in the Latin alphabet)
- function values: +, *
- in Scheme, like in the lambda calculus, functions always go
-to the left: so you write (+ 2 3) not 2 + 3.
- compound non-function values: "h" "horse" and "" are three
-strings of different length (the string "h" is built from the character
-#\h but isn't identical to it; these values have different types)
- '(2 . 3) or (cons 2 3) is an ordered pair
- '(2 3) or (list 2 3) is a list. Other lists (with different
-lengths) are (list), (list 2), (list 2 3 4).
-
- OCaml:
- pretty much like Scheme, except that:
- the ordered pair is written (2, 3)
- the list is written [2; 3]
- the eighth character in the Latin alphabet is written 'h'
- the string consisting just of that character is written "h", as
-in Scheme
- true and false are written like that
- most functions are written leftmost, as in Scheme and the lambda
-calculus. But a few familiar binary operators can be written infix: so
-you can write 2 + 3. You can also write it function-leftmost, like so:
- ( + ) 2 3
- Here the parentheses are needed so that the OCaml parser can
-figure out what you're doing.
-
-Aside on parentheses:
-
- Parentheses are often optional in lambda caluli and also in OCaml.
- If M, N, and P are syntactically simple expressions, you can write ((M N) P), but you don't have to: you can also just write M N P. These mean exactly the same thing. To write M (N P) you do need the parentheses.
-
- In Scheme, EVERY parenthesis is meaningful and they are never
- optional. Typically parentheses mean to "apply this function to these
- arguments". So to add 2 and 3, you write (+ 2 3). In Scheme, this is different from
- ((+ 2) 3) --- we'll talk about this later. For the purposes of our
- course, it would be more convenient if Scheme behaved more like lambda
- calculi and OCaml here.
- However, parentheses sometimes also do other duty in Scheme: if you
- print out the list (list 2 3) (also writable '(2 3)), the interpreter
- will display: (2 3). And the pair (cons 2 3) will display: (2 . 3). The
- parentheses here don't mean that 2 is being used as an argument.
- However, if you asked Scheme to "evaluate" one of these, it would think
- you were using 2 as a function.
- There are good reasons why parentheses are used in "both" of these
- ways in Scheme. We'll leave them for you to discover and read about.
- Another example of parentheses in Scheme: most of the parentheses in
- (let ((x 2)) (+ x 1)) don't play the role of applying functions to arguments.
-
-
-Back to notation...
-
-We've described value variables and value constants in all of these
-languages. As we said, we'll follow the convention of using capital
-Latin letters as metalinguistic schemas for value expressions in each of
-the languages. Typically these schemas can stand for expressions of any
-syntactic complexity. When we want them to stand for syntactically
-simple expressions, we'll say so.
-
-
-When we get to types, we'll use small Greek letters as metalinguistic
-schemas for type expressions (of any syntactic complexity, unless we say
-otherwise).
-
-There are no type expressions or variables in standard Scheme.
-
-Type expressions in OCaml---whether type variables or constants
-representing predefined types---are usually written with lower-case
-expressions (following the same rules as object-language variables). So
-"stack" in OCaml could designate a type or a value; it depends on the
-linguistic context.
-
-OCaml (and all languages of its ML family) does have a special rule for
-type variables bound by quantifiers. Here you use 'x, 'stack, and so
-on. It looks like the prefix ' used in Scheme, but it's used very
-differently. Also, don't confuse the type variable 'x with the value
-variable x'.
-
-Aside:
- What's the difference between the type variable stack and the type
- variable 'stack? You use stack when you're binding it to a specific type
- value. So you might say:
- type stack = HERE SOME COMPLEX EXPRESSION THAT EXPRESSES A TYPE
- On the other hand, you use 'stack when you're only binding the variable
- with a quantifier: when you're saying such-and-such holds for EVERY type
- 'stack...
-
-
-It would be good for us to fix on conventions for object-language type
-constants and variables in the lambda calculi (and to use something
-other than small Greek letters, because they are metalanguage schemas).
- I don't know whether there are uniform conventions about this.
-
-
-
------ End forwarded message -----
------ Forwarded message from Jim Pryor <jim@jimpryor.net> -----
-
-1. Introducing and pounding on difference between declarative and
-imperatival computation.
-
-2. Some geography
-
- Haskell
-Scheme (functional parts) OCaml (functional parts)
- | |
- | |
- | |
-Untyped lambda calculus |
- | |
-Combinatorial logic |
- |
- |
-============ Turing complete (briefly explain)=======================
- |
- more advanced type systems |
- e.g. polymorphic types (System F)
- dependent types
-
- simply typed lambda calculus
- what linguists standardly use
-
-
-Imagine in third column to the right of the others:
-
-Typical languages like C, Python
-Imperatival parts of Scheme, OCaml
-
-
-3. How the same thing looks in each of these:
-
- in untyped lambda: add three two
- (if those are predefined, e.g. three defined as \sz.s(s(sz))
- in combinatorial logic: too long, pieces look like: S(BKI)K
-
- in Scheme: (let* [(three 3)
- (two 2)]
- (+ three two))
-
- in OCaml: let three = 3 in
- let two = 2 in
- three + 2;;
-
- in C: int three = 3;
- int two = 2;
- three + two;
-
-
-Mutation in C: int x = 0;
- x = 1;
-
- in OCaml: let x = ref 0 in
- x := 1;;
-
- in Scheme: (let* [(x (box 0))]
- (set-box! x 1))
-
-
-Pound more on how this is different, and we won't be looking at until a
-lot of groundwork has been laid.
-
-
-4. Question: how can mutation be something fundamentally new if some of
-these other languages without it are Turing complete? How are they able
-to encode/represent the same computations, without using mutation? (And
-in fact, Turing completeness is more than is needed for this.)
-
-Say a few words to sketch / reserve a place for an answer that they
-should be able to appreciate at the end of the course.
-
-
-5. Commonly people think of programming/computation as a sequence of
-changes. But in the languages we'll first be looking at, there are no
-changes. And moreover, there isn't at the beginning a very useful notion
-of sequencing, either.
-
-You can write sequences: in Scheme: (begin M N P Q R)
- in OCaml: begin M; N; P; Q; R end
- or: (M; N; P; Q; R)
-
-however, these just have the value of R. So if none of the earlier
-expressions have any side-effects / make any changes, a sequence ending
-in R means just the same as R.
-
-Aside:
- I'm fudging a bit here: there may also be a difference if some of the
- earlier expressions in the sequence are incomputable, and so have what we'll
- later be calling the "bottom" value. More on this when we talk about
- evaluation order in a few classes.
-
- Another difference is that sequencing is explicit about what order the
- expressions get evaluated in, and this can affect computational
- efficiency. But that's not about their semantics.)
-
-There's a bit of syntactic shorthand, which I'll introduce in a bit,
-that LOOKS LIKE a kind of sequencing. However, once you understand what
-it's shorthand for, you'll see that fundamentally, there's no sequencing
-going on.
-
-6. Instead of sequencing, we just have the
-evaluation/simplification/"reducing" of single, often syntactically
-complex, expressions.
- Later, when we introduce changes and sequencing, we'll do so in a
-way that makes that a new piece of syntactic structure.
-
-
-
-
-More "how to say the same thing in different languages"
-
-
-1. Anonymous functions
-
- Lambda: \x.B
- for example, \x. times x five
- here times and five are free variables, we suppose they're bound
- to appropriate values by the surrounding linguistic context
-
- Scheme: (lambda (x) B)
- for example, (lambda (x) (* x 5))
- -- perhaps aside about role of parens in Scheme should go here
-instead
-
- OCaml: fun x -> x * 5
- or: fun x -> ( * ) x 5
-
-
-2. Binding variables to values with "let"
-
- in Scheme:
- (let* [(x A) (y A')] B)
-
- explain that Scheme also has a simple "let", which sometimes
- has a different meaning from let*, and that they usually will
- want let*, so we'll stick to using that in our pedagogy
-
- explain that there's also a letrec, which does automatically
- something that we want them to learn how to do by hand
- so for the time being we'll avoid it
-
- in OCaml:
- let x = A in
- let y = A' in
- B
-
- for example: let x = 3 + 1 in
- ( * ) x 5
-
-
- explain OCaml also has "let rec", which we'll also avoid for now
-
-
-3. binding with "let" same as supplying as an argument to a function
-
- Scheme's (let* [(x A)] B) and OCaml's let x = A in B are the same
-as:
-
- in Lambda: (\x.B) A
-
- in Scheme: ((lambda (x) B) A)
-
- in OCaml: (fun x -> B) A
-
-
-4. Functions can also be bound to variables
-
- in Scheme: (let* [(f (lambda (x) B))] ...)
-
- in OCaml: let f = fun x -> B in ...
- OCaml shorthand: let f x = B in ...
-
-5. This in Scheme:
- (let* [(f (lambda (x) B))] (f A))
- as we've said, means the same as:
- ((lambda (x) B) A)
- and also means the same as:
- (let* [(x A)] B)
-
- Similarly, this in OCaml:
- let f = fun x -> B in
- f A
- or in shorthand:
- let f x = B in
- f A
- as we've said, means the same as:
- (fun x -> B) A
- and also means the same as:
- let x = A in
- B
-
-6. What if you want to do something like this:
-
- (let* [(x A)] ...rest of the file or interactive session...)
-
- let x = A in ...rest of the file or interactive session...
-
-You can override these bindings:
- (let* [(x A)] (let* [(x A')] B))
-is the same as:
- (let* [(x A')] B)
-
-The closest/innermost binding of x "shadows" or overrides more outer
-bindings.
-
-Scheme and OCaml have shorthands for wrapping a binding around the rest
-of the file or interactive session.
-
-In Scheme it's written like this:
- (define x A)
- ...rest of file or session...
-
-In OCaml it's written like this:
- let x = A;;
- ...rest of file or session...
-
-This is the construction that I said misleadingly looked like
-sequencing. Fundamentally, though, it's just a syntactic shorthand for
-complex let-expressions that don't involve any sequencing.
-
-
-7. One more bit of shorthand, which is very often used.
-
-This in Scheme:
- (define f (lambda (x) B))
-can be written like this:
- (define (f x) B)
-
-Similarly, this in OCaml:
- let f = fun x -> B;;
-can be written like this:
- let f x = B;;
-
-(Compare how "let f = fun x -> B in ..." can be written "let f x = B in
-...")
-
-
-
-
-Subject: Concatanation (!= sequencing)
-
-When we concatenate expressions in these languages, we'll usually be
-treating the leftmost expression as a function, and the rest of the
-expressions as arguments to it.
-
-M N P
-
-in lambda and OCaml treat M as as the function, and N as its first
-argument. M N should evaluate to another function, which takes P as its
-first argument. So this is equivalent to:
-
-(M N) P
-
-If you want M (N P) instead, you need to explicitly use parentheses.
-
-Explain currying:
- add three two = (add three) two
-
-In Scheme, on the other hand, in the first place you always need to
-include parentheses to force a function to be applied to arguments:
-
- (M N P)
-
-Moreover, there's a difference between ((M N) P) and (M N P). And each
-of those are different from ((M) N P). Scheme differentiates between
-functions that take one argument, those that take zero arguments (these
-are called "thunks"), and those that take more than one argument.
-
-This is awkward for our pedagogy, especially when you play with lambda
-calculus inside Scheme. We'll try to do some special tricks that will
-let ((M N) P) and (M N P) come out in Scheme when you'd expect them to.
-We'll tell you about this later.
-
-
-
-
-Subject: Constants / predefined variables
-
-In Scheme we have:
- #t and #f (Scheme uses # to start lots of special values, e.g. #\h)
- 2, 3
- +, *
-
- Syntax for building compound values: '(2 . 3) or (cons 2 3) is a
-pair; '(2 3) or (list 2 3) is a list. Other lists: '() or (list)
-
-In OCaml we have
- true, false
- 2, 3
- +, *
- in OCaml most functions are written to the left of their
-arguments, as in lambda and Scheme. But common arithmetic operations are
-infix unless they're enclosed in parens. So you'd write:
- 2 + 3
-or:
- ( + ) 2 3
-(Note: if you do this, best to always write ( + ) not (+). Sometimes it
-doesn't matter but sometimes it does because of a language design
-issue.)
- pairs: (2, 3)
- lists: [2; 3] others: []
-
-
-In lambda, we have:
- Nothing!
-
-Some lambda calculi do have constants, such as numbers. But mainstream
-ones don't.
-
-If you want boolean values, or numbers, or ordered pairs, or anything,
-you'll have to make them by hand out of the raw stuff of the lambda
-calculus.
-
-
-How do we build our own?
- We'll start with boolean values
- Next we'll do pairs, triples, and so on
- = possibly type-heterog collections, of a specific length >= 2
- Next class we'll do numbers
- We'll also do lists
- = ordered type-homogeneous collections permitting repetition,
- of arbitrary length >= 0
-
- Building multisets = unordered type-homog collections permitting rep
- sets = unordered type-homog collections without rep
- is harder. In these languages, functions are quite basic, ordered
-pairs are harder, sets harder yet. Inverts the usual conceptual order.
-
-
-Booleans
-
-if B is a boolean value (simple or syntactically complex), and IFTRUE
-and IFFALSE are any two other, arbitrary expressions, we want:
-
- B IFTRUE IFFALSE
-to evaluate either to IFTRUE or to IFFALSE (depending on which boolean
-value B is).
-
-For instance:
- equal? two three X Y
-should evaluate to Y.
-
-The boolean constant true needs to be an expression such that:
- true X Y
-always evaluate to X. How to do that?
-
-Easy: define true to be: \x \y. x
-Or more mnemonically: \t \f. t
-
-
-
-
-Ordered pairs
-
-If p is an ordered pair, we want it to accept a function of the form
-(\x y. B) which does something with its component values.
-
-For example:
- p (\x y. x)
-should return the first member of p.
- p (\x y. add x y)
-should return the sum of the members of p (assuming an appropriate
-binding for add).
-
- Note: `p (\x y. add x y)` could also be written as `p add`
-
-How to do this?
-
-Easy: define p to be (\f. f first_value second_value)
-
-then p (\x y. B) is
- (\f. f first_value second_value) (\x y. B) is
- (\x y. B) first_value second_value
-
-Some comments here about CPS.
-
-
------ End forwarded message -----
------ Forwarded message from Jim Pryor <jim@jimpryor.net> -----
-
-Date: Sun, 12 Sep 2010 20:13:46 -0400
-From: Jim Pryor <jim@jimpryor.net>
-To: Chris Barker <chris.barker@nyu.edu>
-Subject: Other...
-
-I've got some other notes pounding on the declarative / imperatival
-difference, that I'd want to work into discussion preceding everything I
-sent you.
-
-Other ideas I had for homework were just doing some beta-reductions and
-so on. I can look for some Scheme exercises in Little Schemer or another
-tutorial we've linked to. I'm sorry, I haven't really come up with much
-more specific yet here.
-
-Miscellany:
-
-I've got a pet peeve about the standard presentation of the grammar for
-lambda calculus as this simple, three rule system. Oh and then by the
-way here's also this unofficial shorthand. It's fine to give them that,
-but I also want to mention you can just give a mildly more complex
-grammar for what people really write. And we can point them to that. I
-worked it out myself, quickly, and could have missed some cases, but I
-think I have it. If you know of another statement of this, we could
-cross-check it sometime.
-
-I want to de-emphasize the role of alpha-conversion. It's perfectly reasonable to regard \x.x and \y.y as syntactically identical. I think Hankin has discussion of three ways to think about this, only one of which makes alpha-conversion any substantive transformation.
-
-I don't mind mentioning eta-reduction, but I want to signal that it
-makes a difference to the calculus whether that's permitted, say that
-we'll be discussing it some later, and for now they shouldn't think much
-about eta-reduction.
-
-
-Pedagogically I'd like to suppress eta-reduction by default, except when
-we explicitly allow it.
-
-
------ Forwarded message from Chris Barker <chris.barker@nyu.edu> -----
-