[lambda.git] / monday

----- 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> -----