Talk:Open research problems/The I/O quandary

Outsourcing the I/O problem

4 Compiling Agda programs

This section deals with the topic of getting Agda programs to interact with the real world. Type checking Agda programs requires evaluating arbitrary terms, ans as long as all terms are pure and normalizing this is not a problem, but what happens when we introduce side effects? Clearly, we don't want side effects to happen at compile time. Another question is what primitives the language should provide for constructing side effecing programs. In Agda, these problems are solved by allowing arbitrary Haskell functions to be imported as axioms. At compile time, these imported functions have no reduction behaviour, only at run time is the Haskell function executed.

Dependently Typed Programming in Agda, Ulf Norell and James Chapman (emphasis added).

In Haskell:

• just extend the FFI enough to replace the usually-abstract I/O definitions with calls to foreign definitions:

instance Monad IO where return = unitIO (>>=) = bindIO foreign import ccall "primUnitIO" unitIO :: a -> IO a foreign import ccall "primBindIO" bindIO :: IO a -> (a -> IO b) -> IO b ⋮

• the IO type is then just a type-level tag, as specified in the Haskell 2010 report:

data IO a -- that's all folks!

Voilà! In this example, the I/O problem has been outsourced to C - if you're not happy with C's solution to the I/O problem, just use another programming language for the Haskell implementation: there's plenty of them to choose from (...but don't use Haskell, to avoid going ⊥-up ;-).

By defining them in this way, IO and its actions in Haskell can also be thought of as being "axiomatic": they have no effect when a Haskell program is compiled, only at run time is the foreign definition executed and its effects occur.

— Atravers Thu Dec 9 01:55:47 UTC 2021