Difference between revisions of "Output/Input"
(Content relocated to "IO then abstraction") |
(New content) |
||
Line 1: | Line 1: | ||
+ | === <u>Clearing away the smoke and mirrors</u> === |
||
+ | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | There is currently no text in this page. |
||
+ | The implementation in GHC uses the following one: |
||
− | You can <span style="color:brown;">search for this page title</span> in other pages, |
||
+ | |||
− | <span style="color:brown;">search the related logs</span>, |
||
+ | <haskell> |
||
− | or <span style="color:brown;">log in</span> to create this page. |
||
+ | 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 IO
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!
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:
- page 2 of 13 in A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I by Peter Landin:
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
- page 3 of Assignments for Applicative Languages by Vipin Swarup, Uday S. Reddy and Evan Ireland:
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 typeObs 𝜏
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
- MTL style for free by Tom Ellis:
data Time_ a = GetCurrentTime (UTCTime -> a) data Lock_ a = AcquireLock (Maybe Lock -> a) NominalDiffTime Key | RenewLock (Maybe Lock -> a) NominalDiffTime Lock | ReleaseLock (() -> a) Lock
- page 2 of Unique Identifiers in Pure Functional Languages by Péter Diviánszky.
[...] The type
Id
can be hidden by the synonym data type:: Create a :== Id -> a
type Create a = Id -> a
- page 26 of How to Declare an Imperative by Philip Wadler:
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: