Difference between revisions of "IO in action"
m |
(Selected content relocated to "Output/Input") |
||
Line 200: | Line 200: | ||
trace msg x = let u = ... in -- how's this going to work? |
trace msg x = let u = ... in -- how's this going to work? |
||
let !_ = putLine msg u in x |
let !_ = putLine msg u in x |
||
− | </haskell> |
||
− | |||
− | == Other interfaces == |
||
− | |||
− | The simplicity of the <code>OI</code>-based interface: |
||
− | |||
− | <haskell> |
||
− | data OI |
||
− | partOI :: (OI -> (OI, OI)) |
||
− | getChar :: (OI -> Char) |
||
− | putChar :: Char -> (OI -> ()) |
||
− | </haskell> |
||
− | |||
− | makes it very adept at implementing other models of I/O: |
||
− | |||
− | * [[Comonad|comonad]]: |
||
− | |||
− | :<haskell> |
||
− | type C a = (OI, a) |
||
− | |||
− | extract :: C a -> a |
||
− | extract (u, x) = let !_ = partOI u in x |
||
− | |||
− | duplicate :: C a -> C (C a) |
||
− | duplicate (u, x) = let !(u1, u2) = partOI u in |
||
− | (u2, (u1, x)) |
||
− | |||
− | extend :: (C a -> b) -> C a -> C b |
||
− | extend h (u, x) = let !(u1, u2) = partOI u in |
||
− | let !y = h (u1, x) in |
||
− | (u2, y) |
||
− | </haskell> |
||
− | |||
− | * [[Arrow|arrow]]: |
||
− | |||
− | :<haskell> |
||
− | type A b c = (OI -> b) -> (OI -> c) |
||
− | |||
− | arr :: (b -> c) -> A b c |
||
− | arr f = \ c' u -> f $! c' u |
||
− | |||
− | both :: A b c -> A b' c' -> A (b, b') (c, c') |
||
− | f' `both` g' = \ c' u -> let !(u1:u2:u3:_) = partsOI u in |
||
− | let !(x, x') = c' u1 in |
||
− | let !y = f' (unit x) u2 in |
||
− | let !y' = g' (unit x') u3 in |
||
− | (y, y') |
||
− | |||
− | |||
− | unit :: a -> OI -> a |
||
− | unit x u = let !_ = partOI u in x |
||
− | |||
− | partsOI :: OI -> [OI] |
||
− | partsOI u = let !(u1, u2) = partOI u in u1 : partsOI u2 |
||
− | </haskell> |
||
− | |||
− | * that [[Monad|other]] interface: |
||
− | |||
− | :<haskell> |
||
− | type M a = OI -> a |
||
− | |||
− | unit :: a -> M a |
||
− | unit x = \ u -> let !_ = partOI u in x |
||
− | |||
− | bind :: M a -> (a -> M b) -> M b |
||
− | bind m k = \ u -> let !(u1, u2) = partOI u in |
||
− | let !x = m u1 in |
||
− | let !y = k x u2 in |
||
− | y |
||
− | </haskell> |
||
− | |||
− | * ...and even the state-passing style used by [https://www.cambridge.org/core/services/aop-cambridge-core/content/view/2EFAEBBE3A19EA03A8D6D75A5348E194/S0956796800001258a.pdf/the-ins-and-outs-of-clean-io.pdf Clean], [https://www.researchgate.net/publication/220997216_Controlling_chaos_on_safe_side-effects_in_data-parallel_operations Single-Assignment C], some Haskell implementations and as part of the I/O model used for the verification of interactive programs in [https://cakeml.org/vstte18.pdf CakeML], remembering that <code>OI</code> values can only be used once: |
||
− | |||
− | :<haskell> |
||
− | newtype W = W OI |
||
− | |||
− | readchar :: W -> (Char, W) |
||
− | readchar (W u) = let !(u1, u2) = partOI u in |
||
− | let !c = getChar u1 in |
||
− | (c, W u2) |
||
− | |||
− | writechar :: Char -> W -> W |
||
− | writechar c (W u) = let !(u1, u2) = partOI u in |
||
− | let !_ = putChar u1 in |
||
− | W u2 |
||
− | </haskell> |
||
− | |||
− | It can also be used to implement the models of [https://dl.acm.org/doi/pdf/10.1145/262009.262011 I/O used in earlier versions] of Haskell: |
||
− | |||
− | * dialogues: |
||
− | |||
− | :<haskell> |
||
− | runD :: ([Response] -> [Request]) -> OI -> () |
||
− | runD d u = foldr (\(!_) -> id) () $ yet $ \ l -> zipWith respond (d l) (partsOI u) |
||
− | |||
− | yet :: (a -> a) -> a |
||
− | yet f = f (yet f) |
||
− | |||
− | partsOI :: OI -> [OI] |
||
− | partsOI u = let !(u1, u2) = partOI u in u1 : partsOI u2 |
||
− | |||
− | respond :: Request -> OI -> Response |
||
− | respond Getq u = let !c = getChar u in Getp c |
||
− | respond (Putq c) u = let !_ = putChar c u in Putp |
||
− | |||
− | data Request = Getq | Putq Char |
||
− | data Response = Getp Char | Putp |
||
− | </haskell> |
||
− | |||
− | * continuations: |
||
− | |||
− | :<haskell> |
||
− | type Answer = OI -> () |
||
− | |||
− | runK :: Answer -> IO -> () |
||
− | runK a u = a u |
||
− | |||
− | doneK :: Answer |
||
− | doneK = \ u -> let !_ = partOI u in () |
||
− | |||
− | getcharK :: (Char -> Answer) -> Answer |
||
− | getcharK k = \ u -> let !(u1, u2) = partOI u in |
||
− | let !c = getChar u1 in |
||
− | let !a = k c in |
||
− | a u2 |
||
− | |||
− | putcharK :: Char -> Answer -> Answer |
||
− | putcharK c a = \ u -> let !(u1, u2) = partOI u in |
||
− | let !_ = putChar c u1 in |
||
− | a u2 |
||
</haskell> |
</haskell> |
||
Revision as of 20:18, 24 August 2022
The IO
type serves as a tag for operations (actions) that interact with the outside world. [...]
The Haskell 2010 Report (page 95 of 329).
So what are I/O actions?
A false start
Unlike most other programming languages, Haskell's non-strict semantics and thus its focus on referential transparency means the common approach to I/O won't work. Even if there was some way to actually introduce it:
# cat NoDirectIO.hs
module NoDirectIO where
foreign import ccall unsafe "c_getchar" getchar :: () -> Char
foreign import ccall unsafe "c_putchar" putchar :: Char -> ()
#
# ghci NoDirectIO.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling NoDirectIO ( NoDirectIO.hs, interpreted )
NoDirectIO.hs:3:1: error:
• Unacceptable argument type in foreign declaration:
‘()’ cannot be marshalled in a foreign call
• When checking declaration:
foreign import ccall unsafe "c_getchar" getchar :: () -> Char
|
3 | foreign import ccall unsafe "c_getchar" getchar :: () -> Char
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
ghci> :q
Leaving GHCi.
#
...such entities (because they are certainly not regular Haskell functions!) are practically useless. For example, what should the output of this be in Haskell?
let
f x y = g y x
g x y = h y y
h x y = "what?"
in f (putstr "hello ") (putstr "world\n")
(That's just one of the counter-examples from section 3.1 (page 43 of 210) in Claus Reinke's Functions, Frames and Interactions!)
For a language like Haskell, there are two options:
- avoid I/O altogether and be denotative;
- use existing language features to build a framework and adapt I/O-centric entities to work within it: a model of I/O.
Actions and functions
In Haskell, functions have their basis in mathematics, not subroutines. It requires all functions to obey this essential rule:
- if a function's result changes, it is only because it's arguments have changed.
So if getchar
and putchar
were applied to a different value at each call site, they could be used like functions:
foreign import ccall unsafe "c_getchar" getchar :: ... -> Char
foreign import ccall unsafe "c_putchar" putchar :: Char -> ... -> ()
These curious values need types:
- the requirement for different values is now extended to avoid having two different types - each value can only be used as an argument once:
let u = ... in let !c1 = getchar u in -- invalid: let !c2 = getchar u in -- reusing u in [c1, c2]
let [c1, c2] = ... in let u = ... in let !_ = putchar c1 u in -- invalid let !_ = putchar c2 u in -- too in ()
let u = ... in let !c = getchar u in -- invalid let !_ = putchar c u in -- again in ()
- This extended requirement will also apply to any other
OI
-based entities, primitive or otherwise.
- since outside interactions are involved, let's keep it simple:
data OI -- abstract getChar :: OI -> Char putChar :: Char -> OI -> ()
Having previously referred to them as "entities", these new type signatures make for more useful descriptions:
⋮
getChar :: (OI -> Char) -- this is an I/O action
putChar :: Char -> (OI -> ()) -- this resembles a function returning an I/O action
An example in action
Since the origin of OI
values are unspecified, let's start with some pseudo-code:
getLine :: (OI -> [Char]) -- another I/O action
putLine :: [Char] -> (OI -> ()) -- also resembles a function returning an I/O action
getLine u = let !c = getChar ... in
if c == '\n' then
[]
else
let !cs = getLine ...
in c:cs
putLine (c:cs) u = let !_ = putChar c ... in putLine cs ...
putLine [] u = putChar '\n' ...
Because OI
values can only be used once:
⋮
getLine u = let (u1, u2) = ... in
let !c = getChar u1 in
if c == '\n' then
[]
else
let !cs = getLine u2
in c:cs
putLine (c:cs) u = let (u1, u2) = ... in
let !_ = putChar c u1 in
putLine cs u2
putLine [] u = putChar '\n' u
Those new local bindings u1
and u2
in getLine
must be defined somehow, and there's only one parameter available:
⋮
getLine u = let (u1, u2) = ... u ... in
let !c = getChar u1 in
if c == '\n' then
[]
else
let !cs = getLine u2
in c:cs
⋮
Now for an extra abstraction in the form of another primitive, to complete the new local bindings:
⋮
partOI :: (OI -> (OI, OI)) -- also an I/O action
getLine u = let (u1, u2) = partOI u in
let !c = getChar u1 in
if c == '\n' then
[]
else
let !cs = getLine u2
in c:cs
putLine (c:cs) u = let (u1, u2) = partOI u in
let !_ = putChar c u1 in
putLine cs u2
putLine [] u = putChar '\n' u
Noticing the tree-like way in which the various local OI
values are being defined and used:
- suggests the existence of a single ancestral
OI
value in the entire program:
main :: (OI -> ()) -- a program is an I/O action
- and clearly shows that the only
safe
way to use an I/O action is from within the definition of another I/O action:
trace :: [Char] -> a -> a trace msg x = let u = ... in -- how's this going to work? let !_ = putLine msg u in x
Further reading
- Output/Input goes into more detail about the type
OI -> a
.
- For those who prefer it, John Launchbury and Simon Peyton Jones's State in Haskell explains the state-passing approach currently in widespread use.