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 example (the type of Conway games). The type is naturally motivated because through the application of one functor we arrive at a lambda calculus with an embedded type for Conway games (giving access to field operations for arithmetic on virtually every type of number ever considered) -- while another functor provides a process calculi with a similarly embedded data type. Moreover, the technique extends to a wide variety of algebra(ic data type)s. The recipe is simple. 1. Provide a recursive specification of the algebra. Example. data Game = Game [Game] [Game] 2. Abstract the specification using parametric polymorphism. Example. data PolyGame g = PolyGame [g] [g] 2.a. Identify the 2-Level knot-tying version of the recursive type Example. data RGame = RGame (PolyGame RGame) 3. Insert name management type into the knot-tying step of the 2-Level version Example. data DefRefGame var = DefRefGame (PolyDefRef var (PolyGame (DefRefGame var))) given the basic form data PolyDefRef var val = Def var (PolyDefRef var val) (PolyDefRef var val) | Ref var | Val val is the name management technology We illustrate the idea with two other forms of name management technology: the lambda calculus and the pi-calculus. Then we show that names themselves can be provided as the codes of the terms of the new type. At the root of this work is the proposal that communication begins from the concrete -- a "closed" recursive type -- representing some observation or proposal of how something works in the universe (of discourse). As said proposal develops or is explored, calculations need to rely more and more on naming (i.e. "let x stand for ... in ..."). Thus, this capability is "injected" into the data type -- moving from the concrete to the general. The analysis above provides a concrete, disciplined procedure for achieving this in both a sequential and concurrent computational setting. Best wishes, --greg -- This code summarizes the previous post. It shows that for any -- "closed" recursive type we can devise a closed extension of this -- type embedding the type as a value in the lambda calculus module Grho( Game, PolyGame, PolyDefRef, DefRefGame, QDefRefGame ,Term, GTerm, QGTerm ,Sum, Agent, Process, GProcess, QGProcess ) where -- Conway's original data type data Game = Game [Game] [Game] deriving (Eq,Show) -- Abstracting Conway's data type data PolyGame g = PolyGame [g] [g] deriving (Eq,Show) -- Recovering Conway's data type in terms of the abstraction newtype RGame = RGame (PolyGame RGame) deriving (Eq,Show) -- RGame ~ Game -- Expressions with references and values data PolyDefRef var val = Def var (PolyDefRef var val) (PolyDefRef var val) | Ref var | Val val deriving (Eq,Show) -- Games with references and values data DefRefGame var = DefRefGame (PolyDefRef var (PolyGame (DefRefGame var))) deriving (Eq,Show) -- Games with references and values in which variables are quoted games newtype QDefRefGame = QDefRefGame (DefRefGame QDefRefGame) deriving (Eq,Show) -- Lambda terms with values data Term var val = Var var | Abs [var] (Term var val) | App (Term var val) [Term var val] | Value val deriving (Eq,Show) -- Lambda terms with games as values data GTerm var = Term var (PolyGame (GTerm var)) deriving (Eq,Show) -- Lambda terms with games as values and variables that are quoted lambda terms data QGTerm = GTerm QGTerm -- And the following defn's/eqns take it one step further by providing a notion of process with -- Conway games as embedded values -- Process terms with values -- Sums data Sum var val agent = PValue val | Locate var agent | Sum [Sum var val agent] deriving (Eq,Show) -- One of the recent observations i've had about the process calculi -- is that '0' is Ground, and as such is another place to introduce -- new Ground. Thus, we can remove the production for '0' and replace -- it with the types of values we would like processes to 'produce'; -- hence the PValue arm of the type, Sum, above. Note that this -- design choice means that we can have expressions of the form -- v1 + v2 + ... + vk + x1A1 + ... xnAn -- i am inclined to treat this as structurally equivalent to -- x1A1 + ... xnAn -- but there is another alternative: to allow -- sums of values to represent superpositions -- Agents data Agent var proc = Input [var] proc | Output [proc] deriving (Eq,Show) -- Processes data Process var sum = Case sum | Deref var | Compose [Process var sum] deriving (Eq,Show) -- Processes over games data GProcess var = Process var (Sum var (PolyGame (GProcess var)) (Agent var (GProcess var))) deriving (Eq,Show) -- Processes over games with quoted process for variables newtype QGProcess = QGProcess (GProcess QGProcess) deriving (Eq,Show) -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com