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

[Alan Jeffrey]

It occurs to me that what you're doing is a dependent resumption 
semantics.  Recalling (e.g. from Hennessy and Plotkin 1979) that a 
(deterministic) resumption model for states S is a solution to the equation:

   M = S + (S x (S -> M))

that is, a program either terminates in state s (inl s) or yields in 
state s, with continuation f (inr (s , f)).  What you've done is 
distinguish the three uses of S, to get:

   M = A + (C x (R -> M))

and then further made R depend on C:

   M = A + ((c : C) x (R c -> M))

Would it be reasonable to call your model a (deterministic) dependent 
resumption semantics?

I agree with your argument re. open vs closed models.  Another way of 
looking at this is that Haskell's IO is a black box, where your model is 
more like a glass box.  This has its tradeoffs: the good news is you can 
write code-transforming / introspecting functions in your style, and the 
bad news is you can write code-transforming / introspecting functions :-)

A.

On 09/23/2010 09:01 AM, Anton Setzer wrote:
> 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
>
>
>