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.