-
-
Save nahiyan/ba87a96d61aa2d312bba59683c6a6fb4 to your computer and use it in GitHub Desktop.
Confusion about analogy's of purity in Haskell
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[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 | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment