Difference between revisions of "Output/Input"

From HaskellWiki
Jump to navigation Jump to search
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> ===
   
The type <code>() -> a</code> (or variations of it) have appeared elsewhere - examples include:
+
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:

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
abstype 'a Job = JOB of unit -> 'a

data Job a = JOB (() --> 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

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
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 }
(deftype #export (IO a)
  (-> Void a))

type IO a = (-->) Void a
abstract class SimpleIO<A> {
    abstract A run()
}

class SimpleIO a where
    run :: () --> a
__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

IO is a very simple monad that implements a slightly modified version of our abstract interface with the difference that instead of wrapping a value a, it wraps a side effect function () -> a.

data IO a = Wrap (() --> a)

The definition of IO<> is simple:

public delegate T IO<out T>();

[...]

  • IO<T> is used to represent a impure function. When a IO<T> function is applied, it returns a T 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, the IO 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 as IO<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
data Time_ a = GetCurrentTime (UTCTime -> a)

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

:: Create a  :==  Id -> a

type Create a = Id -> a

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 -> ()


See also