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 new code.

Best wishes,

--greg

On Mon, Mar 17, 2008 at 8:52 AM, Justin Bailey <jgbailey@gmail.com> wrote:

2008/3/15 Greg Meredith <lgreg.meredith@biosimilarity.com>:

> 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