From 1d9f6bfa82cc692c89a55d5f6da9cc65b8719ef3 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sun, 7 Nov 2010 21:34:11 -0500 Subject: [PATCH] Jacobson as a monad --- week8.mdwn | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/week8.mdwn b/week8.mdwn index e99e223a..27308c95 100644 --- a/week8.mdwn +++ b/week8.mdwn @@ -15,20 +15,22 @@ most one assignment. Jacobson's system contains two main combinators, *g* and *z*. She calls *g* the Geach rule, and *z* effects binding. (There is a third -combinator, *l*, which we'll make use of to adjust function/argument -order to better match English word order; N.B., though, that -Jacobson's name for this combinator is "lift", but it is different -from the monadic lift discussed in some detail below.) Here is a -typical computation (based closely on email from Simon Charlow, with -beta reduction as performed by the on-line evaluator): +combinator which following Curry and Steedman, I'll call *T*, which +we'll make use of to adjust function/argument order to better match +English word order; N.B., though, that Jacobson's name for this +combinator is "lift", but it is different from the monadic lift +discussed in some detail below.) Here is a typical computation (based +closely on email from Simon Charlow, with beta reduction as performed +by the on-line evaluator): 
 ; Analysis of "Everyone_i thinks he_i left"
 let g = \f g x. f (g x) in
 let z = \f g x. f (g x) x in
-let everyone = \P. FORALL x (P x) in
 let he = \x. x in
-everyone ((z thinks) (g left he))
+let everyone = \P. FORALL x (P x) in
+
+everyone (z thinks (g left he))
 
 ~~>  FORALL x (thinks (left x) x)
@@ -136,14 +138,14 @@ the parallel with the reader monad even more by writing a `shift` operator that used `unit` to produce a monadic result, if we wanted to. The monad version of *Everyone_i thinks he_i left*, then (remembering -that `he = fun x -> x`, and that `l a f = f a`) is +that `he = fun x -> x`, and letting `t a f = f a`) is 
 everyone (z thinks (g left he))
 
 ~~> forall w (thinks (left w) w)
 
-everyone (z thinks (g (l bill) (g said (g left he))))
+everyone (z thinks (g (t bill) (g said (g left he))))
 
 ~~> forall w (thinks (said (left w) bill) w)
-- 2.11.0