Difference between revisions of "Output/Input"

From HaskellWiki
Jump to: navigation, search
(Content relocated to "IO then abstraction")
(New content)
Line 1: Line 1:
 +
=== <u>Clearing away the smoke and mirrors</u> ===
  
There is currently no text in this page.
+
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
You can <span style="color:brown;">search for this page title</span> in other pages,
+
The implementation in GHC uses the following one:
<span style="color:brown;">search the related logs</span>,
+
 
or <span style="color:brown;">log in</span> to create this page.
+
<haskell>
 +
type IO a  =  World -> (a, World)
 +
</haskell>
 +
 
 +
An <code>IO</code>computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value. Of course, GHC does not actually pass the world around; instead, it passes a dummy “token,” to ensure proper sequencing of actions in the presence of lazy evaluation, and performs input and output as actual side effects!
 +
 
 +
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.168.4008&rep=rep1&type=pdf A History of Haskell: Being Lazy With Class], Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.</tt>
 +
</div>
 +
 
 +
...so what starts out as an I/O action of type:
 +
 
 +
<haskell>
 +
World -> (a, World)
 +
</haskell>
 +
 
 +
is changed by GHC to approximately:
 +
 
 +
<haskell>
 +
() -> (a, ())
 +
</haskell>
 +
 
 +
As the returned unit-value <code>()</code> contains no useful information, that type can be simplified further:
 +
 
 +
<haskell>
 +
() -> a
 +
</haskell>
 +
 
 +
Why "approximately"? Because "logically" a function in Haskell has no observable effects.
 +
 
 +
----
 +
=== <u>Previously seen</u> ===
 +
 
 +
Variations of the type <code>() -> a</code> have appeared elsewhere:
 +
 
 +
* page 2 of 13 in [https://fi.ort.edu.uy/innovaportal/file/20124/1/22-landin_correspondence-between-algol-60-and-churchs-lambda-notation.pdf A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I] by Peter Landin:
 +
:{|
 +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
 
 +
The use of <code>λ</code>, and in particular (to avoid an irrelevant bound variable) of <code>λ()</code> , to delay and possibly avoid evaluation is exploited repeatedly in our model of ALGOL 60. A function that requires an argument-list of length zero is called a ''none-adic'' function.
 +
</div>
 +
<sup> </sup>
 +
<haskell>
 +
(\ () -> …) :: () -> a
 +
</haskell>
 +
|}
 +
 
 +
* page 3 of [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf Assignments for Applicative Languages] by Vipin Swarup, Uday S. Reddy and Evan Ireland:
 +
:{|
 +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
A value of type <code>Obs 𝜏</code> is called an ''observer''.  Such a value observes (i.e. views or inspects) a state and returns a value of type <code>𝜏</code>. [...] An observer type <code>Obs 𝜏</code> may be viewed as an implicit function space from the set of states to the type <code>𝜏</code>.
 +
</div>
 +
<sup> </sup>
 +
<haskell>
 +
type Obs tau = State -> tau
 +
</haskell>
 +
|}
 +
 
 +
* [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming] by Nobuo Yamashita:
 +
 
 +
:{|
 +
<haskell>
 +
type a :-> b = OI a -> b
 +
</haskell>
 +
|}
 +
 
 +
* [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis:
 +
 
 +
:{|
 +
<haskell>
 +
data Time_ a = GetCurrentTime (UTCTime -> a)
 +
 
 +
data Lock_ a = AcquireLock (Maybe Lock -> a) NominalDiffTime Key
 +
            | RenewLock (Maybe Lock -> a) NominalDiffTime Lock
 +
            | ReleaseLock (() -> a) Lock
 +
</haskell>
 +
|}
 +
 
 +
* page 2 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.128.9269&rep=rep1&type=pdf Unique Identifiers in Pure Functional Languages] by Péter Diviánszky.
 +
:{|
 +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
[...] The type <code>Id</code> can be hidden by the synonym data type
 +
<pre>
 +
:: Create a  :==  Id -> a
 +
</pre>
 +
</div>
 +
<sup> </sup>
 +
<haskell>
 +
type Create a = Id -> a
 +
</haskell>
 +
|}
 +
 
 +
* page 26 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative] by Philip Wadler:
 +
:{|
 +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
The type <code>'a io</code> is represented by a function expecting a dummy argument of type unit and returning a value of type <code>'a</code>.
 +
<pre>
 +
type 'a io = unit -> a
 +
</pre>
 +
</div>
 +
<sup> </sup>
 +
<haskell>
 +
type Io a = () -> a
 +
</haskell>
 +
|}
 +
 
 +
* [https://stackoverflow.com/questions/6647852/haskell-actual-io-monad-implementation-in-different-language/6706442#6706442 ysdx's answer] to [https://stackoverflow.com/questions/6647852/haskell-actual-io-monad-implementation-in-different-language this SO question]:
 +
:{|
 +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 +
Let's say you want to implement <code>IO</code> in SML :
 +
<pre>
 +
structure Io : MONAD =
 +
struct
 +
  type 'a t = unit -> 'a
 +
        ⋮
 +
end
 +
</pre>
 +
</div>
 +
<sup> </sup>
 +
<haskell>
 +
type T a = () -> a
 +
</haskell>
 +
|}
 +
 
 +
* [https://stackoverflow.com/questions/45136398/is-the-monadic-io-construct-in-haskell-just-a-convention/45141523#45141523 luqui's answer] to [https://stackoverflow.com/questions/45136398/is-the-monadic-io-construct-in-haskell-just-a-convention this SO question]:
 +
:{|
 +
|<haskell>
 +
newtype IO a = IO { runIO :: () -> a }
 +
</haskell>
 +
|}
 +
 
 +
* [https://stackoverflow.com/questions/15418075/the-reader-monad/15419592#15419592 luqui's answer] to [https://stackoverflow.com/questions/15418075/the-reader-monad this SO question]:
 +
:{|
 +
|<haskell>
 +
newtype Supply r a = Supply { runSupply :: r -> a }
 +
</haskell>
 +
|}
 +
 
 +
Of these, it is the implementation of <code>OI a</code> in Yamashita's [https://hackage.haskell.org/package/oi oi] package which is most interesting as its values are ''monousal'' - once used, their contents remain constant. This single-use property also appears in the implementation of the abstract <code>decision</code> type described by F. Warren Burton in [https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages].
 +
 
 +
----
 +
=== <code>IO</code><u>, redefined</u> ===
 +
 
 +
Based on these and other observations, a reasonable generalisation of these examples would be <code>OI -> a</code>, which then implies:
 +
 
 +
<haskell>
 +
type IO a = OI -> a
 +
</haskell>
 +
 
 +
Using Burton's ''pseudodata'' approach:
 +
 
 +
<haskell>
 +
-- abstract; single-use I/O-access mediator
 +
data Exterior
 +
getchar :: Exterior -> Char
 +
putchar :: Char -> Exterior -> ()
 +
 
 +
-- from section 2 of Burton's paper
 +
data Tree a = Node { contents :: a,
 +
                    left    :: Tree a,
 +
                    right    :: Tree a }
 +
 
 +
-- utility definitions
 +
type OI  =  Tree Exterior
 +
 
 +
getChar' :: OI -> Char
 +
getChar' =  getchar . contents
 +
 
 +
putChar' :: Char -> OI -> ()
 +
putChar' c = putchar c . contents
 +
 
 +
part    :: OI -> (OI, OI)
 +
parts    :: OI -> [OI]
 +
 
 +
part t  =  (left t, right t)
 +
parts t  =  let !(t1, t2) = part t in
 +
            t1 : parts t2
 +
</haskell>
 +
 
 +
Of course, in an actual implementation <code>OI</code> would be abstract like <code>World</code>, and for similar reasons. This allows for a simpler implementation for <code>OI</code> and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the <code>OI</code> interface, in this case:
 +
 
 +
<haskell>
 +
data OI
 +
part :: OI -> (OI, OI)
 +
getChar' :: OI -> Char
 +
putChar' :: Char -> OI -> ()
 +
</haskell>
 +
<sup> </sup>
 +
 
 +
----
 +
 
 +
See also:
 +
 
 +
* [[IO, partible-style]]
 +
* [[IO then abstraction]]
 +
* [[Open research problems]]

Revision as of 13:52, 2 November 2021

Clearing away the smoke and mirrors

The implementation in GHC uses the following one:

type IO a  =  World -> (a, World)

An IOcomputation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value. Of course, GHC does not actually pass the world around; instead, it passes a dummy “token,” to ensure proper sequencing of actions in the presence of lazy evaluation, and performs input and output as actual side effects!

A History of Haskell: Being Lazy With Class, Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.

...so what starts out as an I/O action of type:

World -> (a, World)

is changed by GHC to approximately:

() -> (a, ())

As the returned unit-value () contains no useful information, that type can be simplified further:

() -> a

Why "approximately"? Because "logically" a function in Haskell has no observable effects.


Previously seen

Variations of the type () -> a have appeared elsewhere:

The use of λ, and in particular (to avoid an irrelevant bound variable) of λ() , to delay and possibly avoid evaluation is exploited repeatedly in our model of ALGOL 60. A function that requires an argument-list of length zero is called a none-adic function.

(\ () -> ) :: () -> a

A value of type Obs 𝜏 is called an observer. Such a value observes (i.e. views or inspects) a state and returns a value of type 𝜏. [...] An observer type Obs 𝜏 may be viewed as an implicit function space from the set of states to the type 𝜏.

type Obs tau = State -> tau
  • page 15 of Non-Imperative Functional Programming] by Nobuo Yamashita:
type a :-> b = OI a -> b
data Time_ a = GetCurrentTime (UTCTime -> a)

data Lock_ a = AcquireLock (Maybe Lock -> a) NominalDiffTime Key
             | RenewLock (Maybe Lock -> a) NominalDiffTime Lock
             | ReleaseLock (() -> a) Lock

[...] The type Id can be hidden by the synonym data type

:: Create a  :==  Id -> a

type Create a = Id -> a

The type 'a io is represented by a function expecting a dummy argument of type unit and returning a value of type 'a.

type 'a io = unit -> a

type Io a = () -> a

Let's say you want to implement IO in SML :

structure Io : MONAD =
struct
  type 'a t = unit -> 'a
         ⋮
end

type T a = () -> a
newtype IO a = IO { runIO :: () -> a }
newtype Supply r a = Supply { runSupply :: r -> a }

Of these, it is the implementation of OI a in Yamashita's oi package which is most interesting as its values are monousal - once used, their contents remain constant. This single-use property also appears in the implementation of the abstract decision type described by F. Warren Burton in Nondeterminism with Referential Transparency in Functional Programming Languages.


IO, redefined

Based on these and other observations, a reasonable generalisation of these examples would be OI -> a, which then implies:

type IO a = OI -> a

Using Burton's pseudodata approach:

 -- abstract; single-use I/O-access mediator
data Exterior
getchar :: Exterior -> Char
putchar :: Char -> Exterior -> ()

 -- from section 2 of Burton's paper
data Tree a = Node { contents :: a,
                     left     :: Tree a,
                     right    :: Tree a }

 -- utility definitions
type OI  =  Tree Exterior

getChar' :: OI -> Char
getChar' =  getchar . contents

putChar' :: Char -> OI -> ()
putChar' c = putchar c . contents

part     :: OI -> (OI, OI)
parts    :: OI -> [OI]

part t   =  (left t, right t)
parts t  =  let !(t1, t2) = part t in
            t1 : parts t2

Of course, in an actual implementation OI would be abstract like World, and for similar reasons. This allows for a simpler implementation for OI and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the OI interface, in this case:

data OI
part :: OI -> (OI, OI)
getChar' :: OI -> Char
putChar' :: Char -> OI -> ()


See also: