Here is:

1. a category of games.
2. a proposal about IO.

1. Category of games

Everything is relative to a pair (S,Phi), where
S is a set, and Phi : S -> Fam (Fam S).  
S is the set of states. 
I write Phi(s) = { { nxt(s,c,r) | r : Rsp s c } | c : Cmd s } 
So Phi says what commands (moves) may be issued, what responses they
may get, and what the state becomes.  
By a game I mean just a state. 

  [ This framework may seem a bit strange.  I reason that one can
    always put a family of games `side by side', and so it
    is sufficient to consider a single set of rules, and identify
    a game with its initial state. ]

If you think of Cmd(s) as consisting of atomic instructions, then we
may define a set Cmd^*(s) of molecular "programs", by an inductive
definition:

  Cmd^*(s) = 1 + (Sigma c : Cmd(s))(Pi r : Rsp(s,c))Cmd^*(nxt(s,c,r))

The "1 +" represents the possibility of a no-op or skip program (that
just immediately returns).  (The family { Cmd^*(s) | s : S } 
is essentially a family of Peterson-Synek trees, but "with leaves".
One can pun about a leaf, and a leave-taking or exit.)

If p : Cmd^*(s) we define a set Rsp^*(s,p) of the possible
traces of responses.  

  Rsp^*(s,p) = case p of inl 0     -> 1 
			 inr (c,f) -> (Sigma r : Rsp(s,c)) Rsp^* (nxt(s,c,r) 

We can also define nxt^*(s,p,t), which tells
you the state in which a program exits. 

  nxt^*(s,p,t) = case p of inl 0     -> s
                           inr (c,f) -> case t of (r,t') -> 
                                        nxt^*(nxt(s,c,r),f(r),t')

The objects of the category are states.  I define the homsets by an
inductive definition, that is as the initial algebra for a certain
endo-functor on the category of binary set-valued functions on S
(with pointwise morphisms), namely:

  F(R,a,b) = Pi c    : Cmd(a)     . 
             Sigma p : Cmd^*(b)   . 
	     Pi t    : Rsp^*(b,p) . 
	     Sigma r : Rsp(a,c)   . 
		 R(nxt(a,c,r),nxt^*(b,p,t)) 

(Action on morphisms left to the reader.  Basically covariant
because R occurs only positively in the rhs.) 

  hom(a,b) = (mu R : R = F(R))(a,b) 

Considered (a la Curry-Howard) as a relation between states, the
hom-set function is a simulation (co-algebra for F).  But note, it is
a *least* fixed point - the coalgebra is the inverse of the initial
algebra constructor : F(hom) \subseteq hom.

The computational interpretation of the morphisms is that they are
strategies for responding to commands for the domain state by
running a (possibly null) subroutine on the codomain state.  
( Or perhaps it is more intuitive to think of the commands as
arriving for the codomain state ..)

(There is also an interpretation in terms of Aczel's rule sets.  A
morphism from A to B allows us to translate proofs of A (maybe open,
i.e. from hypotheses) to proofs of B, a step at a time.)

I don't know much about the category that results, beyond it is a
category (with a kind of copy-cat as the identity morphism, `in-lining
of subroutines' as the composition).  Perhaps it has all the
categorical gubbins and symmetrical monoidal hoojits that one needs in
game semantics.  It would I think be interesting to see what happens
when one tries to make game models of constructive type theory.  This
might (speculating wildly) shed some light on how to incorporate both
initial algebra types and final coalgebra types in a common framework.
(But first, what about the ordinary non-dependent function type?)

There are a bunch of other mildly interesting concepts that have
natural inductive definitions. 

The principle of inductive definitions used here seems
proof-theoretically rather strong (in general).  Probably it has the
strength of the W-type.  In games for which the sets Cmd and Rsp are
finite(/countable), I suspect that the definition of hom has the
strength of first order arithmetic(/ID_1) .  There is a Pi
over Rsp^*(b,p), but that set is in general finite (/countable).
There is a strong scent of K\"onig's lemma in the vicinity.  Somehow
we are going "right up to the brink". 

2. A proposal about IO

In Haskell, the typing judgment of a (main) program is

  main :: IO ()

meaning that running main evokes a computation which returns with the
element of the standard singleton type, if it returns at all.  (The
system arranges that on return (or uncaught exception) it effectively
calls System.exitWith, a primitive which does not return.)

There are various things to remark here: 

 * the program might hang, i.e. go into a coma, 
   computing forever the `next' interaction. 

 * the program needn't exit.  It may carry on
   interacting forever. 

 * the value returned is junk.  The type judgment
   says nothing about the specification of the program. 
   What a waste! 

How do things look from the perspective that the type system of a
functional programming language should be rich enough to let us write
down (the statements and proofs of) constructive mathematics, and
should ensure that evaluation (to whnf, at least) always terminates?

My idea is that the typing judgment should be 

  main :: IO(X,Y) 

where X and Y are state predicates.  The judgement means that
if started in a state satisfying X (i.e. with some hypothetical
proof that X is satisfied), then the program will
terminate in a state satisfying Y (i.e. with a proof dependent
on this initial assumption that X is satisfied). 

  WARNING: I do not really know exactly what I mean by a 
  state predicate.  Should it be a plain type-valued function?
  Or boolean valued?  Or should `state-predicate' be somehow
  something primitive?  How should state predicates behave
  with respect to simulation? 

To define this, I define a predicate transformer `<|', written
infix, with the state on the left. 

  s <| X = ( Sigma p : Cmd^*(s), Pi t : Rsp^*(s,p) ) X(nxt^*(s,p,t) 
	   where s : S, X : Pow S. 

(The predicate transformer X |-> (<| X) can be seen as a monad
on a certain category of predicates.)

Then I define IO as follows: 

  IO(X,Y) = (Pi s : S) X(s) => s <| Y 

If this is the type of a program, then I think it follows that the
specification of an IO primitive should have the same form.  It should
say:

  * Under what conditions it terminates. 
  * In those conditions, the weakest precondition on the current
    state which guarantees a given predicate X holds in the next state.

A program that never exits will have type of the form IO(X,\ s -> False). 
A typical Haskell program will have type IO(\ s -> True, \ s -> True ). 

... rough stuff below

Some general properties.

1. thinning on right
IO(X,Y)    Y \subseteq Y'
_________________________
  IO(X,Y') 

2. thinning on left
X \subseteq X'   IO(X',Y) 
_________________________
  IO(X,Y) 

2.5. skip
_____________
  IO(X,X)

3. skip'
X \subseteq Y
_______________
  IO(X,Y) 

4. composition
IO(X,Y)    IO(Y,Z)
__________________
  IO(X,Z)

3&4 => 1&2&2.5 

See Hoare and He Jifeng, Unifying Theories of Programming, p95. 

-----

I am not persuaded by Andy Gordon's thesis that the correctness of
functional programs is to be proved by establishing a bisimulation
between a specification (one program), and its implementation
(another).  Of course one doesn't want the implementation to be
capable of doing something that the specification can't.  But why
should one want the implementation to be *capable* of doing anything
the specification can?  We really want the things that *have to*
happen in the specification to follow from the things that have to
happen in the implementation.  We want all and only the right things
to happen.

-----

State variables, state functions, state predicates.

  We might say: 

  * A state is a function from state variables, or observables
    to values. 

	State = Var -> Val

  * A state predicate is a function from states to propositions
    (truth-values, whatever you like to call them ...)

	Pred  = (Var -> Val) -> Prop

Observable

  Some classic tangle: 
    observation (action)  - how to measure air pressure (in certain units)
    observation (instance of an action) - a particular measuring.
    observation (value)   - such and such a value 
    observation (instance) - value obtained in a particular case
    observable            - air pressure (capable of being measured
			    in various units). 
   
  Some identified or named procedure for measuring or otherwise
obtaining a value on a given occasion.  
  Hoare & He Jifeng p 24.
  Does observable mean something basic, like the position or momentum
of a particle, or could it mean some random statistic like the number
of people in the supermarket with some brand of baked beans in their
basket?

  Do we really have any conception of `all observables', so that they
can form the domain of a function?  Do they form a set?  A class?
(Hoare & He Jifeng seems to think this is obvious: "Every predicate
P(x,y,..,z) can be identified with the closed set of all tuples of
observations that satisfy it."  

  Are observations (things you do) mathematical entities at all? 

  I recall trying to accustom myself to the idea in a book on quantum
mechanics that an observable could be modelled as a certain kind of
operator on Hilbert space.  Ever since then I have felt extremely
nervous about the idea of an observable. (Something nasty in the
woodshed.) 


State variable

  How about another word like state variable?  This at least avoids
any potentially confusing overlap with the terminology of mathematical
physics.   Is it something syntactic?  Just a free variable?  One subject
to special conventions involving `decorations' like prime (`\'')?

State variables, as opposed to state functions, are perhaps
from which the state functions are obtained by composition with
ordinary mathematical functions.  

What *is* a state variable?  Something you directly observe?
Something part of the tacit context of the specification you are
writing?  

State

  Is the idea that an instantaneous state of the universe (or what
will do as the universe for practical purposes), is a point in some
multi-dimensional space, specified by its value in each of various
dimensions?  Are these dimensions the state variables?  Are they in
any sense independent?  (Perhaps instead of a `dimension', I should
think of projections onto lower dimensional spaces.  Perhaps even the
moderately well-behaved operators of the mathematical physicists.)

  [ Lampson somewhere introduces state variables as `subspaces' of 
a state space. 
    There is some dark stuff at the front of Dijkstra and
Scholten `Predicate calculus and program semantics' about states,
state spaces, and so on.  They suggest that there is something
sordid about the very idea an individual state,
except perhaps where program semantics is concerned. ]

  Is there a more `predicate oriented' view, according to which
a state is identified with all the state predicates true in that
state?  Some sense in which states are an abstraction from
predicates, predictions, hypotheses, experiments, .. ? 
(The world is all that is the case..)

  The idea of instantaneous state is something that needs analysis.
Is it a kind of postulate?  It is surely closely related to the idea
of a point in the continuum.  Knowing something of the analysis of the
notion of point in terms of neighbourhoods and coverings, it is
natural to wonder whether it works in exactly the same way for
(temporal) instants, as well as for spatial points.  Time is
all downhill.

  Noone has ever seen an instantaneous state of the universe. It is an
abstraction.  From what?  From experiments.

Experiment

  Experiment is just a fancy name for observation?

  It is tempting to think that an experiment is something boolean
valued.  (The truth value of a hypothesis being tested.) But maybe
it is better to think of it as just the recording of some data/events,
under certain circumstances or initial conditions.  Then comes the
interpretation of the data, and a judgement about its relevance to a
hypothesis.

  In an experiment, the experimentor follows some program - the
experimental procedure.  They (or their apparatus) perform certain
basic steps, in response to what they see.  The experiment has some
outcome, which is a value, not necessarily boolean.  The experimentor
moves first (spontaneously).

  Perhaps an observation (value) can be thought of as a basic
neighbourhood of the state of the universe -- all of those states in
which the observation (action) yields that value.  

  An important kind of basic observation is a terminating procedure
that yields concrete recordable values (like finite sequences of
rational intervals).  Would it be performing an observation if we run
an experiment which does not terminate, but just amasses more and more
data?  Maybe, but perhaps it is some kind of `point at infinity'.

  What do I expect in practice?  That the specification of an IO
interface presents us with some mathematical model of the state of the
world, in which the state-space is some subset of a product indexed by
real variables.  To this we may add auxiliary, hidden variables.
The specification of an individual primitive will look rather like a 
state relation, or predicate on pairs of states -- most of the time. 

-----

  Lawvere seems to think that variables (dynamically varying
quantities or values) are somehow more real, objective, sacred, ..
and values (the very things that we observe of variables) are somehow
more abstract, subjective, bourgeoise, .. . (His first examples are
morphisms with domain `time', codomain `position'.)

-----

  Hoare & He Jifeng. p 28: "Since our concern is primarily with
descriptions of physical systems, we shall prefer to use predicates
containing free variables selected from an alphabet whose existence,
composition and meaning can only be explained informally by relating
them to reality."

  Why do Hoare & He Jifeng say `alphabet'? (p 9.)