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