[Agda] IO, semi-closed handles, and problems with extensional equality

[Anton Setzer]

In my last email I made a mistake.
The translation of an IO program from one language which I thought had type

(map : (c : C) -> IO C' R' (R c)) -> IO C R A -> IO C' R' A

by replacing atomic commands in the high level language C
by programs  (map c) : IO C' R' (R c)
doesn't work.
map c could be  of the form (leaf r)
in this case the operation would collapse the tree into a leaf,
which doesn't work if the tree is non-wellfounded.
This problem we had already observed in an early paper (me and
Peter Hancock).
In order to repair it one has to replace the type of map
by
map : (c : C) -> IO+ C' R' (R c)
where IO+ C' R' B is the set of IO programs which have at least one
interaction.

Here is the full code (which uses codata  but can be easily translated into
data with \infty)

module refinementPrograms where


codata IO (C : Set) (R : C -> Set) (A : Set) : Set where
  node : (c : C) -> (R c -> IO C R A) -> IO C R A
  leaf : A -> IO C R A


_>>_ : {C : Set}{R : C -> Set}{A : Set}{B : Set}->
       IO C R A -> (A -> IO C R B) -> IO C R B
node c f >> g = node c (\ r -> f r >> g)
leaf a   >> g = g a


-- IO+ is the set of IO programs with at least one interaction
-- (It's like having apart from the natural numbers the positive natural
--  numbers)
data IO+ (C : Set) (R : C -> Set) (A : Set) : Set where
  node : (c : C) -> (R c -> IO C R A) -> IO+ C R A


mutual
  translate : {C : Set}{R : C -> Set}{C' : Set}{R' : C' -> Set}{A : Set}
              (map : (c : C) -> IO+ C' R' (R c))
              -> IO C R A
              -> IO C' R' A
  translate map (node c f) = translateaux map (map c) f
  translate map (leaf a) = leaf a
 
  -- translateaux map p q  and
  -- translateaux' map p q are   both
  -- p >> \ a -> translate map (q a)
  -- one for p: IO+ ...  and one for p : IO ...

  translateaux : {C : Set}{R : C -> Set}{C' : Set}{R' : C' -> Set}{A :
Set}{B : Set}
                 (map : (c : C) -> IO+ C' R' (R c))
                 -> IO+ C' R' B
                 -> (B -> IO C R A)
                 -> IO C' R' A          
  translateaux map (node c g) f = node c (λ r -> translateaux' map (g r) f)


  translateaux' : {C : Set}{R : C -> Set}{C' : Set}{R' : C' -> Set}{A :
Set}{B : Set}
                 (map : (c : C) -> IO+ C' R' (R c))
                 -> IO C' R' B
                 -> (B -> IO C R A)
                 -> IO C' R' A          
  translateaux' map (node c g) f = node c (λ r -> translateaux' map (g r) f)
  translateaux' map (leaf r) f = translate map (f r)


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------