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
|
