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

[Alan Jeffrey]

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.
-------------- next part --------------
open import IO.Primitive
open import Data.Char
open import Relation.Binary.PropositionalEquality
open import Foreign.Haskell

module IOvsEquiv where 

Costring = Colist Char

-- Cheating for now and making extensionality of >>= an axiom.
-- Should we use a separate extensional equivalence for IO?

postulate _⟨>>=⟩_ : {A B : Set} → {io₁ io₂ : IO A} → {f₁ f₂ : A → IO B} → (io₁ ≡ io₂) → (∀ a → f₁ a ≡ f₂ a) → (io₁ >>= f₁) ≡ (io₂ >>= f₂)

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

-- Testy!

main = program₁
-- main = program₂

-- Proofy! (Checked w/ Agda 2.2.7)

ohdear : program₁ ≡ program₂
ohdear = refl ⟨>>=⟩ lemma where
  lemma : ∀ a → hello₁ a ≡ hello₂ a
  lemma [] = refl
  lemma (x ∷ xs) = refl

-- So we have two programs with quite different behaviour,
-- but which have been proved extensionally equivalent.
-- Oh dear.