[Haskell-cafe] 2-level type analysis of introducing naming into data types

[Greg Meredith]

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 <jgbailey at gmail.com> wrote:

> 2008/3/15 Greg Meredith <lgreg.meredith at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080317/c220c763/attachment.htm