> infixr +!  
> infixr +?  

There seems to be an intuitive notion of the discriminative power or
`acuity' of an interactive program, and of the interactive programs
allowed by a typesystem. I am not finding it easy to formulate it
precisely, and am open to arguments that it makes no sense, or
suggestions about how to formulate the idea.

As a drastic simplification, we can model interactive programs as
communicating with messages coded as integers.  I suppose that the
program sends the first message, the environment sends the next, and
further messages are exchanged in strict alternation until finally the
program sends the last message.  (This surely captures a lot of
programs.)  To make this more precise, we can represent these programs
using a pair of mutually recursive types:

> data ProgW = Write Int ProgR             -- writer programs
> data ProgR = Halt | Read (Int -> ProgW)  -- reader programs

We can interpret these programs as consuming an infinite stream of
integers and returning a log of their interactions (using a state
monad).

> data LogW  = Out Int LogR
> data LogR  = End  | In Int LogW

> interpw :: ProgW -> [ Int ] -> ( LogW     , [ Int ] )
> interpw (Write i pr)  inp   =  ( Out i lr ,   res   )
>                                where ( lr ,   res   ) = interpr pr inp
> interpr :: ProgR -> [ Int ] -> ( LogR     , [ Int ] )
> interpr Halt          inp   =  ( End      ,   inp   )
> interpr (Read f)  (i:inp)   =  ( In i lw  ,   res   )
>                                where ( lw ,   res   ) = interpw (f i) inp

Definition: It seems reasonable to say that two programs of the same
kind (i.e. both readers or both writers) are *behaviourally equal* if
their interpretations give the same values on all infinite streams of
inputs.

For example, here is a program that perpetually writes the cumulative
sum of the inputs it has seen so far

> example1 :: ProgW
> example1 = e 0 where e n = Write n (Read (\m -> e (n + m)))

A modification of it, halting when the output has overflowed some
limit:

> example2 :: ProgW
> example2 = 
>   e 0 where e n = Write n (if n < 65536 
>                              then Read (\m -> e (n + m)) 
>                              else Halt)

The following seem to me the most interesting kinds
of program (in ProgW and ProgR).

  * productive (or non-hanging) programs which always evaluate to
    constructor form (Write, Read or Halt).

  * perpetual programs, which are productive programs that never halt,
    whatever the input stream.  

  * wellfounded programs, which are productive programs that always
    halt (returning a finite log).  One practical interest of these is
    that they can safely be run "in batch" as isolated transactions
    having exclusive use of all resources.

Wellfounded programs seem to play a key role.  Example2 is for some
purposes an adequate approximation to example1, and we can make this
more precise by defining approximation of an arbitrary program by a
wellfounded program using the following kind of `addition'

> (+?) :: ProgR -> ProgR -> ProgR
> (+!) :: ProgW -> ProgR -> ProgW
> Halt +? p       = p
> Read f +? p     = Read (\i -> (f i) +! p)
> Write n pr +! p = Write n (pr +? p)

Definition: A wellfounded program p1 :: ProgW (or ProgR) *approximates*
a productive program p2 :: ProgW (resp. ProgR) if there is a program
p3 :: ProgR such that (addw p1 p3) is behaviourally equal to p2.
Clearly p1 has to be well-founded for this definition to make sense.

Conjecture: productive programs are behaviourally equal if and
only if they are approximated by the same wellfounded programs.

Definition: say that a program p1 is at least as discriminating as a
program p2 (p1 \geq p2) if 

    fst(interpw p1 inp) = fst(inpterpw p1 inp') 
    => fst(interpw p2 inp') = fst(inpterpw p2 inp') 

Conjecture: p1 +? p2 is at least as discriminating as a2. 

Conjecture: Given any two programs, we can find a program which
is at least as discriminating as them both. 

Conjecture: Given any countable family of programs, we can 
find a program which is at least as discriminating as any program
in the family. 

(A program partitions the input stream into countably many basic
intervals on each of which it is constant.)



--------------
detritus ...

> type Input = String
> type Out = String
> data E a = Pay a | Use Input (Out -> E a)
> data M a = Yap a | Rsp Out (Input -> M a)

These are both monads

> playE (Pay a) x = Left a
> playE (Use i phi) (Yap b) = Right b
> playE (Use i phi) (Rsp o psi) = playE (phi o) (psi i)
> playM (Yap b) x = Right b
> playM (Rsp o psi) (Pay a) = Left a
> playM (Rsp o psi) (Use i phi) = playM (psi i) (phi o)

> data StrF a x  = StrF a x
> data Str a     = Str (StrF a (Str a))
> push a as      = Str (StrF a as) 
> top (Str (StrF a as)) = a
> pop (Str (StrF a as)) = as
> reps (Str (StrF f fs)) x = Str (StrF x xs) where xs = reps fs (f x)
> bang a = let x = Str (StrF a x) in x 

> type Inp       = Str Int
> data State b   = State (Inp -> StrF b Inp)

> instance Monad State where
>   return x     = State ( StrF x )
>   (State g >>= f)  
>                = State ( (\(StrF b inp) -> 
>                          (\(State h) -> h inp) (f b) ) . g)


> consume1 :: State Int
> consume1 = State (\(Str as) -> as )

> intw :: ProgW -> State LogW 
> intr :: ProgR -> State LogR 
> intw (Write n pr) = do lr <- intr pr
>                        return (Out n lr) 
> intr (Read fw)    = do n  <- consume1 
>                        lw <- intw (fw n)
>                        return (In n lw) 

> intr Halt         = return End

> data B  =  Z  |  I  B  |  R  (Int -> B) 
> data Bt =  Zt |  It Bt |  Rt Int Bt      | IOpt Nat Bt
> iint :: B -> State Bt
> iint Z     = return Zt
> iint (I b) = do t <- iint b   ; return (It t)
> iint (R f) = do x <- consume1 ; t <- iint (f x) ; return (Rt x t)

A more eager kind of interpretation.

> data NatF x    = Zero | Succ x 
> data Nat       = Nat (NatF Nat) 
> ini            = Nat Zero
> nxt n          = Nat (Succ n) 

> iint'  :: B -> State Bt
> iint'  Z     = return Zt
> iint'  (I b) = do t <- iint'' b nxt ; return (It t)
> iint'  (R f) = do x <- consume1 ; t <- iint' (f x) ; return (Rt x t)
> iint'' :: B -> (Nat -> Nat) -> State Bt
> iint'' (I b) bf = iint'' b (nxt . bf) 
> iint'' x bf  = do l <- iint' x ; return (IOpt (bf ini) l)



Try to define a combination of two programs which is at least as
discriminating as both.

> mx a b = case a of 
>           Z    -> b
>           I a' -> case b of Z -> a'
>                             I b' -> mx a' b'
>                             R f  -> R (\i-> mx a' (f i))
>           R f  -> case b of Z -> a 
>                             I b' -> R (\i-> mx (f i) b')
>			      R g  -> R (\i-> mx (f i) (g i))


Two ordinals can fight each other.  

> win  :: ProgR -> ProgW -> Bool
> win Halt  a      = False
> win (Read f) (Write n r ) = not (win r (f n))

Here is another kind of contest. 

> lose :: B -> B -> Bool
> lose Z     a      = True
> lose (I p) Z      = False       
> lose (I p) (I q)  = lose p (I q)             -- the user writes (skip ours)
> lose (I p) (R f)  = lose p (R (f . (+1)))    -- the user reads
> lose (R f) Z      = False       
> lose (R f) (I q)  = lose (R (f . (+1))) q    -- the user writes
> lose (R f) (R g)  = lose (f 0) (R g)         -- the user reads


 > import Prelude hiding ((*),(^),(+))

> data N x = N x [N x]
> instance Monad N where
>   return x = N x []
>   (N x ts) >>= f = app (f x) [ t >>= f | t <- ts ]
>                    where app (N y us) us' = N y (us ++ us')