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

[Anton Setzer]

On 22/09/10 21:14, Alan Jeffrey wrote:
> Can you say a bit about why this approach is better than a plain old
> monad?  Why is it better to be parametric in C, R and translateLocal
> rather than fix:
>
>   C = \exists IO
>   R (X , io) = X
>   translateLocal (X , io) = io
>
> ?  Also, monads (or premonoidal categories if you prefer) have a nice
> categorical presentation, could you say how to interpret your
> construction categorically?
>
> A.
>

Maybe I should give a condensed answer to the question what is better
about being parametric:
In Haskell we have one IO type which should serve all possible
interfaces. Therefore this data type must be an open data type, to which
everybody could add whatever she wants. But this means that one has to
deal with open data types, which is something different from all other
data types in Haskell.

By making IO parametric we get a closed data type which serves one
specific interface. Now one can inspect it and can (using the translate
operation I mentioned before) translate it into a different
interface, and have different execute operations for different
interfaces. One could have one
for programs with console input, one for GUIs, one for file handling,
one for interfacing with the controls of a car, and build execution
functions
which take a combination of such interfaces (e.g. GUI + file handling)

 One can reason about the elements of this data type etc.
In Haskell one has a problem since the interface necessarily seems to be
a dependent type
(    (C : Set) x (R : C -> Set) ). In Agda we can do better.

Anton



-- 
---------------------------------------
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/
---------------------------------------