Difference between revisions of "Talk:Open research problems/The I/O quandary"
Jump to navigation
Jump to search
(Selected content relocated to "The I/O quandary") |
(Remaining content relocated to "The I/O quandary") |
||
| Line 1: | Line 1: | ||
| + | There is currently no text in this page. |
||
| − | == Outsourcing the I/O problem == |
||
| + | You can <span style="color:brown;">search for this page title</span> in other pages, |
||
| − | |||
| + | <span style="color:brown;">search the related logs</span>, |
||
| − | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
| + | or <span style="color:brown;">create this page</span>. |
||
| − | '''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 <i>allowing arbitrary |
||
| − | Haskell functions to be imported as axioms.</i> At compile time, these imported |
||
| − | functions have no reduction behaviour, <i>only at run time is the |
||
| − | Haskell function executed</i>. |
||
| − | |||
| − | <tt>[http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf Dependently Typed Programming in Agda], Ulf Norell and James Chapman (<i>emphasis added</i>).</tt> |
||
| − | </div> |
||
| − | |||
| − | In Haskell: |
||
| − | |||
| − | * just extend the FFI enough to replace the ''usually''-abstract I/O definitions with calls to foreign definitions: |
||
| − | :{| |
||
| − | |<haskell> |
||
| − | 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 |
||
| − | ⋮ |
||
| − | </haskell> |
||
| − | |} |
||
| − | |||
| − | * the <code>IO</code> type is then just a type-level tag, as specified in the Haskell 2010 report: |
||
| − | |||
| − | :{| |
||
| − | |<haskell> |
||
| − | data IO a -- that's all folks! |
||
| − | </haskell> |
||
| − | |} |
||
| − | |||
| − | ''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 <code>⊥</code>-up ;-). |
||
| − | |||
| − | By defining them in this way, <code>IO</code> 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. |
||
| − | |||
| − | — [[User:Atravers|Atravers]] Thu Dec 9 01:55:47 UTC 2021 |
||
Latest revision as of 22:12, 15 March 2022
There is currently no text in this page. You can search for this page title in other pages, search the related logs, or create this page.