Re: MSFT C9 video on a monadic approach to location

[categories@mta.ca]

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