Confusion about analogy's of purity in Haskell

purity-haskell-freenode

[18:27] <trumanshow19> Would someone mind help iron out the
inconsistencies in my head with respect to purity in
Haskell. Statement 1: Haskell is a purely functional lanugage, S2:
Haskell is not impure, but... S3: f :: a -> a is a "pure" function as
opposed to a -> IO a.

[18:27] <trumanshow19> If a -> is pure, to distinguish a -> IO a, then
how do I describe the latter, is there is no impurity in Haskell ?

[18:28] <trumanshow19> The only opposite of pure I know is impure.

[18:28] <geekosaur> trumanshow19, IO is a bit of a trick. anything you
write in IO is actually entirely pure: you are actually writing in
Haskell a program that emits IO "opcodes" which are run by the
runtime, which is impure.

[18:28] <aweinstock> (f :: a -> IO a) is a pure function that returns
an IO action (which can be executed impurely)

[18:28] <lambdabot> shachaf says: getLine :: IO String contains a
String in the same way that /bin/ls contains a list of files

[18:28] <geekosaur> that is, "getLine" is not a function which reads a
line, it is a variable containing an opcode that the runtime
interprets to mean "read a line".

[18:28] <ski> trumanshow19 : all functions in Haskell are "pure"

[18:29] <geekosaur> the main function's result is an IO action, or a
chain of these opcodes connected by >>=

[18:29] <geekosaur> which the runtime can then run

[18:29] <trumanshow19> geekosaur: thanks. But that's true of *any*
language. The `getLine` equivalent in Java doesn't get a line when I
write the Java, it's run when I run the executed impure bytecode.

[18:30] <Philonous> trumanshow19, The heart of the issue is that IO
values are just values like any other and they can be returned from a
function, IO values represent programs that, when executed, can have
"impure" effects. You can't execute them from within haskell, though

[18:30] <bennofs> trumanshow19: well, in most languages, IO a would be
represented as a function without any arguments

[18:30] <trumanshow19> ski: this is what is confusing. People often
say: a -> a is pure, by which they mean there is no "IO" before the
last a.

[18:30] <trumanshow19> So if a -> is pure, what is a -> IO a ?

[18:30] <geekosaur> think of a program that outputs a program

[18:30] <bennofs> > const 3 getLine

[18:30] <lambdabot>  3

[18:30] <geekosaur> your Java writes a JavaScript program that, when
run, does the IO

[18:31] <trumanshow19> I very often see this kind of definition, in
the widely used Haskell books and online material.

[18:31] <geekosaur> *that* is the analogy in effect here

[18:31] <ski> trumanshow19 : you can't embed I/O actions inside
e.g. an expression of type `Integer'. that is the most visible
difference with Java here

[18:31] <ski> trumanshow19 : "People often say: a -> a is pure, by
which they mean there is no "IO" before the last a." -- yes. and it's
bad terminology to say so

[18:32] <bennofs> trumanshow19: yeah, and there is a clear separation
between "constructing" an IO value and actually executing the IO

[18:32] <trumanshow19> "ski: yes. and it's bad terminology to say so"
... Learn you a Haskell, Real World Haskell,.... they all use this "a
-> a" is pure distinction in their descriptions.

[18:32] <ReinH> trumanshow19: And yet it's still bad.

[18:33] <aweinstock> is it possible to get an offline copy of the
database that lambdabot uses for @quote?

[18:33] <bennofs> trumanshow19: and yet... it doesn't matter so much,
as long as you understand how it is meant

[18:33] * ski thinks it confuses newbies

[18:34] <tommd> I like saying it is "deterministic" or a "function",
though some people have different opionions on what constitutes a
"function".

[18:34] <ski> `putStr' is clearly a function (returning a monadic
action)

[18:34] <ski> @type putStr

[18:34] <lambdabot> String -> IO ()

[18:35] <tommd> ski: Are you sure that's always true?

[18:35] <bennofs> ski: is there any other word for a thing of type a
-> IO b that you'd recommend, instead of "impure function"?

[18:35] <ski> tommd : yes

[18:35] <trumanshow19> Learn you a Haskell: " And if we're taking data
out of an I/O action, we can only take it out when we're inside
another I/O action. This is how Haskell manages to neatly separate the
pure and impure parts of our code."

[18:35] <trumanshow19> http://learnyouahaskell.com/input-and-output

[18:35] <ReinH> The definition of function is pretty clear: a type
whose outermost constructor is (->).

[18:35] <tommd> ski: Does HaLVM (or any other compiler) not through an
exception?  Does the language require no exception can be thrown?

[18:35] <ReinH> trumanshow19: Yes, LYAH is not a paragon of accuracy

[18:35] <ski> bennofs : you could possibly say "monadic function" or
maybe "Kleisli function" to mean a function which returns a monadic
action

[18:36] <Philonous> LYAH seems to be preoccupied with cutesy analogies
and pretty pictures rather than rigorous

[18:36] <Philonous> being*

[18:36] <trumanshow19> Real World Haskell: "In Haskell, the default is
for functions to not have side effects: the result of a function
depends only on the inputs that we explicitly provide. We call these
functions pure; functions with side effects are impure."

[18:36] <trumanshow19>
http://book.realworldhaskell.org/read/types-and-functions.html

[18:36] <ReinH> trumanshow19: I know they say this.

[18:36] <ReinH> It's still wrong.

[18:36] <tommd> ski: Ah, unapplied, as in 'putStr' as a
value.  Nevermind.

[18:36] <ReinH> it's a convenient fiction

[18:36] <ski> tommd : `putStr' will return the same action (an equal
action) every time you call it with the same (an equal) string
argument

[18:36] <Philonous> It's not even convenient, really.

[18:37] <ski> it's a point-of-view

[18:37] <ReinH> ski: that's just like your opinion man

[18:37] <ski> what matters is how we can reason about it, at the level
of the language

[18:37] <ski> ReinH : which ?

[18:38] <trumanshow19> It isn't too surprising, then, when the
declaration that Haskell is a purely FP language is met with confusion
when the pillars of Haskell teaching use imprecise analogy for pure vs
impure.

[18:38] <ReinH> ski: I was just going off of "it's a point of view"

[18:38] <tommd> ski: I'm sure I can construct a situation where that
isn't true.  () /= _|_

[18:38] <ReinH> trumanshow19: I wouldn't call either of those "pillars
of Haskell teaching"

[18:38] <ReinH> not by a long shot

[18:38] <tommd> ski: Am I missing your point?

[18:38] <bennofs> Well, you could argue that since you can't really do
anything at all with IO actions other than forcing them or putting
them in another IO action so they're executed, the function itself is
still impure since you cannot get the result without performing impure
actions

[18:39] <Philonous> trumanshow19, You're not the first to notice
this. Unfortunately, those sources aren't going to go away

[18:39] <ReinH> bennofs: not really

[18:39] <ski> ReinH : i mean that if we're talking about the POV of
implementing Haskell, then implementations typically use
update-in-place of memory and registers. e.g. if compiling via C, then
it would probably use impure constructions in C. however, this in no
way affects the purity of the language itself

[18:39] <ReinH> It's pretty simple: evaluation of IO actions is pure.

[18:39] <ReinH> ski: Sure, and underlying it all is mutations of
registers, so Haskell can't be pure, QED

[18:40] <ski> ReinH : by "POV" i mean that whether it's pure or not
depends from which language level you're viewing it. it's not
absolute. it's relative to the language you're reasoning inside

[18:40] <ski> ReinH : therefore, it *is* pure, from the POV of the
Haskell language

[18:40] <ReinH> Evaluation of haskell is observably pure.

[18:40] <ski> tommd : elaborate on what you mean ?

[18:41] <bennofs> ReinH: I still wouldn't call getLine a "pure
function", simply because you cannot use it in any meaningful way if
you're not perfoming the impure part of it. The main functionality of
it is impure, no matter if techniqually, you can already get the "IO"
action without executing it

[18:41] <ReinH> bennofs: I wouldn't call getLine a function.

[18:41] <ReinH> Because it isn't.

[18:41] <ski> (well, `getLine' is simply not a function at all)

[18:41] <bennofs> oops, sorry. substitute getLine with putStrLn

[18:41] <ReinH> The main functionality of getLine is to be a value
that represents an IO action

[18:41] <ReinH> bennofs: putStrLn is a pure function that returns an
IO action, as mentioned

[18:42] <ReinH> Again: evaluation of IO values is pure

[18:42] <ReinH> Execution is not, but no one expects execution to be
pure

[18:42] <ReinH> indeed, it can't be pure if you want to actually do
anything

[18:43] <trumanshow19> ReinH: are you getting about evaluation as a
distinction of execution for the fact that Haskell evaluation is lazy?

[18:43] <Philonous> bennofs, You can store the result in a
datastructure and use it later, at which point the association between
"putStrLn" and the action is lost.

[18:43] <ReinH> trumanshow19: no, simply for the fact that they are
different things

[18:43] <trumanshow19> That is to say: it would be impossible to
implement a strict purely functional programming language that has
getLine and putStrLn ?

[18:43] <bennofs> trumanshow19: no

[18:43] <ReinH> It has nothing to do with laziness

[18:43] <bennofs> trumanshow19: the point of IO actions is that you
can build IO actions without performing there effects

[18:44] <bennofs> trumanshow19: building the actions is
pure. Perfoming their effects (= executing them) (this is what the
Haskell runtime does) is not

[18:44] <ski> bennofs : you can refactor `do _ <- putStrLn "foo"; _ <-
putStrLn "foo"' into `do let {act = putStrLn "foo"}; _ <- act; _ <-
act' in Haskell. you can't refactor `{ puts("foo"); puts("foo"); }'
into `{ int act = puts("foo"); (void)act; (void)act; }' in C

[18:44] <nshepperd> putStrLn is actually more powerful than the
equivalent impure C function, in that you can bundle up 'putStrLn
"hello"' as a value, put it into a list, pass it to a function to be
executed later, etc etc

[18:45] <trumanshow19> By building you mean tying into a text editor?
I.e. getLine >>= putStrLn  :: IO ()  ?

[18:45] <ReinH> trumanshow19: No, evlauation

[18:45] <ReinH> *evaluation

[18:45] <ReinH> putStrLn "foo" >> putStrLn "bar" evaluates to an IO
action that is composed of both actions. This happens separately from
execution.

[18:46] <trumanshow19> Well, how would a strict language evaluate
`getLine >>= putStrLn` *without* performing these two effects?

[18:46] <bennofs> trumanshow19: evaluating it. You can build up a
value of type :: IO () in your program and store it in a datastructure

[18:46] <nshepperd> > putStrLn "we don't print this" `seq` 7

[18:46] <lambdabot>  7

[18:47] <trumanshow19> "<bennofs> You can build up a value of type ::
IO () in your program and store it in a datastructure" .. in a strict
language also?#

[18:47] <ReinH> bennofs: laziness makes the separation between
evaluation and execution more clear, but they are still two separate
processes

[18:47] <nshepperd> trumanshow19: yes

[18:48] <nshepperd> trumanshow19: just as much as you can (strictly)
compile a program without running it

[18:48] <ski> > length [putStrLn s | s <- take (2 + 3) (cycle
["hi","there"])]

[18:48] <lambdabot>  5

[18:49] <trumanshow19> Interesting, what would this look like? I'd
love to see an example in OCaml, or Java, where I am able to build up
an IO value of `getLine >>= putStrLn` that does *not* either execute
getLine or write to the terminal my key strokes.

[18:49] <bennofs> trumanshow19: you can for example represent IO () a
just a function in a strict language that doesn't take any
arguments. Executing the IO action would then correspondend to
involking that function

[18:49] <ski> trumanshow19 : "how would a strict language evaluate
`getLine >>= putStrLn` *without* performing these two effects?" --
more or less as in Haskell

[18:49] <trumanshow19> Maybe I'm being stupid, but I've never seen
this in an imperative do-this-do-that language.

[18:49] <ReinH> trumanshow19: Well yes, because they are not pure.

[18:49] <ReinH> So they don't have the same semantics

[18:49] <hexagoxel> trumanshow19: i liked
http://www.alexeyshmalko.com/2015/io-is-your-command-pattern/

[18:50] <bennofs> trumanshow19: (fun () =>   ... get line in ocaml
...) : () -> string   would be equal to just getLine in Haskell

[18:50] <ReinH> strictness is a property of *evaluation*, not
execution

[18:50] <trumanshow19> ReinH: what's an example of a strict, purely FP
language?

[18:50] <trumanshow19> Then my question is "how would <that language>
evaluate `getLine >>= putStrLn` *without* performing these two
effects?"

[18:50] <bennofs> trumanshow19: sequencing it would work like:
sequence f k = fun () => k (f ()) ()

[18:50] <nshepperd> Idris is strict, isn't it?

[18:51] <ski> trumanshow19 : there's a temptation in strict languages
to add side-effects, because strictness means that it's relatively
easy (for smaller examples, not using higher-order functions) to
reason about when they will happen. otoh "non-strictness (especially
by-need/lazinesS) keeps you honest", by making it harder to predict
this

[18:51] <ReinH> nshepperd: yes

[18:51] <bennofs> trumanshow19: oops, just looked up ocaml syntax,
replace => with -> in my examples

[18:52] <ski> trumanshow19 : continuing what bennofs says, you'd
probably never explicitly execute an I/O action in such a strict
language, letting the run-time start the process

[18:52] <ReinH> trumanshow19: They would implement getLine >>=
putStrLn by strictly evaluating rather than lazily evaluating to the
resulting IO () value.

[18:52] <ReinH> strictness is a property of evaluation, not execution

[18:53] <ski> (if you could/would execute it yourself, then that would
break equational reasoning for you)

[18:53] <ReinH> There is no reason IO can't be implemented both
strictly and purely because strictness and purity are orthogonal

[18:53] <nshepperd> > (getLine >>= putStrLn) `seq` 500

[18:53] <lambdabot>  500

[18:54] <nshepperd> trumanshow19: strictly evaluated IO action ^^

[18:54] <nshepperd> (more or less)

[18:54] <ski> i recall seeing on some blog someone who'd made a toy
language and implementation for controlling some kind of robots. using
monads for those effects (also being a dynamically typed language)

[18:55] <aweinstock> trumanshow19: ocaml example: fun () ->
print_string (read_line ())

[18:55] <trumanshow19> ski ReinH nshepperd hexagoxel bennofs : thanks!
Time to ponder :-)

[18:55] <aweinstock> (ocaml is strict and impure, but still in the ML
family, related to haskell)

[18:57] <ski> trumanshow19 : "what's an example of a strict, purely FP
language?". Hope is an example

[18:57] <ski>
<https://en.wikipedia.org/wiki/Hope_%28programming_language%29>

[18:58] <ski> trumanshow19 : for one that is used (and is actually a
logic/functional programming language), Mercury