Dear Categorists, Most of the content in this lecture/discussion<http://channel9.msdn.com/shows/Going+Deep/E2E-Whiteboard-Jam-Session-with-Brian-Beckman-Greg-Meredith-Monads-and-Coordinate-Systems/>is probably already known and better presented elsewhere. However, the approach to unifying nominal and positional access to data in computations is novel, to the best of my knowledge. So, it may be of interest here. Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 1219 NW 83rd St Seattle, WA 98117 +1 206.650.3740 http://biosimilarity.blogspot.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Categorists, Most of the content in this lecture/discussion<http://channel9.msdn.com/shows/Going+Deep/E2E-Whiteboard-Jam-Session-with-Brian-Beckman-Greg-Meredith-Monads-and-Coordinate-Systems/>is probably already known and better presented elsewhere. However, the approach to unifying nominal and positional access to data in computations is novel, to the best of my knowledge. So, it may be of interest here. Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 1219 NW 83rd St Seattle, WA 98117 +1 206.650.3740 http://biosimilarity.blogspot.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[From moderator: From: field inadvertently omitted from this post; sorry Vaughan] On 7/8/2010 8:41 AM, Meredith Gregory wrote:
Most of the content in this lecture/discussion<http://channel9.msdn.com/shows/Going+Deep/E2E-Whiteboard-Jam-Session-with-Brian-Beckman-Greg-Meredith-Monads-and-Coordinate-Systems/>is probably already known and better presented elsewhere. However, the approach to unifying nominal and positional access to data in computations is novel, to the best of my knowledge. So, it may be of interest here.
It might be helpful if the derivatives+fixpoints view of lambda terms described in this talk was connected up somehow to the more naive view of monads found in CWM, which might be put as follows. (I may not get everything perfectly typed, in which case I'd be happy to see a cleaner version aimed at the same intuition about syntax.) A monad is a functor T: C --> C in a category whose objects are to be understood as term languages (think sets of terms, though C need not be Set) such that for any term language X in ob(C), TX is the term language over X. "Over X" means that the terms in X play the role in TX as the variables occurring in the terms of TX. The unit eta_X: X --> TX as a morphism of C indicates which terms of TX are to be understood as its variables. The equations making eta_X both a left and right unit assert respectively that substituting a term for a variable (in the above sense of variable) is that term, and that substituting a variable for itself in a term is that term. The multiplication mu_X: TTX --> TX specifies how terms constructed as terms of terms are to be understood simply as terms. This is where the equational theory lives in the monad, namely as the kernel of mu_X; for example TTX might contain each of x(y+z) and xy+yz as a term of terms, which mu_X would identify as being the same term. Associativity of mu_X asserts that the order in which terms of terms of terms in TTTX are assembled is immaterial: when using mu_X twice to reduce TTTX to TX, the first step can reduce either the first two T's in TTTX or the last two. The functor T: C --> C makes this notion of monad an object of type C^C. In the interest of reducing this type complexity Haskell reorganizes the notion of monad in terms of Bind and Return operations. The above talk featuring Brian Beckman and Greg seems to be from the latter perspective, although neither definition of monad was given during the talk, raising the question of whether the derivatives+fixpoints view is better supported by one or the other view of monads, or is independent of both. Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 7/8/2010 8:41 AM, Meredith Gregory wrote:
Most of the content in this lecture/discussion<http://channel9.msdn.com/shows/Going+Deep/E2E-Whiteboard-Jam-Session-with-Brian-Beckman-Greg-Meredith-Monads-and-Coordinate-Systems/>is probably already known and better presented elsewhere. However, the approach to unifying nominal and positional access to data in computations is novel, to the best of my knowledge. So, it may be of interest here.
It might be helpful if the derivatives+fixpoints view of lambda terms described in this talk was connected up somehow to the more naive view of monads found in CWM, which might be put as follows. (I may not get everything perfectly typed, in which case I'd be happy to see a cleaner version aimed at the same intuition about syntax.) A monad is a functor T: C --> C in a category whose objects are to be understood as term languages (think sets of terms, though C need not be Set) such that for any term language X in ob(C), TX is the term language over X. "Over X" means that the terms in X play the role in TX as the variables occurring in the terms of TX. The unit eta_X: X --> TX as a morphism of C indicates which terms of TX are to be understood as its variables. The equations making eta_X both a left and right unit assert respectively that substituting a term for a variable (in the above sense of variable) is that term, and that substituting a variable for itself in a term is that term. The multiplication mu_X: TTX --> TX specifies how terms constructed as terms of terms are to be understood simply as terms. This is where the equational theory lives in the monad, namely as the kernel of mu_X; for example TTX might contain each of x(y+z) and xy+yz as a term of terms, which mu_X would identify as being the same term. Associativity of mu_X asserts that the order in which terms of terms of terms in TTTX are assembled is immaterial: when using mu_X twice to reduce TTTX to TX, the first step can reduce either the first two T's in TTTX or the last two. The functor T: C --> C makes this notion of monad an object of type C^C. In the interest of reducing this type complexity Haskell reorganizes the notion of monad in terms of Bind and Return operations. The above talk featuring Brian Beckman and Greg seems to be from the latter perspective, although neither definition of monad was given during the talk, raising the question of whether the derivatives+fixpoints view is better supported by one or the other view of monads, or is independent of both. Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Vaughan, i should mention that for the type, M[=E2=88=82=C2=B5Mx=C2=B5M,=C2=B5M], to b= e inhabited you need some way to bottom out the recursion. In the reflective= higher-order pi-calculus that corresponds to the constant summand, 1, repre= senting the stopped process.=20 For the lambda calculus you need to do something similar -- like add in an e= xplicit distinguished representation of divergence, or add in some ground te= rms, like the booleans.=20 More generally, the trick needs to employ the option monad if the type is is= o to 1+N for appropriate N. i'm happy to provide either Haskell or Scala code to illustrate that the pro= cedure is effective. i can also provide OCaml code, but it's considerably mo= re verbose and painful to write. Best wishes, --greg Managing Partner Biosimilarity LLC [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
categories＠mta.ca -
Meredith Gregory -
Vaughan Pratt