[Agda] IO, semi-closed handles, and problems with extensional
equality
Anton Setzer
A.G.Setzer at swansea.ac.uk
Wed Sep 22 23:32:07 CEST 2010
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.
Our approach is that one distinguishes between the data type of IO
programs and its execution.
An IO program is an infinite tree which represents the actions carried
out by the program.
This IO tree is a possibilty non-well-founded tree with inner nodes
labelled by
commands and with a node labelled by command c having branching degree R c.
The leafs are labelled by elements a: A where A is the type in IO A.
In old Agda with codata this type is defined as
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
which is just an F-coalgebra where
F X = ((c : C) x (R c -> X) ) + A
(In the current Agda this has to be replaced by a data type with
some infinity symbols)
One can now define
return : A -> IO C R A
return a = leaf a
and
_>>_ : 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
and prove that the Monad laws hold with respect to bisimulation equality.
Therefore what we have is an implementation of a monad.
Therefore the set of IO programs is just a standard data type in Agda
(it's a set
of infinite trees), about which one could reason. We defined for instance a
new composition relation:
If you have
p : (c : C) -> IO C' R' (R c)
which means for every command in the high level language C
you have an IO program in the low level language C' R' which returns
an element of R c
then you obtain an operation
f : IO C R A -> IO C' R' A
f (node c g) = (p c) >> \ r : R c -> f (g r)
f (leaf a) = leaf a
So for each command c: C one executes the program p c
and uses the response of p c to determine the response used for the
next step.
The execution of an IO program is a completely separate issue. It is not
normalisation of an element of IO C R A
(an element of this type reduces to (node c f) or (leaf a) )
You need an external function execute, which is not executed from inside
Agda
Execute will be relative to some fixed interface which corresponds to
real world
programs (such as opening a window, drawing a line, writing to the keyboard,
getting input from the mouse)
If p : IO C R A for this interfaer C R
the exeuction of p is as follows:
It normalises p
If p reduces to node c g
then command c is executed in the real world, and once the real world
responds with response r (r could be an element of the one element type
1 in
case the command is something which only receives an acknowledgement that
it was done, like drawing a line; or it could be the input from the real
world
such as the coordinates of the last mouse movement)
execute continues with (g r)
If p reduces to leaf a
then the program stops and gives answer a.
So categorically we just determine one possible Monad and define
IO C R A as a data type of Agda.
We just don't treat the IO monad as a new atomic data type in Agda
with separate rules but define it by using coalgebras
Execute provides an execution of the program and the library I mentioned
http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/
used the FFI in order to be able to execute these programs.
There is as well a canonical translation of most IO operations
in Haskell into our setting.
In Haskell an IO operation is given by a function
f : A -> IO B
(sometimes there are several arguments, sometimes there are none)
E.g.
getLine : String -> IO Unit
putStrLine : IO String
)
Each such operations corresponds to having commands
f : A -> C
and response sets
R (f a) = B
So in our data type each of these operations is interpreted as one
atomic command, which then by a function
translateGeneric <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGeneralLib.html#994>
is translated into a native Io program which executes
each command by executing the corresponding haskell program.
See the library consisting of
[TXT] <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOConsoleLib.html> InteractivePrograms.IOConsoleLib.html <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOConsoleLib.html>
[TXT] <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGeneralLib.html> InteractivePrograms.IOGeneralLib.html <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGeneralLib.html>
[TXT] <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGraphicsLib.html> InteractivePrograms.IOGraphicsLib.html <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/InteractivePrograms.IOGraphicsLib.html>
and the 3 examples
IOExampleConsole.html <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleConsole.html>
[TXT] <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleGraphicsDrawingProgram.html> IOExampleGraphicsDrawingProgram.html <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleGraphicsDrawingProgram.html>
[TXT] <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleGraphicsMovingText.html> IOExampleGraphicsMovingText.html <http://www.cs.swan.ac.uk/%7Ecsetzer/software/agda2/IOLib/IOLibVers.0.1/IOExampleGraphicsMovingText.html>
in http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/IOLibVers.0.1/
Anton
>
> On 09/22/2010 02:27 PM, Anton Setzer wrote:
>> On 22/09/10 09:10, Lennart Augustsson wrote:
>>> I think Agda should abandon lazy IO (and thus semi-closed handles).
>>> They are a constant source of nuisance in Haskell and programs using
>>> them can only be explained by assuming that the IO monad gives totally
>>> random results. You can explain them in the same way in Agda, I guess
>>> but it's not pretty.
>>>
>>> (Here's the argument why program₁ and program₂ can behave differently
>>> even if they are equivalent:
>>> Anything happening in the IO monad is random, so running program₁
>>> twice can result if different behaviour.
>>> So even if program₁ ≡ program₂ you can't expect running program₁
>>> necessarily giving the same result as program₂.)
>>>
>>> -- Lennart
>>>
>>
>> I agree that something is broken with the IO as it is in Haskell, it
>> really
>> behaves strangely when using files.
>> I did some research with peter Hancock and came to the solution that
>> an interface of an IO program should be given by a set of commands
>> C and a set of return values to this comment R : C -> Set.
>> Then an IO program can be given by issueing a command
>> to the real world (an element c of type C and depending on the
>> response of the world (an element Rc) issues the next command,
>> or terminates (if one wants a monad) with an element of the return type.
>>
>> This guarantees a strict order between inputs and outputs, namely
>> the program can only issue a response once it has issued a command,
>> and after the response the next command is issued.
>> For file handling one can read the file one piece at a time,
>> and depending it write to a different file. If one wants to get
>> the content of a file as a string, one would need to issue a command
>> which in one go reads the complete file. One can model
>> more sophisticated behaviour, but that needs to be done while
>> interacting
>> with a transparent IO interface.
>>
>> See the articles with Peter hancock on my homepage
>>
>> http://www.cs.swan.ac.uk/~csetzer/
>>
>> and the implementation of a graphics library and a drawing program
>> at
>>
>> http://www-compsci.swan.ac.uk/~csetzer/software/agda2/IOLib/
>>
>> Anton
>>
>>> On Wed, Sep 22, 2010 at 4:30 AM, Alan
>>> Jeffrey<ajeffrey at bell-labs.com> wrote:
>>>
>>>> Hi everyone,
>>>>
>>>> Starting a new thread, since we've stopped talking about FFIs a
>>>> while ago.
>>>> Old thread is here:
>>>>
>>>> http://article.gmane.org/gmane.comp.lang.agda/1936
>>>>
>>>> I kicked the hornets nest and asked why IO is based on Costring
>>>> rather than
>>>> String. It seems to me that the culprit is semi-closed handles in
>>>> Haskell,
>>>> as described here:
>>>>
>>>> http://www.haskell.org/onlinelibrary/io.html#sect21.2.2
>>>>
>>>> "[After a call to hGetContents hdl], hdl is effectively closed, but
>>>> items
>>>> are read from hdl on demand and accumulated in a special list
>>>> returned by
>>>> hGetContents hdl."
>>>>
>>>> AFAICT, this is the underlying source of laziness in the IO
>>>> library, the
>>>> other functions return results strictly, for example there's no
>>>> problem with
>>>> hGetLine having the Agda type (Handle -> IO String) as it waits
>>>> until a NL
>>>> before returning a fully evaluated string.
>>>>
>>>> The discussion around IO and lazy strings made me realize there's a
>>>> question
>>>> as to what the goals for the IO library should be. I will posit an
>>>> innocent-looking goal, and then give a counterexample using the
>>>> current IO
>>>> bindings :-)
>>>>
>>>> GOAL:
>>>> Extensionally equivalent programs have the same runtime behaviour.
>>>>
>>>> Obviously this is an informal goal, as the Haskell runtime system
>>>> isn't
>>>> formalized, but at least we can do experiments. For example, here
>>>> are a
>>>> couple of programs which do not have the same runtime behaviour:
>>>>
>>>> -- This program blocks until it receives input
>>>>
>>>> hello₁ : Costring → IO Unit
>>>> hello₁ [] = putStrLn (fromString "hello")
>>>> hello₁ (x ∷ xs) = putStrLn (fromString "hello")
>>>>
>>>> program₁ : IO Unit
>>>> program₁ = getContents>>= hello₁
>>>>
>>>> -- This program prints immediately
>>>>
>>>> hello₂ : Costring → IO Unit
>>>> hello₂ x = putStrLn (fromString "hello")
>>>>
>>>> program₂ : IO Unit
>>>> program₂ = getContents>>= hello₂
>>>>
>>>> For extensional equivalence, I should probably define a proper
>>>> equivalence
>>>> on IO, which includes the monad laws, but for right now I'll do a
>>>> hack and
>>>> extend propositional equivalence with a postulate expressing
>>>> that>>= is a
>>>> congruence (note, wrt extensional equivalence on the right):
>>>>
>>>> postulate _⟨>>=⟩_ :
>>>> {A B : Set} → {io₁ io₂ : IO A} → {f₁ f₂ : A → IO B} →
>>>> (io₁ ≡ io₂) → (∀ a → f₁ a ≡ f₂ a) →
>>>> (io₁>>= f₁) ≡ (io₂>>= f₂)
>>>>
>>>> Unfortunately, it is easy to show that (program₁ ≡ program₂), thus
>>>> giving a
>>>> counterexample to the goal. (The proof uses the snapshot 2.2.7
>>>> compiler,
>>>> but can probably be munged to go through in 2.2.6).
>>>>
>>>> Possible fixes:
>>>>
>>>> a) Abandon the goal (er, so what's the point of mechanized proof
>>>> then?)
>>>>
>>>> b) Abandon semi-closed handles (ouch, buffering inefficencies!)
>>>>
>>>> c) Er, something really clever I've not thought of.
>>>>
>>>> Thoughts?
>>>>
>>>> A.
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>>
>>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>>
--
---------------------------------------
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/
---------------------------------------
-------------- next part --------------
Skipped content of type multipart/related
More information about the Agda
mailing list