Justin,
Thanks for the query. Here are the considerations/concerns i with which i
was working.
- Data is *not* native to either lambda or pi-calculi
- operational encodings for simple types (Bool and Nat) were
given near the inception of these calculi
- embeddings of these types took several decades to work out
semantically (full abstraction for PCF is an example of the difficulty in
the case of lambda; i submit that we haven't really figured out the
corresponding story for concurrency, yet)
- On the other hand, naming is necessary for effective work with
any moderately complex recursive data structure
- this is so common we are like fish to this water -- we don't
even recognize when we're doing it (as an example see Conway's original
presentation of numbers as games -- he starts using naming but does not
acknowledge this very subtle shift in the mathematics)
- Lambda and pi-calculi are the best name management technology
we know
- Is there a natural and elementary way to provide the benefits of
these name management technologies for dealing with these concrete data
structures?
Yes, it turns out that the simplest way finds solutions as sitting between
least and greatest fixpoints of the functor that pops out of the 2-level
type analysis (hence the pretty domain equations that are expressed as
Haskell data types). Moreover, it also gives a freebie way to embed data
types in these decidedly operational calculi. Further, as i only recently
realized it gives a way to compare Brian Smith style reflection with the
reflection Matthias Radestock and i identified with the rho-calculus. See
this<http://svn.biosimilarity.com/src/open/mirrororrim/rho/trunk/src/main/haskell/grho.hs>new
code.
Best wishes,
--greg
On Mon, Mar 17, 2008 at 8:52 AM, Justin Bailey <[EMAIL PROTECTED]> wrote:
> 2008/3/15 Greg Meredith <[EMAIL PROTECTED]>:
> > All,
> >
> >
> > The following Haskell code gives a 2-level type analysis of a
> > functorial approach to introducing naming and name management into a
> > given (recursive) data type. The analysis is performed by means of an
>
> What's the upshot of this? That is, what does this analysis give you?
> I mostly follow the argument but I don't understand the benefits. I
> feel like I'm missing something.
>
> Justin
>
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105
+1 206.650.3740
http://biosimilarity.blogspot.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
