From c5c1236e4deb5ef61e2f1624d82e59a881604484 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 10:02:46 -0400 Subject: [PATCH 01/16] Add 'using the programming languages' Signed-off-by: Jim Pryor --- index.mdwn | 3 +++ using_the_programming_languages.mdwn | 0 2 files changed, 3 insertions(+) create mode 100644 using_the_programming_languages.mdwn diff --git a/index.mdwn b/index.mdwn index 7286d417..eb61fb70 100644 --- a/index.mdwn +++ b/index.mdwn @@ -135,6 +135,9 @@ familiar with one of them, it's not difficult to move between it and the other. [[How to get the programming languages running on your computer]] + +[[Using the programming languages]] + ## Recommended Books ## diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn new file mode 100644 index 00000000..e69de29b -- 2.11.0 From c805d825fc74745eabcdaade309fb50ee9829dc9 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 10:03:29 -0400 Subject: [PATCH 02/16] add .swp files to .gitignore Signed-off-by: Jim Pryor --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index b84c8066..35f5b3c4 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /.ikiwiki /recentchanges +/.*.swp -- 2.11.0 From 718c35b8eef781aef8bbd63e2c5ccebf6f5352dd Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 10:52:59 -0400 Subject: [PATCH 03/16] moved programming resources to new page, expanded Signed-off-by: Jim Pryor --- index.mdwn | 5 -- using_the_programming_languages.mdwn | 106 +++++++++++++++++++++++++++++++++++ 2 files changed, 106 insertions(+), 5 deletions(-) diff --git a/index.mdwn b/index.mdwn index eb61fb70..79538456 100644 --- a/index.mdwn +++ b/index.mdwn @@ -171,11 +171,6 @@ This covers some of the same introductory ground as The Little Schemer, but this time in ML. The dialect of ML used is SML, not OCaml, but there are only superficial syntactic differences between these languages. -# Other resources # - -* [Barker's Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda): tutorial with embedded Javascript code that enables a user to type a lambda form into a web browser page and click to execute (reduce) it. -* [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/): requires installing Java, but provides a number of tools for evaluating lambda expressions and other linguistic forms. - ##[[Schedule of Topics]]## ##[[Lecture Notes]]## diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index e69de29b..1c7aae6d 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -0,0 +1,106 @@ +We assume here that you've already gotten [Schema and OCaml installed on your computer](/how_to_get_the_programming_languages_running_on_your_computer/). + + +## Programming in the pure untyped lambda calculus ## + +There are several ways to do this, and we're still thinking out loud in this space about which method we should recommend you use. + +1. To get started, Chris has a nice [Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda) +webpage introducing the untyped lambda calculus. This page has embedded Javascript +code that enables you to type lambda expressions into your web browser page +and click a button to "execute" (that is, reduce or normalize) it. + + To do more than a few simple exercises, though, you'll need something more complex. + +2. One option is to use a short Scheme macro, like the one [linked at the bottom of Chris' webpage](http://homepages.nyu.edu/~cb125/Lambda/lambda.scm). +You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then (STEP BY STEP...). + + Here's Chris' explanation of the macro: + + (define (reduce f) ; 1 + ((lambda (value) (if (equal? value f) f (reduce value))) ; 2 + (let r ((f f) (g ())) ; 3 + (cond ((not (pair? f)) ; 4 + (if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g))))) ; 5 + ((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f))) ; 6 + (r (caddar f) (list (cadar f) (r (cadr f) g) g))) ; 7 + ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f))) ; 8 + (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g)))) ; 9 + (else (map (lambda (x) (r x g)) f)))))) ;10 + + If you have a Scheme interpreter, you can call the function like this: + + (reduce '(((lambda x (lambda y (x y))) 2) 3)) + ;Value: (2 3) + + (reduce '((lambda x (lambda y (x y))) 2)) + ;Value: (lambda #[promise 2] (2 #[promise 2])) + + Comments: f is the form to be evaluated, and g is the local assignment function; g has the structure (variable value g2), where g2 contains the rest of the assignments. The named let function r executes one pass through a form. The arguments to r are a form f, and an assignment function g. Line 2: continue to process the form until there are no more conversions left. Line 4 (substitution): If f is atomic [or if it is a promise], check to see if matches any variable in g and if so replace it with the new value. Line 6 (beta reduction): if f has the form ((lambda variable body) argument), it is a lambda form being applied to an argument, so perform lambda conversion. Remember to evaluate the argument too! Line 8 (alpha reduction): if f has the form (lambda variable body), replace the variable and its free occurences in the body with a unique object to prevent accidental variable collision. [In this implementation a unique object is constructed by building a promise. Note that the identity of the original variable can be recovered if you ever care by forcing the promise.] Line 10: recurse down the subparts of f. + + +3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it: + + A practical Lambda-calculator in Scheme + + The code below implements a normal-order interpreter for the untyped lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambda-calculus. Yet they make complex terms easier to define and apply. + + The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc. + + This calculator implements a normal-order evaluator for the untyped lambda-calculus with shortcuts. Shortcuts are distinguished constants that represent terms. An association between a shortcut symbol and a term must be declared before any term that contains the shortcut could be evaluated. The declaration of a shortcut does not cause the corresponding term to be evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet to be defined ones. Shortcuts make programming in lambda-calculus remarkably more convenient. + + Besides terms to reduce, this lambda-calculator accepts a set of commands, which add even more convenience. Commands define new shortcuts, activate tracing of all reductions, compare terms modulo alpha-conversion, print all defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file by a special command. + Examples + + First we define a few shortcuts: + + (X Define %c0 (L f (L x x))) ; Church numeral 0 + (X Define %succ (L c (L f (L x (f (c f x)))))) ; Successor + (X Define* %c1 (%succ %c0)) + (X Define* %c2 (%succ %c1)) + (X Define %add (L c (L d (L f (L x (c f (d f x))))))) ; Add two numerals + (X Define %mul (L c (L d (L f (c (d f)))))) ; Multiplication + + (%add %c1 %c2) + REPL reduces the term and prints the answer: (L f (L x (f (f (f x))))). + + (X equal? (%succ %c0) %c1) + (X equal?* (%succ %c0) %c1) + + The REPL executes the above commands and prints the answer: #f and #t, correspondingly. The second command reduces the terms before comparing them. + + See also . + + +4. Oleg also provides another lambda interpreter [written in +Haskell](http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell). +Jim converted this to OCaml and bundled it with a syntax extension that makes +it easier to write pure untyped lambda expressions in OCaml. You don't have to +know much OCaml yet to use it. Using it looks like this: + + let zero = < z>> + let succ = < s (n s z)>> + let one = << $succ$ $zero$ >> + let k = < y>> + let id = < x>> + let add = < n $succ$ m>> + let pred = < n (fun u v -> v (u s)) ($k$ z) $id$ >>;; + + church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;; + - : int = 2 + + +5. To play around with a **typed lambda calculus**, which we'll look at later +in the course, have a look at the [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/). +This requires installing Java, but provides a number of tools for evaluating +lambda expressions and other linguistic forms. (Mac users will most likely +already have Java installed.) + + +## Reading about Scheme ## + +[R5RS Scheme](http://people.csail.mit.edu/jaffer/r5rs_toc.html) + +## Reading about OCaml ## + + -- 2.11.0 From d773dfc0b5aab6bc79f9a6990af79aed988648f4 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 11:01:24 -0400 Subject: [PATCH 04/16] whitespace, formatting Signed-off-by: Jim Pryor --- ...ramming_languages_running_on_your_computer.mdwn | 4 +- index.mdwn | 8 +-- schedule_of_topics.mdwn | 2 +- using_the_programming_languages.mdwn | 72 ++++++++++++++++------ 4 files changed, 59 insertions(+), 27 deletions(-) diff --git a/how_to_get_the_programming_languages_running_on_your_computer.mdwn b/how_to_get_the_programming_languages_running_on_your_computer.mdwn index 8de3b703..063957a5 100644 --- a/how_to_get_the_programming_languages_running_on_your_computer.mdwn +++ b/how_to_get_the_programming_languages_running_on_your_computer.mdwn @@ -26,7 +26,7 @@ you'll be in one of two subgroups: Then you'll need pre-packaged (and usually pretty GUI) installers for everything. These are great when they're available and kept up-to-date; however those conditions aren't always met. - + If you're using **Windows**, you'll be in one of two subgroups: @@ -173,7 +173,7 @@ However, if you're not able to get that working, don't worry about it much. This will build an installer package which you should be able to double-click and install. - + * **To install on Mac with MacPorts** You can install the previous version of OCaml (3.11.2, diff --git a/index.mdwn b/index.mdwn index 79538456..877ff47e 100644 --- a/index.mdwn +++ b/index.mdwn @@ -81,7 +81,7 @@ Other keywords: the Curry-Howard isomorphism(s) monads in category theory and computation --> - + ## Who Can Participate? ## The course will not presume previous experience with programming. We @@ -90,12 +90,12 @@ languages, and we will encourage experimentation with running, modifying, and writing computer programs. The course will not presume lots of mathematical or logical background, either. -However, it will demand a certain amount of comfort working with such material; as a result, +However, it will demand a certain amount of comfort working with such material; as a result, it will not be especially well-suited to be a first graduate-level course in formal semantics or philosophy of language. If you have concerns about your background, come discuss them with us. -It hasn't yet been decided whether this course counts for satisfying the logic requirement for +It hasn't yet been decided whether this course counts for satisfying the logic requirement for Philosophy PhD students. Faculty and students from outside of NYU Linguistics and Philosophy are welcome @@ -138,7 +138,7 @@ other. [[Using the programming languages]] - + ## Recommended Books ## * *An Introduction to Lambda Calculi for Computer Scientists*, by Chris diff --git a/schedule_of_topics.mdwn b/schedule_of_topics.mdwn index eb7cf80a..50a9c33b 100644 --- a/schedule_of_topics.mdwn +++ b/schedule_of_topics.mdwn @@ -52,7 +52,7 @@ This is very sketchy at this point, but it should give a sense of our intended s 15. The types of continuations; continuations as first-class values 16. [Phil/ling application] Partee on whether NPs should be uniformly interpreted as generalized quantifiers, or instead "lifted" when necessary. Lifting = a CPS transform. 17. [Phil/ling application] Expletives

-18. Some references: +18. Some references: * [de Groote on the lambda-mu calculus in linguistics](http://www.loria.fr/%7Edegroote/papers/amsterdam01.pdf) * [on donkey anaphora and continuations](http://dx.doi.org/10.3765/sp.1.1) * [Wadler on symmetric sequent calculi](http://homepages.inf.ed.ac.uk/wadler/papers/dual-reloaded/dual-reloaded.pdf) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 1c7aae6d..9faaad4f 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -27,29 +27,60 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f))) ; 8 (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g)))) ; 9 (else (map (lambda (x) (r x g)) f)))))) ;10 - + If you have a Scheme interpreter, you can call the function like this: - + (reduce '(((lambda x (lambda y (x y))) 2) 3)) ;Value: (2 3) (reduce '((lambda x (lambda y (x y))) 2)) ;Value: (lambda #[promise 2] (2 #[promise 2])) - - Comments: f is the form to be evaluated, and g is the local assignment function; g has the structure (variable value g2), where g2 contains the rest of the assignments. The named let function r executes one pass through a form. The arguments to r are a form f, and an assignment function g. Line 2: continue to process the form until there are no more conversions left. Line 4 (substitution): If f is atomic [or if it is a promise], check to see if matches any variable in g and if so replace it with the new value. Line 6 (beta reduction): if f has the form ((lambda variable body) argument), it is a lambda form being applied to an argument, so perform lambda conversion. Remember to evaluate the argument too! Line 8 (alpha reduction): if f has the form (lambda variable body), replace the variable and its free occurences in the body with a unique object to prevent accidental variable collision. [In this implementation a unique object is constructed by building a promise. Note that the identity of the original variable can be recovered if you ever care by forcing the promise.] Line 10: recurse down the subparts of f. + + Comments: f is the form to be evaluated, and g is the local assignment + function; g has the structure (variable value g2), where g2 contains the rest + of the assignments. The named let function r executes one pass through a form. + The arguments to r are a form f, and an assignment function g. Line 2: continue + to process the form until there are no more conversions left. Line 4 + (substitution): If f is atomic [or if it is a promise], check to see if matches + any variable in g and if so replace it with the new value. Line 6 (beta + reduction): if f has the form ((lambda variable body) argument), it is a lambda + form being applied to an argument, so perform lambda conversion. Remember to + evaluate the argument too! Line 8 (alpha reduction): if f has the form (lambda + variable body), replace the variable and its free occurences in the body with a + unique object to prevent accidental variable collision. [In this implementation + a unique object is constructed by building a promise. Note that the identity of + the original variable can be recovered if you ever care by forcing the + promise.] Line 10: recurse down the subparts of f. 3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it: A practical Lambda-calculator in Scheme - The code below implements a normal-order interpreter for the untyped lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambda-calculus. Yet they make complex terms easier to define and apply. - - The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc. - - This calculator implements a normal-order evaluator for the untyped lambda-calculus with shortcuts. Shortcuts are distinguished constants that represent terms. An association between a shortcut symbol and a term must be declared before any term that contains the shortcut could be evaluated. The declaration of a shortcut does not cause the corresponding term to be evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet to be defined ones. Shortcuts make programming in lambda-calculus remarkably more convenient. + The code below implements a normal-order interpreter for the untyped + lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are + not first class and do not alter the semantics of the lambda-calculus. Yet they + make complex terms easier to define and apply. + + The code also includes a few convenience tools: tracing of all reduction, + comparing two terms modulo alpha-renaming, etc. + + This calculator implements a normal-order evaluator for the untyped + lambda-calculus with shortcuts. Shortcuts are distinguished constants that + represent terms. An association between a shortcut symbol and a term must be + declared before any term that contains the shortcut could be evaluated. The + declaration of a shortcut does not cause the corresponding term to be + evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet + to be defined ones. Shortcuts make programming in lambda-calculus remarkably + more convenient. + + Besides terms to reduce, this lambda-calculator accepts a set of commands, + which add even more convenience. Commands define new shortcuts, activate + tracing of all reductions, compare terms modulo alpha-conversion, print all + defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are + entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file + by a special command. - Besides terms to reduce, this lambda-calculator accepts a set of commands, which add even more convenience. Commands define new shortcuts, activate tracing of all reductions, compare terms modulo alpha-conversion, print all defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file by a special command. Examples First we define a few shortcuts: @@ -67,7 +98,8 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then (X equal? (%succ %c0) %c1) (X equal?* (%succ %c0) %c1) - The REPL executes the above commands and prints the answer: #f and #t, correspondingly. The second command reduces the terms before comparing them. + The REPL executes the above commands and prints the answer: #f and #t, + correspondingly. The second command reduces the terms before comparing them. See also . @@ -78,16 +110,16 @@ Jim converted this to OCaml and bundled it with a syntax extension that makes it easier to write pure untyped lambda expressions in OCaml. You don't have to know much OCaml yet to use it. Using it looks like this: - let zero = < z>> - let succ = < s (n s z)>> - let one = << $succ$ $zero$ >> - let k = < y>> - let id = < x>> - let add = < n $succ$ m>> - let pred = < n (fun u v -> v (u s)) ($k$ z) $id$ >>;; + let zero = < z>> + let succ = < s (n s z)>> + let one = << $succ$ $zero$ >> + let k = < y>> + let id = < x>> + let add = < n $succ$ m>> + let pred = < n (fun u v -> v (u s)) ($k$ z) $id$ >>;; - church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;; - - : int = 2 + church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;; + - : int = 2 5. To play around with a **typed lambda calculus**, which we'll look at later -- 2.11.0 From d3336a1a5f222802c44b5a827428a4968b7d39c0 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 11:14:23 -0400 Subject: [PATCH 05/16] tweaks to using page Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 44 ++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 9faaad4f..bfb97ae4 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -53,18 +53,19 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then promise.] Line 10: recurse down the subparts of f. -3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it: +3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it +(I've made some trivial changes to the text): A practical Lambda-calculator in Scheme - + The code below implements a normal-order interpreter for the untyped lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambda-calculus. Yet they make complex terms easier to define and apply. - + The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc. - + This calculator implements a normal-order evaluator for the untyped lambda-calculus with shortcuts. Shortcuts are distinguished constants that represent terms. An association between a shortcut symbol and a term must be @@ -73,31 +74,30 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet to be defined ones. Shortcuts make programming in lambda-calculus remarkably more convenient. - + Besides terms to reduce, this lambda-calculator accepts a set of commands, which add even more convenience. Commands define new shortcuts, activate tracing of all reductions, compare terms modulo alpha-conversion, print all defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file by a special command. - + Examples - + First we define a few shortcuts: - - (X Define %c0 (L f (L x x))) ; Church numeral 0 - (X Define %succ (L c (L f (L x (f (c f x)))))) ; Successor + + (X Define %c0 (L s (L z z))) ; Church numeral 0 + (X Define %succ (L n (L s (L z (s (n z z)))))) ; Successor (X Define* %c1 (%succ %c0)) (X Define* %c2 (%succ %c1)) - (X Define %add (L c (L d (L f (L x (c f (d f x))))))) ; Add two numerals - (X Define %mul (L c (L d (L f (c (d f)))))) ; Multiplication - - (%add %c1 %c2) + (X Define %add (L m (L n (L s (L z (m s (n s z))))))) ; Add two numerals + + (%add %c1 %c2) REPL reduces the term and prints the answer: (L f (L x (f (f (f x))))). - + (X equal? (%succ %c0) %c1) (X equal?* (%succ %c0) %c1) - + The REPL executes the above commands and prints the answer: #f and #t, correspondingly. The second command reduces the terms before comparing them. @@ -113,13 +113,13 @@ know much OCaml yet to use it. Using it looks like this: let zero = < z>> let succ = < s (n s z)>> let one = << $succ$ $zero$ >> - let k = < y>> - let id = < x>> + let two = << $succ$ $one$ >> let add = < n $succ$ m>> - let pred = < n (fun u v -> v (u s)) ($k$ z) $id$ >>;; - - church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;; - - : int = 2 + (* or *) + let add = < fun s z -> m s (n s z)>> + + church_to_int << $add$ $one$ $two$ >>;; + - : int = 3 5. To play around with a **typed lambda calculus**, which we'll look at later -- 2.11.0 From 7a29e788593675531e78ce0b29858d56fef39e3c Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 11:16:32 -0400 Subject: [PATCH 06/16] stub link to OCaml lambda calc Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 2 ++ 1 file changed, 2 insertions(+) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index bfb97ae4..6a87070b 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -121,6 +121,8 @@ know much OCaml yet to use it. Using it looks like this: church_to_int << $add$ $one$ $two$ >>;; - : int = 3 + To install Jim's OCaml bundle, DO THIS... + 5. To play around with a **typed lambda calculus**, which we'll look at later in the course, have a look at the [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/). -- 2.11.0 From 58f0762cdb57ea8f620249bec19714c6c08665dc Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 12:54:46 -0400 Subject: [PATCH 07/16] added notes on using OCaml lambda interpreter Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 6a87070b..52e4cffe 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -110,18 +110,29 @@ Jim converted this to OCaml and bundled it with a syntax extension that makes it easier to write pure untyped lambda expressions in OCaml. You don't have to know much OCaml yet to use it. Using it looks like this: - let zero = < z>> - let succ = < s (n s z)>> - let one = << $succ$ $zero$ >> - let two = << $succ$ $one$ >> - let add = < n $succ$ m>> + let zero = << fun s z -> z >>;; + let succ = << fun n s z -> s (n s z) >>;; + let one = << $succ$ $zero$ >>;; + let two = << $succ$ $one$ >>;; + let add = << fun m n -> n $succ$ m >>;; (* or *) - let add = < fun s z -> m s (n s z)>> + let add = << fun m n -> fun s z -> m s (n s z) >>;; church_to_int << $add$ $one$ $two$ >>;; - : int = 3 To install Jim's OCaml bundle, DO THIS... + + Some notes: + + * When you're talking to the interactive OCaml program, you have to finish complete statements with a ";;". Sometimes these aren't necessary, but rather than learn the rules yet about when you can get away without them, it's easiest to just use them consistently, like a period at the end of a sentence. + * The expressions inside the << and >> are an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: "let var = some_value;;" assigns a value to a variable, and "function_foo arg1 arg2" applies the specified function to the specified arguments. "church_to_int" is a function that takes a single argument --- the lambda expression that follows it, << $add$ $one$ $two$ >> -- and, if that expression has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line "- : int = 3" is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3. + * If you call church_to_int with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way. + * The $s inside the << and >> are essentially corner quotes. If we do this: "let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;" then the OCaml variable b will have as its value an (atomic) lambda expression, consisting just of the variable "a" in the untyped lambda calculus. On the other hand, the OCaml variable c will have as its value a lambda expression consisting just of the variable "*x*". That is, here the OCaml variable "a" is spliced into the lambda expression << $a$ >>. + * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression << w x y z >> is parsed via usual conventions as << (((w x) y) z) >>. Here << x y >> is not any single syntactic constituent. But if you do instead "let a = << x y >>;; let b = << w $a$ z >>", then what you get *will* have << x y >> as a constituent, and will be parsed as << ((w (x y)) z) >>. + * << fun x y -> something >> is equivalent to << fun x -> fun y -> something >>, which is parsed as << fun x -> (fun y -> something) >> (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in << fun x1 x2 x3 x4 x5 -> something >>. + * The << >> and $-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are run together with the << and >>: you can do either << fun x -> x >> or <x>>. But the $s *must* be separated from the << >> brackets with spaces or ( )s. + 5. To play around with a **typed lambda calculus**, which we'll look at later -- 2.11.0 From 853016cb8c3201ab406e8265803ecfa697d792a5 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 13:00:24 -0400 Subject: [PATCH 08/16] tweaked using OCaml lambda interpreter Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 52e4cffe..5a71e916 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -126,12 +126,18 @@ know much OCaml yet to use it. Using it looks like this: Some notes: * When you're talking to the interactive OCaml program, you have to finish complete statements with a ";;". Sometimes these aren't necessary, but rather than learn the rules yet about when you can get away without them, it's easiest to just use them consistently, like a period at the end of a sentence. - * The expressions inside the << and >> are an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: "let var = some_value;;" assigns a value to a variable, and "function_foo arg1 arg2" applies the specified function to the specified arguments. "church_to_int" is a function that takes a single argument --- the lambda expression that follows it, << $add$ $one$ $two$ >> -- and, if that expression has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line "- : int = 3" is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3. - * If you call church_to_int with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way. - * The $s inside the << and >> are essentially corner quotes. If we do this: "let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;" then the OCaml variable b will have as its value an (atomic) lambda expression, consisting just of the variable "a" in the untyped lambda calculus. On the other hand, the OCaml variable c will have as its value a lambda expression consisting just of the variable "*x*". That is, here the OCaml variable "a" is spliced into the lambda expression << $a$ >>. - * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression << w x y z >> is parsed via usual conventions as << (((w x) y) z) >>. Here << x y >> is not any single syntactic constituent. But if you do instead "let a = << x y >>;; let b = << w $a$ z >>", then what you get *will* have << x y >> as a constituent, and will be parsed as << ((w (x y)) z) >>. - * << fun x y -> something >> is equivalent to << fun x -> fun y -> something >>, which is parsed as << fun x -> (fun y -> something) >> (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in << fun x1 x2 x3 x4 x5 -> something >>. - * The << >> and $-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are run together with the << and >>: you can do either << fun x -> x >> or <x>>. But the $s *must* be separated from the << >> brackets with spaces or ( )s. + + * What's written betwen the `<<` and `>>` is parsed as an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: `let var = some_value;;` assigns a value to a variable, and `function_foo arg1 arg2` applies the specified function to the specified arguments. `church_to_int` is a function that takes a single argument --- the lambda expression that follows it, `<< $add$ $one$ $two$ >>` -- and, if that expression has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line `- : int = 3` is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3. + + * If you call `church_to_int` with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way. + + * The `$`s inside the `<<` and `>>` are essentially corner quotes. If we do this: `let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;` then the OCaml variable `b` will have as its value an (atomic) lambda expression, consisting just of the variable `a` in the untyped lambda calculus. On the other hand, the OCaml variable `c` will have as its value a lambda expression consisting just of the variable `x`. That is, here the OCaml variable `a` is spliced into the lambda expression `<< $a$ >>`. + + * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression `<< w x y z >>` is parsed via usual conventions as `<< (((w x) y) z) >>`. Here `<< x y >>` is not any single syntactic constituent. But if you do instead `let a = << x y >>;; let b = << w $a$ z >>`, then what you get *will* have `<< x y >>` as a constituent, and will be parsed as `<< ((w (x y)) z) >>`. + + * `<< fun x y -> something >>` is equivalent to `<< fun x -> fun y -> something >>`, which is parsed as `<< fun x -> (fun y -> something) >>` (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in `<< fun x1 x2 x3 x4 x5 -> something >>`. + + * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside with the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. -- 2.11.0 From 59c2b08c49b40480fa9507521b3e85d198cbe9ef Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 13:02:37 -0400 Subject: [PATCH 09/16] OCaml lambda interp: value of the var Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 5a71e916..5684823e 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -131,7 +131,7 @@ know much OCaml yet to use it. Using it looks like this: * If you call `church_to_int` with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way. - * The `$`s inside the `<<` and `>>` are essentially corner quotes. If we do this: `let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;` then the OCaml variable `b` will have as its value an (atomic) lambda expression, consisting just of the variable `a` in the untyped lambda calculus. On the other hand, the OCaml variable `c` will have as its value a lambda expression consisting just of the variable `x`. That is, here the OCaml variable `a` is spliced into the lambda expression `<< $a$ >>`. + * The `$`s inside the `<<` and `>>` are essentially corner quotes. If we do this: `let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;` then the OCaml variable `b` will have as its value an (atomic) lambda expression, consisting just of the variable `a` in the untyped lambda calculus. On the other hand, the OCaml variable `c` will have as its value a lambda expression consisting just of the variable `x`. That is, here the value of the OCaml variable `a` is spliced into the lambda expression `<< $a$ >>`. * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression `<< w x y z >>` is parsed via usual conventions as `<< (((w x) y) z) >>`. Here `<< x y >>` is not any single syntactic constituent. But if you do instead `let a = << x y >>;; let b = << w $a$ z >>`, then what you get *will* have `<< x y >>` as a constituent, and will be parsed as `<< ((w (x y)) z) >>`. -- 2.11.0 From 1712f331cae5fd829de0d6b5cbd4fe3c322b14e5 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 13:03:36 -0400 Subject: [PATCH 10/16] OCaml lambda interp: parens Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 5684823e..89dba4dd 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -135,7 +135,7 @@ know much OCaml yet to use it. Using it looks like this: * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression `<< w x y z >>` is parsed via usual conventions as `<< (((w x) y) z) >>`. Here `<< x y >>` is not any single syntactic constituent. But if you do instead `let a = << x y >>;; let b = << w $a$ z >>`, then what you get *will* have `<< x y >>` as a constituent, and will be parsed as `<< ((w (x y)) z) >>`. - * `<< fun x y -> something >>` is equivalent to `<< fun x -> fun y -> something >>`, which is parsed as `<< fun x -> (fun y -> something) >>` (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in `<< fun x1 x2 x3 x4 x5 -> something >>`. + * `<< fun x y -> something >>` is equivalent to `<< fun x -> fun y -> something >>`, which is parsed as `<< fun x -> (fun y -> (something)) >>` (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in `<< fun x1 x2 x3 x4 x5 -> something >>`. * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside with the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. -- 2.11.0 From bb39cb30cacc0252a77d4a4ec4199b1e1db1da52 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 13:04:32 -0400 Subject: [PATCH 11/16] OCaml lambda interp: surround brackets with spaces Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 89dba4dd..a910091e 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -137,7 +137,7 @@ know much OCaml yet to use it. Using it looks like this: * `<< fun x y -> something >>` is equivalent to `<< fun x -> fun y -> something >>`, which is parsed as `<< fun x -> (fun y -> (something)) >>` (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in `<< fun x1 x2 x3 x4 x5 -> something >>`. - * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside with the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. + * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside with the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. It's probably easiest to just always surround the `<<` and `>>` with spaces. -- 2.11.0 From 996ccf8e1b455abc03a10916ec37339325c8e8cc Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 13:06:16 -0400 Subject: [PATCH 12/16] OCaml lambda interp: when fully reduced Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index a910091e..461927c2 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -127,7 +127,7 @@ know much OCaml yet to use it. Using it looks like this: * When you're talking to the interactive OCaml program, you have to finish complete statements with a ";;". Sometimes these aren't necessary, but rather than learn the rules yet about when you can get away without them, it's easiest to just use them consistently, like a period at the end of a sentence. - * What's written betwen the `<<` and `>>` is parsed as an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: `let var = some_value;;` assigns a value to a variable, and `function_foo arg1 arg2` applies the specified function to the specified arguments. `church_to_int` is a function that takes a single argument --- the lambda expression that follows it, `<< $add$ $one$ $two$ >>` -- and, if that expression has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line `- : int = 3` is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3. + * What's written betwen the `<<` and `>>` is parsed as an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: `let var = some_value;;` assigns a value to a variable, and `function_foo arg1 arg2` applies the specified function to the specified arguments. `church_to_int` is a function that takes a single argument --- the lambda expression that follows it, `<< $add$ $one$ $two$ >>` -- and, if that expression when fully reduced or "normalized" has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line `- : int = 3` is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3. * If you call `church_to_int` with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way. -- 2.11.0 From 6b16fea470000df513c10a4d69631bd33d39c8f1 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 13:27:43 -0400 Subject: [PATCH 13/16] also added Chris' tutorial to offsite_reading Signed-off-by: Jim Pryor --- offsite_reading.mdwn | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/offsite_reading.mdwn b/offsite_reading.mdwn index 3e670b36..f41f816d 100644 --- a/offsite_reading.mdwn +++ b/offsite_reading.mdwn @@ -49,7 +49,9 @@ get more out of out. (Rinse and repeat.) ## Untyped lambda calculus and combinatory logic ## -* [[!wikipedia Lambda calculus]]

+* [[!wikipedia Lambda calculus]] +* [Chris Barker's Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda)

+ * [[!wikipedia Haskell Curry]] * [[!wikipedia Moses Schönfinkel]] * [[!wikipedia Alonzo Church]]

-- 2.11.0 From bf509c72901e685403b3976e1a91994dbdc31934 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 15:29:36 -0400 Subject: [PATCH 14/16] tweaked offsite_reading Signed-off-by: Jim Pryor --- offsite_reading.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/offsite_reading.mdwn b/offsite_reading.mdwn index f41f816d..b2bab593 100644 --- a/offsite_reading.mdwn +++ b/offsite_reading.mdwn @@ -57,8 +57,8 @@ get more out of out. (Rinse and repeat.) * [[!wikipedia Alonzo Church]]

* [[!wikipedia Combinatory logic]] * [Combinatory logic](http://plato.stanford.edu/entries/logic-combinatory/) at the Stanford Encyclopedia of Philosophy -* [[!wikipedia B,C,K,W system]] * [[!wikipedia SKI combinatory calculus]]

+* [[!wikipedia B,C,K,W system]] * [[!wikipedia Church-Rosser theorem]] * [[!wikipedia Normalization property]] * [[!wikipedia Turing completeness]]

-- 2.11.0 From 6bc67ca45d4311fb724df881aadc348858b880d3 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 15:31:57 -0400 Subject: [PATCH 15/16] offsite_reading typo Signed-off-by: Jim Pryor --- using_the_programming_languages.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 461927c2..2097dea2 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -137,7 +137,7 @@ know much OCaml yet to use it. Using it looks like this: * `<< fun x y -> something >>` is equivalent to `<< fun x -> fun y -> something >>`, which is parsed as `<< fun x -> (fun y -> (something)) >>` (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in `<< fun x1 x2 x3 x4 x5 -> something >>`. - * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside with the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. It's probably easiest to just always surround the `<<` and `>>` with spaces. + * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. It's probably easiest to just always surround the `<<` and `>>` with spaces. -- 2.11.0 From b0eaf38584e3896eb24654e0d5ce48dd26b8d01f Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 17:49:11 -0400 Subject: [PATCH 16/16] added family_tree Signed-off-by: Jim Pryor --- family_tree_of_functional_languages.mdwn | 44 ++++++++++++++++++++++++++++++++ index.mdwn | 1 + 2 files changed, 45 insertions(+) create mode 100644 family_tree_of_functional_languages.mdwn diff --git a/family_tree_of_functional_languages.mdwn b/family_tree_of_functional_languages.mdwn new file mode 100644 index 00000000..82003834 --- /dev/null +++ b/family_tree_of_functional_languages.mdwn @@ -0,0 +1,44 @@ +There's no need for you to know this for our seminar. But in case you're interested... + +Others (and ourselves) will often talk about "functional programming languages." But it would be more appropriate to talk of functional *paradigms* or *programming patterns*. Most programming languages are hybrids that allow programmers to use any of several programming paradigms. The ones that get called "functional languages" are just ones that give functional paradigms a central place in their design, and make them very easy to use. + +We can divide functional languages into two classes: those that are *dynamically typed* and those that are *statically typed*. + +The dynamically typed languages give types more of a background role in the program. They include the Lisp family (which in turn includes all the variants of [[!wikipedia Scheme]], and also [[!wikipedia Common Lisp]], and [[!wikipedia Clojure]]). They also include [[!wikipedia Erlang]] and [[!wikipedia Joy]] and [[!wikipedia Pure]], and others. + +Although these languages are hospitable to functional programming, some of them also permit you to write imperatival code too. In Scheme, by convention, imperatival functions are named ending with a "!". So `(set-car! p 1)` is a Scheme expression that, when evaluated, *mutates* the pair p so that its first member changes to 1. For our purposes though, we'll mostly be working with the parts of Scheme that are purely functional. We'll be discussing the difference between functional and imperatival programming a lot during the seminar. + +We're using Scheme in parallel with our discussion of *untyped* lambda calculi. Scheme isn't really untyped. If you assign a string to variable x and then try to add x to 1, Scheme will realize that strings aren't the right type of value to add to integers, and will complain about it. However, Scheme will complain about it *at runtime*: that is, at the point when that particular instruction is about the be executed. This is what's meant by calling these languages "dynamically typed." + +In practice, dynamically typed languages allow the programmer to be more relaxed about the types of the values they're manipulating. For instance, it's trivial to create a list whose first member is a string, whose second member is an integer, and so on. You just have to keep track somehow so that you don't try doing anything with values of the wrong type, else you'll get an error at runtime. + + +The other large class of languages are statically typed. This means that typing information is checked at *compile time*: that is, when you're converting your source code into a file that your computer knows how to directly execute. If you make type mistakes---for instance, you try to add a string to an integer---the compiler will choke on this so you never get to the point of even trying to run the program. Once you finally do get the program to compile, you can be more confident that errors of that sort have all been eliminated. They can't sneak up to bite you unawares while the program is running. + +Formerly, static typing required the programmer to add lots of annotations in her source code explicitly specifying what they type of each function argument is, what the type of the function's return value was, and so on. This is tedious, and partly for this reason dynamically typed languages have become popular and are thought of as easier to work with. However, nowadays statically typed languages tend to use "type inference": that is, you can let the computer do most of the work of figuring out what the types of everything are. For example, if you define a function like this: + + let foo x y = (1 + x, sqrt(y) ) + +the compiler will see that its first argument x is added to an integer, so it also needs to be an integer; and (supposing sqrt is known independently to take floating point arguments), foo's second argument y needs to be a floating point value. What's more, foo returns a pair whose first member is of type int and second member is of type float. The compiler can figure this out all on its own. The programmer doesn't have to explicitly spell it out, though she could, like follows: + + let foo (x:int) (y:float) : int*float = (1 + x, sqrt(y) ) + +This just says explicitly that foo takes an argument x of type int, an argument y of type float, and returns a pair of type int\*float (that is, a pair whose first member is if type int and whose second member is of type float). + +Type inference allows programmers to enjoy the benefits of strict compile-time type-checking, which as we said, helps eliminate a large class of errors at a more convenient time---when the program is being developed, rather than after it's been deployed and is running. While making life easier for the programmer, so that they don't have to explicitly write out the types of everything. (However, if a programmer doesn't keep track of types at least in her head, she's going to get into trouble and will face compile-time errors until she gets everything sorted out.) + +Though as we said dynamically-typed languages have become popular, programmers who get used to modern statically-typed languages find them productive. Sometimes they become zealots for working this way instead; at any case, they say that the popular dim opinion of static typing is based on out-of-date experiences of older languages like C and Java. + +Most functional programming languages these days are statically typed. + +We can further divide these languages based on whether they use *lazy* or *strict/eager* evaluation. We'll discuss the difference between these during the seminar. + +Most programming languages, functional or not, use strict/eager evaluation. For instance, languages of the ML family are all statically-typed functional languages with strict/eager evaluation. These include [[!wikipedia SML]] and [[!wikipedia Caml]] and [[!wikipedia Nemerle]]. Other statically-typed functional languages with strict/eager semantics are [[!wikipedia Scala]] and [[!wikipedia Coq]]. Like Scheme, many of these languages permit *imperatival* as well as functional coding; but they are regarded as functional programming languages because they are so hospitable to functional programming, and give it a central place in their design. + +A few languages such as [[!wikipedia Miranda]] and [[!wikipedia Haskell]] are statically-typed languages that instead mostly use lazy evaluation. However, it'd be more strictly accurate to say Haskell is lazy *by default*. You can also make Haskell evaluate some expressions strictly/eagerly; you just have to be ask for that explicitly. (I don't know about Miranda.) Languages like OCaml are the reverse: they're strict/eager by default, but you can get lazy evaluation where it's needed, you just have to ask for it explicitly. + +Unlike OCaml, Haskell is much more extreme about being non-imperatival. Though it's possible to write imperative code in Haskell, too; one just has to encapsulate it in a ST or IO *monad*. We'll be discussing in the seminar how monads can be used to create purely functional representations of imperatival algorithms. (You can do the same in languages like Scheme and OCaml, too. What's different is that in Haskell monads are the *only* way to deal with imperatival code.) + +We'll talk much more about monads, lazy vs strict evaluation, and functional vs imperatival code as we proceed. + + diff --git a/index.mdwn b/index.mdwn index 877ff47e..c10667bb 100644 --- a/index.mdwn +++ b/index.mdwn @@ -138,6 +138,7 @@ other. [[Using the programming languages]] +[[Family tree of functional programming languages]] ## Recommended Books ## -- 2.11.0