+[[!toc levels=3]]
+
## Links to tutorials and other resources on Scheme, OCaml, and Haskell ##
* Help on [[Learning Scheme]]
* Help on [[Learning OCaml]]
* Help on [[Learning Haskell]]
+
<!-- -->
* This site's [[explanation of the differences|rosetta1]] between these languages
* [[Famous Computer Scientists|people]]
+## Old links ##
+
+*The links below are from the last time we taught the course; we should check them again...*
-<!--
There's lots of links here already to tutorials and encyclopedia entries about many of the notions we'll be dealing with.
Many of these links are to Wikipedia. You can learn a lot from such articles,
the group and hopefully get to a point where you can read it again and
get more out of. (Rinse and repeat.)
-## Functions ##
+### Functions ###
* [[!wikipedia Higher-order function]]
* [[!wikipedia First-class function]]
* [[!wikipedia Currying]]
-## Functional vs imperative programming ##
+### Functional vs imperative programming ###
* [[!wikipedia Declarative programming]]
* [[!wikipedia Functional programming]]
* [[!wikipedia Side effect (computer science) desc="Side effects"]]
* [[!wikipedia Imperative programming]]
-## General issues about variables and scope in programming languages ##
+### General issues about variables and scope in programming languages ###
* [[!wikipedia Variable (programming) desc="Variables"]]
* [[!wikipedia Free variables and bound variables]]
* [[!wikipedia Scope (programming) desc="Variable scope"]]
* [[!wikipedia Closure (computer science) desc="Closures"]]
-##[[Learning Scheme]]##
-## Untyped lambda calculus and combinatory logic ##
+### Untyped lambda calculus and combinatory logic ###
* [[Dana Scott's Turing centenary address on the lambda calculus|http://turing100.acm.org/lambda_calculus_timeline.pdf]]
* [[!wikipedia Lambda calculus]]
* [Combinator Birds](http://www.angelfire.com/tx4/cus/combinator/birds.html)
* [Les deux combinateurs et la totalite](http://www.paulbraffort.net/j_et_i/j_et_i.html) by Paul Braffort.
-## Evaluation Order ##
+### Evaluation Order ###
* [[!wikipedia Evaluation strategy]]
* [[!wikipedia Eager evaluation]]
* [[!wikipedia Lazy evaluation]]
* [[!wikipedia Strict programming language]]
-## Confluence, Normalization, Undecidability ##
+### Confluence, Normalization, Undecidability ###
* [[!wikipedia Church-Rosser theorem]]
* [[!wikipedia Normalization property]]
* [Scooping the Loop Snooper](http://www.cl.cam.ac.uk/teaching/0910/CompTheory/scooping.pdf), a proof of the undecidability of the halting problem in the style of Dr Seuss by Geoffrey K. Pullum
-## Recursion and the Y Combinator ##
+### Recursion and the Y Combinator ###
* [[!wikipedia Recursion (computer science) desc="Recursion"]]
* [[!wikipedia Y combinator]]
* [The Y Combinator](http://dangermouse.brynmawr.edu/cs245/ycomb_jim.html) derives the applicative-order Y-combinator from scratch, in Scheme. This derivation is similar in flavor to the derivation found in The Little Schemer, but uses a slightly different starting approach...
* [The church of the least fixed point, by Sans Pareil](http://www.springerlink.com/content/n4t2v573m58g2755/)
-## Folds ##
+### Folds ###
* [[!wikipedia Fold (higher-order function)]]
-## Types ##
+### Types ###
* [[!wikipedia Typed lambda calculus]]
* [[!wikipedia Simply typed lambda calculus]]
* [[!wikipedia Bottom type]]
-##[[Learning OCaml]]##
-
-## Monads ##
+### Monads ###
* [[!wikipedia Monad (functional programming) desc="Monads in Functional Programming"]]
* [Daniel Friedman. A Schemer's View of Monads](/schemersviewofmonads.ps): from <https://www.cs.indiana.edu/cgi-pub/c311/doku.php?id=home> but the link above is to a local copy.
* [A Gentle Intro to Haskell: About Monads](http://www.haskell.org/tutorial/monads.html) (link currently broken, check <http://www.haskell.org/haskellwiki/Tutorials>)
* Monsters and context-shifting, e.g. Gillies/von Fintel on "ifs" [not sure which paper]
-## Monads in Category Theory ##
+### Monads in Category Theory ###
* [Category Theory at SEP](http://plato.stanford.edu/entries/category-theory/)
* [[!wikipedia Category theory]]
* [A Partial Ordering of some Category Theory applied to Haskell](http://blog.sigfpe.com/2010/03/partial-ordering-of-some-category.html)
-## Side-effects / mutation ##
+### Side-effects / mutation ###
* [[!wikipedia Referential transparency (computer science)]]
* [[!wikipedia Side effect (computer science) desc="Side effects"]]
* [Pointers in OCaml](http://caml.inria.fr/resources/doc/guides/pointers.html)
-## Continuations ##
+### Continuations ###
* [[!wikipedia Continuation]]
* [[!wikipedia Continuation-passing style]]
* [Delimited continuations in natural language semantics](http://okmij.org/ftp/gengo/)
-## The Curry-Howard Correspondence ##
+### The Curry-Howard Correspondence ###
* The [[!wikipedia Curry-Howard isomorphism]]
* [The Curry-Howard correspondence in Haskell](http://www.thenewsh.com/~newsham/formal/curryhoward/)
* [Haskell wikibook on the Curry-Howard Isomorphism](http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism) at Haskell wiki<p>
-## Linear Logic ##
+### Linear Logic ###
* [[!wikipedia Linear logic]]
--->
intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
though without explicitly using monads.
-All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
+All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
To run it, download the file, start OCaml, and say
# #use "intensionality-monad.ml";;
</pre>
This system is modeled on the way Montague arranged his grammar.
-There are significant simplifications: for instance, determiner
-phrases are thought of as corresponding to individuals rather than to
-generalized quantifiers.
+There are significant simplifications compared to Montague: for
+instance, determiner phrases are thought of here as corresponding to
+individuals rather than to generalized quantifiers.
The main difference between the intensional types and the extensional
types is that in the intensional types, the arguments are functions
In addition, the result of each predicate is an intension.
This expresses the fact that the set of people who left in one world
may be different than the set of people who left in a different world.
-(Normally, the dependence of the extension of a predicate to the world
+
+Normally, the dependence of the extension of a predicate to the world
of evaluation is hidden inside of an evaluation coordinate, or built
into the the lexical meaning function, but we've made it explicit here
-in the way that the intensionality monad makes most natural.)
+in the way that the intensionality monad makes most natural.
The intensional types are more complicated than the extensional
types. Wouldn't it be nice to make the complicated types available
using the value that `x` was bound to in context<sub>2</sub>, _where `f` was bound_?
-In fact, when we specified rules for the Lambda Calculus, we committed ourselves to taking the second of these strategies. But both of the kinds of binding described here are perfectly coherent. The first is called "dynamic binding" or "dynamic scoping" and the second is called "lexical or static binding/scoping". Neither is intrinsically more correct or appropriate than the other. The first is somewhat easier for the people who write implementations of programming languages to handle; so historically it used to predominate. But the second is easier for programmers to reason about. In Scheme, variables are bound in the lexical/static way by default, just as in the Lambda Calculus; but there is special vocabulary for dealing with dynamic binding too, which is useful in some situations. (As far as I'm aware, Haskell and OCaml only provide the lexical/static binding.)
+In fact, when we specified rules for the Lambda Calculus, we committed ourselves to taking the second of these strategies. But both of the kinds of binding described here are perfectly coherent. The first is called "dynamic binding" or "dynamic scoping" and the second is called "lexical or static binding/scoping". Neither is intrinsically more correct or appropriate than the other. The first is somewhat easier for the people who write implementations of programming languages to handle; so historically it used to predominate. But the second is easier for programmers to reason about.
-In any case, if we're going to have the same semantics as the untyped Lambda Calculus, we're going to have to make sure that when we bind the variable `f` to the value `\y. y x`, that (locally) free variable `x` remains associated with the value `2` that `x` was bound to in the context where `f` is bound, not the possibly different value that `x` may be bound to later, when `f` is applied. One thing we might consider doing is _evaluating the body_ of the abstract that we want to bind `f` to, using the then-current environment to evaluate the variables that the abstract doesn't itself bind. But that's not a good idea. What if the body of that abstract never terminates? The whole program might be OK, because it might never go on to apply `f`. But we'll be stuck trying to evaluate `f`'s body anyway, and will never get to the rest of the program. Another thing we could consider doing is to substitute the `2` in for the variable `x`, and then bind `f` to `\y. y 2`. That would work, but the whole point of this evaluation strategy is to avoid doing those complicated (and inefficient) substitutions. Can you think of a third idea?
+> In Scheme, variables are bound in the lexical/static way by default, just as in the Lambda Calculus; but there is special vocabulary for dealing with dynamic binding too, which is useful in some situations. As far as I'm aware, Haskell and OCaml only provide the lexical/static binding. <em>Shell scripts</em>, on the other hand, only use dynamic binding. If you type this at a shell prompt: `( x=0; foo() { echo $x; }; bar() { local x=1; foo; }; bar )`, it will print `1` not `0`.
+
+In any case, if we're going to have the same semantics as the untyped Lambda Calculus, we're going to have to make sure that when we bind the variable `f` to the value `\y. y x`, that (locally) free variable `x` remains associated with the value `0` that `x` was bound to in the context where `f` is bound, not the possibly different value that `x` may be bound to later, when `f` is applied. One thing we might consider doing is _evaluating the body_ of the abstract that we want to bind `f` to, using the then-current environment to evaluate the variables that the abstract doesn't itself bind. But that's not a good idea. What if the body of that abstract never terminates? The whole program might be OK, because it might never go on to apply `f`. But we'll be stuck trying to evaluate `f`'s body anyway, and will never get to the rest of the program. Another thing we could consider doing is to substitute the `2` in for the variable `x`, and then bind `f` to `\y. y 2`. That would work, but the whole point of this evaluation strategy is to avoid doing those complicated (and inefficient) substitutions. Can you think of a third idea?
What we will do is have our environment associate `f` not just with a `Lambda` term, but also with the environment that was in place _when_ `f` was bound. Then later, if we ever do use `f`, we have that saved environment around to look up any free variables in. More specifically, we'll associate `f` not with the _term_: