2-Level type analysis of adding names to games

-- 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
-- (or other name mgt) 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)