author Jim Pryor Tue, 24 Aug 2010 16:54:46 +0000 (12:54 -0400) committer Jim Pryor Tue, 24 Aug 2010 16:54:46 +0000 (12:54 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>

index 6a87070..52e4cff 100644 (file)
@@ -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 = <<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>>
+               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 m n -> 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 <<fun x->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