Difference between revisions of "Output/Input"
m |
m (Unlinked "IO, partible-style") |
||
(20 intermediate revisions by the same user not shown) | |||
Line 38: | Line 38: | ||
=== <u>Previously seen</u> === |
=== <u>Previously seen</u> === |
||
− | + | 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 95: | Line 112: | ||
type Create a = Id -> a |
type Create a = Id -> a |
||
</haskell> |
</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 100: | 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 108: | 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 143: | Line 203: | ||
|} |
|} |
||
+ | * [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]: |
||
⚫ | 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]. |
||
+ | :{| |
||
+ | |<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> |
||
+ | |} |
||
+ | |||
⚫ | Of these, it is the [https://hackage.haskell.org/package/oi/docs/src/Data-OI-Internal.html#OI 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> === |
=== <code>IO</code><u>, redefined</u> === |
||
− | Based on these and other observations, a reasonable |
+ | Based on these and other observations, a reasonable distillment of these examples would be <code>OI -> a</code>, which then implies: |
<haskell> |
<haskell> |
||
Line 184: | 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 |
+ | 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 203: | 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 218: | 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 224: | 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:
- 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 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)
- An impure lazy programming language, also by Tom Ellis:
data IO a = IO (() -> 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)
- 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
- The Haskell I/O Tutorial by Albert Lai:
But I can already tell you why we cannot follow other languages and use simply
X
or() -> X
.
- Free Monads for Less (Part 3 of 3): Yielding IO by Edward Kmett:
newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor
type Oi a = forall i . i -> 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
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.
- No:
- 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.