Difference between revisions of "Output/Input"

From HaskellWiki
Jump to navigation Jump to search
m (Another example added)
m (Unlinked "IO, partible-style")
(17 intermediate revisions by the same user not shown)
Line 38: Line 38:
 
=== <u>Previously seen</u> ===
 
=== <u>Previously seen</u> ===
   
Variations of the type <code>() -> a</code> have appeared elsewhere:
+
The type <code>() -> a</code> (or variations of it) 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 49: Line 49:
 
<haskell>
 
<haskell>
 
(\ () -> …) :: () -> a
 
(\ () -> …) :: () -> a
  +
</haskell>
  +
|}
  +
  +
* page 148 of 168 in [[IO Semantics|Functional programming and Input/Output]] by Andrew Gordon:
  +
:{|
  +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
  +
<pre>
  +
abstype 'a Job = JOB of unit -> 'a
  +
</pre>
  +
</div>
  +
<sup> </sup>
  +
<haskell>
  +
data Job a = JOB (() -> a)
 
</haskell>
 
</haskell>
 
|}
 
|}
Line 76: Line 89:
 
<haskell>
 
<haskell>
 
data Time_ a = GetCurrentTime (UTCTime -> a)
 
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:
data Lock_ a = AcquireLock (Maybe Lock -> a) NominalDiffTime Key
 
  +
| RenewLock (Maybe Lock -> a) NominalDiffTime Lock
 
  +
:{|
| ReleaseLock (() -> a) Lock
 
  +
<haskell>
  +
data IO a = IO (() -> a)
 
</haskell>
 
</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.
+
* 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">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
Line 97: Line 114:
 
|}
 
|}
   
* page 7 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.701.930&rep=rep1&type=pdf Functional Reactive Animation] by Paul Hudak and Conal Elliott:
+
* 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">
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
An early implementation of Fran represented behaviors as implied in the formal semantics:
 
An early implementation of Fran represented behaviors as implied in the formal semantics:
 
<haskell>
 
<haskell>
data Behavior a = Time -> a
+
data Behavior a = Behavior (Time -> a)
 
</haskell>
 
</haskell>
 
</div>
 
</div>
Line 110: Line 127:
 
:{|
 
:{|
 
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
|<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>.
+
The type <code>'a io</code> is represented by a function expecting a dummy argument of type <code>unit</code> and returning a value of type <code>'a</code>.
 
<pre>
 
<pre>
 
type 'a io = unit -> a
 
type 'a io = unit -> a
Line 118: Line 135:
 
<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>
  +
|}
  +
  +
* page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason:
  +
:{|
  +
|<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
  +
<pre>
  +
class IO[A](run: () => A)
  +
</pre>
  +
</div>
  +
<sup> </sup>
  +
<haskell>
  +
class Io a where run :: () -> a
 
</haskell>
 
</haskell>
 
|}
 
|}
Line 151: Line 201:
 
newtype Supply r a = Supply { runSupply :: r -> a }
 
newtype Supply r a = Supply { runSupply :: r -> a }
 
</haskell>
 
</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 194: Line 251:
 
</haskell>
 
</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:
+
Of course, in an actual implementation <code>OI</code> would be abstract like <code>World</code>, and for similar reasons. This permits 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>
 
<haskell>
Line 213: Line 270:
 
::* C isn't "pure" - it allows unrestricted access to observable effects, including those of I/O.
 
::* C isn't "pure" - it allows unrestricted access to observable effects, including those of I/O.
 
::* C isn't "functional" - it was never intended to be [[Referential transparency|referentially transparent]], which severely restricts the ability to use [[Equational reasoning examples|equational reasoning]].
 
::* C isn't "functional" - it was never intended to be [[Referential transparency|referentially transparent]], which severely restricts the ability to use [[Equational reasoning examples|equational reasoning]].
  +
  +
* Is the Haskell language "purely functional"?
  +
  +
::[https://chadaustin.me/2015/09/haskell-is-not-a-purely-functional-language Haskell is not a purely functional language], but is often described as being referentially transparent.
   
 
* Can functional programming be liberated from the von Neumann paradigm?
 
* Can functional programming be liberated from the von Neumann paradigm?
Line 228: Line 289:
 
* Why do our programs need to read input and write output?
 
* Why do our programs need to read input and write output?
   
::Because programs are usually written for [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.628.7053&rep=rep1&type=pdf practical] purposes, such as implementing domain-specific [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.2089&rep=rep1&type=pdf little languages].
+
::Because programs are usually written for [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.628.7053&rep=rep1&type=pdf practical] purposes, such as implementing domain-specific [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.2089&rep=rep1&type=pdf little languages] like [https://dhall-lang.org Dhall].
   
 
----
 
----
Line 234: Line 295:
 
=== <u>See also</u> ===
 
=== <u>See also</u> ===
   
  +
* [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML]
* [[IO, partible-style]]
 
  +
* [[Disposing of dismissives]]
 
* [[IO then abstraction]]
 
* [[IO then abstraction]]
 
* [https://okmij.org/ftp/Computation/IO-monad-history.html The IO monad in 1965]
 
* [https://okmij.org/ftp/Computation/IO-monad-history.html The IO monad in 1965]

Revision as of 12:36, 14 January 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, ())

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

The type () -> a (or variations of it) 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
  • page 15 of Non-Imperative Functional Programming by Nobuo Yamashita:
type a :-> b = OI a -> b
data Time_ a = GetCurrentTime (UTCTime -> a)
data IO a = IO (() -> 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)

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

But I can already tell you why we cannot follow other languages and use simply X or () -> X.

newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor

type Oi a = forall i . i -> a
class IO[A](run: () => A)

class Io a where run :: () -> 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 }

As long as we have its special case IO c = () ~> c, we can represent (up to isomorphism) […] a ~> c […]

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


Various questions

  • Is the C language "purely functional"?
No:
  • C isn't "pure" - it allows unrestricted access to observable effects, including those of I/O.
  • C isn't "functional" - it was never intended to be referentially transparent, which severely restricts the ability to use equational reasoning.
  • Is the Haskell language "purely functional"?
Haskell is not a purely functional language, but is often described as being referentially transparent.
  • Can functional programming be liberated from the von Neumann paradigm?
That remains an open research problem.
  • Can a language be "purely functional" or "denotative"?
Conditionally, yes - the condition being the language is restricted in what domains it can be used in:
  • If a language is free of observable effects, including those of I/O, then the only other place where those effects can reside is within its implementation.
  • There is no bound on the ways in which observable effects can be usefully combined, leading to a similarly-unlimited variety of imperative computations.
  • A finite implementation cannot possibly accommodate all of those computations, so a subset of them must be chosen. This restricts the implementation and language to those domains supported by the chosen computations.
  • Why do our programs need to read input and write output?
Because programs are usually written for practical purposes, such as implementing domain-specific little languages like Dhall.

See also