Re: MSFT C9 video on a monadic approach to location

[Meredith Gregory <lgreg.meredith@gmail.com>]

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