Difference between revisions of "Output/Input"
(New content) |
m |
||
(56 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
− | == | + | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
+ | A purely functional program implements a <i>function</i>; it has no side effect. [...] if the side effect can’t be in the functional program, it will have to be outside it. | ||
+ | |||
+ | <tt>[https://web.archive.org/web/20210415200634/https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.9123&rep=rep1&type=pdf Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell], Simon Peyton Jones (pages 3-4 of 60). </tt> | ||
+ | </div> | ||
+ | |||
+ | One technique has been used for similar tasks: | ||
+ | |||
+ | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||
+ | This is discussed by Burton[https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf <span></span>], and is built on by Harrison[https://core.ac.uk/download/9835633.pdf <span></span>]. The effect of this proposal is to place the non-determinism <i>entirely</i> outside the software [...] | ||
+ | |||
+ | <tt>[https://academic.oup.com/comjnl/article-pdf/32/2/162/1445725/320162.pdf Functional Programming and Operating Systems], Simon B. Jones and A. F. Sinclair (page 10 of 13).</tt> | ||
+ | </div> | ||
+ | |||
+ | It can also be used to provide access to external resources: | ||
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> | ||
− | The | + | The approach generalizes so that a program can make use of other run-time information such as the current time or current amount of available storage. |
+ | |||
+ | <tt>[https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages], F. Warren Burton (front page).</tt> | ||
+ | </div> | ||
− | < | + | Perhaps it can be used for I/O... |
− | + | <br> | |
− | </ | + | |
+ | __TOC__ | ||
+ | <sup> <sup> | ||
+ | |||
+ | ---- | ||
+ | === <u>Details, details</u> === | ||
− | + | How does it work? | |
− | < | + | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
+ | [...] supply each program with an extra argument consisting of an infinite (lazy) binary tree of values. (We choose a tree [...] since any number of subtrees may be extracted from an infinite tree). In practice, these values will be determined at run time (when used as arguments to a special function [...]), but once fixed will never change. | ||
</div> | </div> | ||
− | ... | + | ...<i>“a special function”</i>: only one? More will definitely be needed! To keep matters [https://www.interaction-design.org/literature/article/kiss-keep-it-simple-stupid-a-design-principle simple], each value shall only be used <b>once</b> (if at all) as an argument to any such function. |
<haskell> | <haskell> | ||
− | + | main' :: Tree Exterior -> ... | |
− | |||
− | + | -- section 2 | |
+ | data Tree a = Node { contents :: a, | ||
+ | left :: Tree a, | ||
+ | right :: Tree a } | ||
− | + | data Exterior -- the abstract value type | |
− | () - | + | getchar :: Exterior -> Char -- the special functions |
+ | putchar :: Char -> Exterior -> () -- (add more as needed :-) | ||
</haskell> | </haskell> | ||
− | + | Avoiding gratuitous repetition: | |
<haskell> | <haskell> | ||
− | + | type OI = Tree Exterior | |
− | |||
− | + | getChar' :: OI -> Char | |
+ | getChar' = getchar . contents | ||
− | -- | + | putChar' :: Char -> OI -> () |
− | = | + | putChar' c = putchar c . contents |
+ | </haskell> | ||
+ | <sup> </sup> | ||
− | + | ==== An alternative abstraction ==== | |
− | + | About those trees: are they really necessary? If <code>OI</code> was an abstract data type, the use of trees could at least be confined to the implementation: | |
− | |||
− | |||
− | |||
− | |||
− | |||
<haskell> | <haskell> | ||
− | + | data OI | |
+ | getChar' :: OI -> Char | ||
+ | putChar' :: Char -> OI -> () | ||
</haskell> | </haskell> | ||
− | |||
− | + | ...provided that single-use property applies directly to <code>OI</code> values (thereby deeming <i>“special”</i> any function which uses an <code>OI</code> argument). That includes the initial <code>OI</code> value supplied to each program: | |
− | + | ||
− | |||
− | |||
− | |||
− | |||
<haskell> | <haskell> | ||
− | + | main' :: OI -> ... | |
</haskell> | </haskell> | ||
− | |||
− | + | But most Haskell programs will need more: | |
− | |||
<haskell> | <haskell> | ||
− | + | part :: OI -> (OI, OI) | |
+ | part t = (left t, right t) | ||
</haskell> | </haskell> | ||
− | |||
− | + | ...than two <code>OI</code> values: | |
− | |||
<haskell> | <haskell> | ||
− | + | parts :: OI -> [OI] | |
+ | parts t = let (t1, t2) = part t in t1 : parts t2 | ||
+ | </haskell> | ||
− | + | So <code>OI</code> can be a tree-free abstract data type after all: | |
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
<haskell> | <haskell> | ||
− | + | data OI | |
+ | partOI :: OI -> (OI, OI) | ||
+ | getChar :: OI -> Char | ||
+ | putChar :: Char -> OI -> () | ||
</haskell> | </haskell> | ||
− | | | + | <sup> </sup> |
+ | |||
+ | ---- | ||
+ | === <u>Other interfaces</u> === | ||
+ | |||
+ | * [[Monad|monad]] | ||
+ | |||
+ | :<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 | ||
+ | |||
+ | getcharM :: M Char | ||
+ | getcharM = getChar | ||
− | + | putcharM :: Char -> M () | |
− | + | putcharM = putChar | |
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
</haskell> | </haskell> | ||
− | |||
− | * [ | + | * [[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) | ||
+ | |||
+ | getcharC :: C () -> Char | ||
+ | getcharC (u, ()) = getChar u | ||
+ | |||
+ | putcharC :: C Char -> () | ||
+ | putcharC (u, c) = putChar c u | ||
+ | |||
</haskell> | </haskell> | ||
− | |||
− | * [ | + | * [[Arrow|arrow]]: |
− | + | ||
− | + | :<haskell> | |
− | + | type A b c = (OI -> b) -> (OI -> c) | |
− | + | ||
− | + | arr :: (b -> c) -> A b c | |
+ | arr f = \ c' u -> let !x = c' u in f x | ||
+ | |||
+ | 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') | ||
+ | where | ||
+ | unit x u = let !_ = partOI u in x | ||
+ | |||
+ | getcharA :: A () Char | ||
+ | getcharA = \ c' u -> let !(u1, u2) = partOI u in | ||
+ | let !_ = c' u1 in | ||
+ | let !ch = getChar u2 in | ||
+ | ch | ||
− | + | putcharA :: A Char () | |
− | + | putcharA = \ c' u -> let !(u1, u2) = partOI u in | |
− | + | let !ch = c' u1 in | |
− | + | let !z = putChar ch u2 in | |
+ | z | ||
</haskell> | </haskell> | ||
− | |||
− | + | The <code>OI</code> interface can also be used to implement [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf I/O models 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) | |
− | |||
− | + | 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 | |
− | data | + | </haskell> |
− | |||
− | |||
− | + | * continuations: | |
− | |||
− | |||
− | |||
− | + | :<haskell> | |
− | type OI | + | type Answer = OI -> () |
− | + | runK :: Answer -> OI -> () | |
− | + | 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> | ||
− | + | ...and even <i>that</i> <s><i>world</i></s> state-passing style used in GHC, which is also used by [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.935&rep=rep1&type=pdf Clean], [https://staff.science.uva.nl/c.u.grelck/publications/HerhSchoGrelDAMP09.pdf Single-Assignment C] 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> | <haskell> | ||
− | + | newtype World = W OI | |
− | + | ||
− | getChar | + | getcharL :: World -> (Char, World) |
− | + | getcharL (W u) = let !(u1, u2) = partOI u in | |
+ | let !c = getChar u1 in | ||
+ | (c, W u2) | ||
+ | |||
+ | putcharL :: Char -> World -> World | ||
+ | putcharL c (W u) = let !(u1, u2) = partOI u in | ||
+ | let !_ = putChar u1 in | ||
+ | W u2 | ||
</haskell> | </haskell> | ||
<sup> </sup> | <sup> </sup> | ||
---- | ---- | ||
+ | === <u>See also</u> === | ||
− | + | * [[Plainly partible]] | |
+ | * [[Disposing of dismissives]] | ||
+ | * [[IO then abstraction]] | ||
− | + | [[Category:Theoretical foundations]] | |
− | |||
− |
Latest revision as of 19:38, 16 December 2022
A purely functional program implements a function; it has no side effect. [...] if the side effect can’t be in the functional program, it will have to be outside it.
Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, Simon Peyton Jones (pages 3-4 of 60).
One technique has been used for similar tasks:
This is discussed by Burton, and is built on by Harrison. The effect of this proposal is to place the non-determinism entirely outside the software [...]
Functional Programming and Operating Systems, Simon B. Jones and A. F. Sinclair (page 10 of 13).
It can also be used to provide access to external resources:
The approach generalizes so that a program can make use of other run-time information such as the current time or current amount of available storage.
Nondeterminism with Referential Transparency in Functional Programming Languages, F. Warren Burton (front page).
Perhaps it can be used for I/O...
Details, details
How does it work?
[...] supply each program with an extra argument consisting of an infinite (lazy) binary tree of values. (We choose a tree [...] since any number of subtrees may be extracted from an infinite tree). In practice, these values will be determined at run time (when used as arguments to a special function [...]), but once fixed will never change.
...“a special function”: only one? More will definitely be needed! To keep matters simple, each value shall only be used once (if at all) as an argument to any such function.
main' :: Tree Exterior -> ...
-- section 2
data Tree a = Node { contents :: a,
left :: Tree a,
right :: Tree a }
data Exterior -- the abstract value type
getchar :: Exterior -> Char -- the special functions
putchar :: Char -> Exterior -> () -- (add more as needed :-)
Avoiding gratuitous repetition:
type OI = Tree Exterior
getChar' :: OI -> Char
getChar' = getchar . contents
putChar' :: Char -> OI -> ()
putChar' c = putchar c . contents
An alternative abstraction
About those trees: are they really necessary? If OI
was an abstract data type, the use of trees could at least be confined to the implementation:
data OI
getChar' :: OI -> Char
putChar' :: Char -> OI -> ()
...provided that single-use property applies directly to OI
values (thereby deeming “special” any function which uses an OI
argument). That includes the initial OI
value supplied to each program:
main' :: OI -> ...
But most Haskell programs will need more:
part :: OI -> (OI, OI)
part t = (left t, right t)
...than two OI
values:
parts :: OI -> [OI]
parts t = let (t1, t2) = part t in t1 : parts t2
So OI
can be a tree-free abstract data type after all:
data OI
partOI :: OI -> (OI, OI)
getChar :: OI -> Char
putChar :: Char -> OI -> ()
Other interfaces
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 getcharM :: M Char getcharM = getChar putcharM :: Char -> M () putcharM = putChar
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) getcharC :: C () -> Char getcharC (u, ()) = getChar u putcharC :: C Char -> () putcharC (u, c) = putChar c u
type A b c = (OI -> b) -> (OI -> c) arr :: (b -> c) -> A b c arr f = \ c' u -> let !x = c' u in f x 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') where unit x u = let !_ = partOI u in x getcharA :: A () Char getcharA = \ c' u -> let !(u1, u2) = partOI u in let !_ = c' u1 in let !ch = getChar u2 in ch putcharA :: A Char () putcharA = \ c' u -> let !(u1, u2) = partOI u in let !ch = c' u1 in let !z = putChar ch u2 in z
The OI
interface can also be used to implement I/O models used in earlier versions of Haskell:
- dialogues:
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) 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
- continuations:
type Answer = OI -> () runK :: Answer -> OI -> () 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
...and even that world state-passing style used in GHC, which is also used by Clean, Single-Assignment C and as part of the I/O model used for the verification of interactive programs in CakeML, remembering that OI
values can only be used once:
newtype World = W OI
getcharL :: World -> (Char, World)
getcharL (W u) = let !(u1, u2) = partOI u in
let !c = getChar u1 in
(c, W u2)
putcharL :: Char -> World -> World
putcharL c (W u) = let !(u1, u2) = partOI u in
let !_ = putChar u1 in
W u2