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.
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)