Difference between revisions of "Output/Input"
m |
(Quotes reorganised or removed) |
||
Line 1: | Line 1: | ||
[[Category:Theoretical foundations]] |
[[Category:Theoretical foundations]] |
||
− | === <u>Clearing away the smoke and mirrors</u> === |
+ | ==== <u>Clearing away the smoke and mirrors</u> ==== |
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
Line 27: | Line 27: | ||
</haskell> |
</haskell> |
||
+ | ...because <i>"logically"</i> a function in Haskell has no observable effects - being exact requires a change of notation: |
||
− | The result (of type <code>a</code>) can then be returned directly: |
||
<haskell> |
<haskell> |
||
− | () -> a |
+ | () --> (a, ()) |
</haskell> |
</haskell> |
||
+ | The <i>"result"</i> (of type <code>a</code>) can then be <i>"returned"</i> directly: |
||
− | <sub>Why <i>"approximately"</i>? Because <i>"logically"</i> a function in Haskell has no observable effects.</sub> |
||
+ | |||
+ | <haskell> |
||
+ | () --> a |
||
+ | </haskell> |
||
---- |
---- |
||
=== <u>Previously seen</u> === |
=== <u>Previously seen</u> === |
||
− | + | Variants of <code>() --> a</code> have appeared elsewhere - examples include: |
|
* 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: |
* 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: |
||
Line 48: | Line 52: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | (\ () -> …) :: () -> a |
+ | (\ () -> …) :: () --> a |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 61: | Line 65: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | data Job a = JOB (() -> a) |
+ | data Job a = JOB (() --> a) |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 72: | Line 76: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | type Obs tau = State -> tau |
+ | type Obs tau = State --> tau |
</haskell> |
</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) |
||
− | </haskell> |
||
− | |} |
||
− | |||
− | * [http://h2.jaguarpaw.co.uk/posts/impure-lazy-language An impure lazy programming language], also by Tom Ellis: |
||
− | |||
− | :{| |
||
− | <haskell> |
||
− | data IO a = IO (() -> a) |
||
− | </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 7 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.701.930&rep=rep1&type=pdf Functional Reactive Animation] by Conal Elliott and Paul Hudak: |
||
− | :{| |
||
− | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | An early implementation of Fran represented behaviors as implied in the formal semantics: |
||
− | <haskell> |
||
− | data Behavior a = Behavior (Time -> a) |
||
− | </haskell> |
||
− | </div> |
||
|} |
|} |
||
Line 134: | Line 90: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | type Io a = () -> a |
+ | type Io a = () --> a |
− | </haskell> |
||
− | |} |
||
− | |||
− | * The [https://www.vex.net/~trebla/haskell/IO.xhtml Haskell I/O Tutorial] by Albert Lai: |
||
− | :{| |
||
− | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | But I can already tell you why we cannot follow other languages and use simply <code>X</code> or <code>() -> X</code>. |
||
− | </div> |
||
− | |} |
||
− | |||
− | * [http://comonad.com/reader/2011/free-monads-for-less-3 Free Monads for Less (Part 3 of 3): Yielding IO] by Edward Kmett: |
||
− | :{| |
||
− | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | <haskell> |
||
− | newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor |
||
− | </haskell> |
||
− | </div> |
||
− | <sup> </sup> |
||
− | <haskell> |
||
− | type Oi a = forall i . i -> a |
||
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 167: | Line 103: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | class Io a where run :: () -> a |
+ | class Io a where run :: () --> a |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 180: | Line 116: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | data IO t = Action (() -> t) |
+ | data IO t = Action (() --> t) |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 198: | Line 134: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | type T a = () -> a |
+ | type T a = () --> a |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 205: | Line 141: | ||
:{| |
:{| |
||
|<haskell> |
|<haskell> |
||
− | newtype IO a = IO { runIO :: () -> a } |
+ | newtype IO a = IO { runIO :: () --> a } |
</haskell> |
</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> |
||
− | |} |
||
− | |||
− | * [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood/51772273#51772273 chi's answer] to [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood this SO question]: |
||
− | :{| |
||
− | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | As long as we have its special case <code>IO c = () ~> c</code>, we can represent (up to isomorphism) […] <code>a ~> c</code> […] |
||
− | </div> |
||
|} |
|} |
||
Line 233: | Line 155: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | type IO a = (->) Void a |
+ | type IO a = (-->) Void a |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 249: | Line 171: | ||
<haskell> |
<haskell> |
||
class SimpleIO a where |
class SimpleIO a where |
||
− | run :: () -> a |
+ | run :: () --> a |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 263: | Line 185: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | data IO a = IO (() -> a) |
+ | data IO a = IO (() --> a) |
− | __construct :: (() -> a) -> IO a |
+ | __construct :: (() --> a) -> IO a |
__construct = IO |
__construct = IO |
||
</haskell> |
</haskell> |
||
Line 276: | Line 198: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | data IO a = Wrap (() -> a) |
+ | data IO a = Wrap (() --> a) |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 292: | Line 214: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | type IO t = () -> t |
+ | type IO t = () --> t |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 306: | Line 228: | ||
<sup> </sup> |
<sup> </sup> |
||
<haskell> |
<haskell> |
||
− | type Io a = () -> a |
+ | type Io a = () --> a |
</haskell> |
</haskell> |
||
|} |
|} |
||
Line 314: | Line 236: | ||
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
[...] So <code>suspend () -> A</code> offers us the exact same guarantees as <code>IO<A></code>. |
[...] So <code>suspend () -> A</code> offers us the exact same guarantees as <code>IO<A></code>. |
||
+ | </div> |
||
+ | |} |
||
+ | |||
+ | * [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood/51772273#51772273 chi's answer] to [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood this SO question]: |
||
+ | :{| |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | As long as we have its special case <code>IO c = () ~> c</code>, we can represent (up to isomorphism) […] <code>a ~> c</code> […] |
||
+ | </div> |
||
+ | |||
+ | where <code>~></code> is used instead of <code>--></code>. |
||
+ | |} |
||
+ | |||
+ | ==== Avoiding alternate annotations ==== |
||
+ | |||
+ | Having to deal with both <code>-></code> and <code>--></code> is annoying - another option is to use a different argument type, instead of <code>()</code>: |
||
+ | |||
+ | * [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) |
||
+ | </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 7 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.701.930&rep=rep1&type=pdf Functional Reactive Animation] by Conal Elliott and Paul Hudak: |
||
+ | :{| |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | An early implementation of Fran represented behaviors as implied in the formal semantics: |
||
+ | <haskell> |
||
+ | data Behavior a = Behavior (Time -> a) |
||
+ | </haskell> |
||
</div> |
</div> |
||
|} |
|} |
Revision as of 19:53, 24 August 2022
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, ())
...because "logically" a function in Haskell has no observable effects - being exact requires a change of notation:
() --> (a, ())
The "result" (of type a
) can then be "returned" directly:
() --> a
Previously seen
Variants of () --> a
have appeared elsewhere - examples include:
- 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 148 of 168 in Functional programming and Input/Output by Andrew Gordon:
abstype 'a Job = JOB of unit -> 'a
data Job a = JOB (() --> 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 26 of How to Declare an Imperative by Philip Wadler:
The type
'a io
is represented by a function expecting a dummy argument of typeunit
and returning a value of type'a
.type 'a io = unit -> a
type Io a = () --> a
- page 27 of Purely Functional I/O in Scala by Rúnar Bjarnason:
class IO[A](run: () => A)
class Io a where run :: () --> a
type IO<'T> = private | Action of (unit -> 'T)
data IO t = Action (() --> t)
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 }
- Monads, I/O and Concurrency in Lux by Eduardo Julián:
(deftype #export (IO a) (-> Void a))
type IO a = (-->) Void a
- Referentially Transparent Input/Output in Groovy by Mark Perry:
abstract class SimpleIO<A> { abstract A run() }
class SimpleIO a where run :: () --> a
- The
IO
Monad for PHP by Tom Harding:
__construct :: (-> a) -> IO a
[...] The parameter to the constructor must be a zero-parameter [none-adic] function that returns a value.
data IO a = IO (() --> a) __construct :: (() --> a) -> IO a __construct = IO
- The Observable disguised as an IO Monad by Luis Atencio:
IO
is a very simple monad that implements a slightly modified version of our abstract interface with the difference that instead of wrapping a valuea
, it wraps a side effect function() -> a
.data IO a = Wrap (() --> a)
- More Monad:
IO<>
Monad, from dixin's Category Theory via C# series:
The definition of
IO<>
is simple:public delegate T IO<out T>();
[...]
IO<T>
is used to represent a impure function. When aIO<T>
function is applied, it returns aT
value, with side effects.
type IO t = () --> t
So let’s implement the
IO
Monad right now and here. Given that OCaml is strict and that the order of function applications imposes the order of evaluation, theIO
Monad is just a thunk, e.g.,type 'a io = unit -> 'a
type Io a = () --> a
[...] So
suspend () -> A
offers us the exact same guarantees asIO<A>
.
As long as we have its special case
IO c = () ~> c
, we can represent (up to isomorphism) […]a ~> c
[…]where
~>
is used instead of-->
.
Avoiding alternate annotations
Having to deal with both ->
and -->
is annoying - another option is to use a different argument type, instead of ()
:
- 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)
- 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 7 of Functional Reactive Animation by Conal Elliott and Paul Hudak:
An early implementation of Fran represented behaviors as implied in the formal semantics:
data Behavior a = Behavior (Time -> 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 distillment 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 permits 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 -> ()