MSFT C9 video on a monadic approach to location

MSFT C9 video on a monadic approach to location

[Meredith Gregory]

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/ ]

Re: MSFT C9 video on a monadic approach to location

[Vaughan Pratt]

[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/ ]

Re: MSFT C9 video on a monadic approach to location

[Meredith Gregory]

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/ ]

Re: MSFT C9 video on a monadic approach to location

[categories]

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/ ]

MSFT C9 video on a monadic approach to location

[Meredith Gregory]

[-- Attachment #1: Type: multipart/alternative, Size: 650 bytes --]