From a practical point of view, how do functional languages with formally specified semantics (like ML) handle side effects like printing? I'm aware of things like the IO monad in Haskell but I'm interested in how the actual primitives are encoded and implemented. Thanks in advance.
$\begingroup$
$\endgroup$
3
-
$\begingroup$ I'm not sure to understand the question. You want to know how printing is implemented? What do you mean by side effect. I searched it online and don't get much result. $\endgroup$– user123Commented Nov 6, 2021 at 22:30
-
$\begingroup$ I don't have a computer science background. I actually found the answer to my question. I think by side effect you mean something like the following (from wikipedia): an operation, function or expression is said to have a side effect if it modifies some state variable value(s) outside its local environment, that is to say has an observable effect besides returning a value. $\endgroup$– user123Commented Nov 6, 2021 at 22:52
-
$\begingroup$ Actually, I answer mostly questions about operating-systems and the interface between operating-systems and programming languages so this is a good question of interest for me. $\endgroup$– user123Commented Nov 6, 2021 at 22:55
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
7
Monads in Haskell serve two purposes.
A monad that is defined within Haskell is really a simulation of some computational effect in terms of pure (side-effect free) computation. After all, Haskell is a pure language.
The second use of monads in Haskell, as well as in programming language semantics, and many other languages, is to model external or primitive computational effects. Such effects cannot be defined within the language itself. They necessarily come from some external environment (hardware, operating system, virtual machine).
In Haskell the monad that gives access to external effects is IO. This is why the main program has the type IO () – so that it can actually interact with the external world through computational effects.
Under the hood, the Haskell compiler compiles pure code, including user-defined monads, to machine code that behaves equivalently to the pure code (with respect to a formal semantics). But it takes special care of code of type IO by compiling things like putStr to actual system calls that trigger real I/O (I am over-simplifying a bit, but you get the point).
The ML-family of languages differ from Haskell because they do not separate so cleanly the pure & effectful computations. In such "impure" languages, all computations happen in a single IO-style monad that gives access to all external effects (I/O, mutable memory, exceptions) all the time. And the fact that this is the case is not recorded in types. Thus, an ML computation of type int would really be something like IO Int in Haskell.
Of course, the programmer is free to define their own monads in ML to simulate various computational effects, just like in Haskell, but this is a bit irrelevant here.
You ask how the effects are specified in the formal semantics. There are several ways of doing it (transition semantics, algebraic semantics, abstract interpretation), and I am not sure that describing them here would serve a purpose. Please ask for further references if you'd like to know the details.
The important thing to understand is the relationship between the formal semantics, which is the mathematical model of computational effects, and the actual implementation by the language compiler, which converts source code to machine code that triggers computational effects by using the available hardware, possibly via some system calls. We want the mathematical model and the compiled code to match, i.e., the compiler should be correct with respect to the formal semantics.
answered Nov 7, 2021 at 18:41
-
$\begingroup$ If I understand correctly, Haskell handles side effects by building up a control flow graph (in the same fashion as
data Expr = ... | ...) and the interpretation executes it in a meta-theoretic level, and IO is simply encapsulating the monadic structure of the abstract "graph"? $\endgroup$ Commented Nov 7, 2021 at 19:00 -
$\begingroup$ It's not clear from your question what are you asking. Are you asking how precisely Haskell and ML actually compile effectful code, or how computational effects are specified in formal semantics? $\endgroup$ Commented Nov 7, 2021 at 19:03
-
$\begingroup$ Phrases such "the interpretation executes it in a meta-theoretic level" do not mean a whole lot to me. Maybe try to explain precisely what you would like to know, in concrete terms. $\endgroup$ Commented Nov 7, 2021 at 19:04
-
1$\begingroup$ As I said, there are several formalisms for reasoning about external effects. A recent one (apologies for self-promotion) is Runners in action. It's got monads for extermal computation, but also programming concepts for virtualization and OS-style access to external effects. $\endgroup$ Commented Nov 7, 2021 at 20:34
-
1$\begingroup$ I am afraid "pure language with IO capability" is a bit of an oxymoron, since IO makes it impure. But Haskell and ML are both polymorphic $\lambda$-calculi with IO. $\endgroup$ Commented Nov 7, 2021 at 20:35
$\begingroup$
$\endgroup$
From a practical point of view, how do functional languages with formally specified semantics (like ML) handle side effects like printing? I'm aware of things like the IO monad in Haskell but I'm interested in how the actual primitives are encoded and implemented.
It is strange to lump ML and Haskell together in this question. Unlike Haskell, ML is not a functional language in the sense that you seem to be using the term here.
ML handles side-effects in exactly the same way that C or Java or almost any mainstream programming language does: it doesn't. It ignores them.
This is in contrast to Haskell, where side-effects are not possible at all. There are no ways to express side-effects in the Haskell 2010 language and there are no ways to express side-effects using the Haskell 2010 standard library.
Okay. There is a big asterisk attached to that paragraph.
First off, there are actually functions like System.IO.Unsafe.unsafePerformIO which allow you to use unrestricted side-effects. Note, however, that this function is explicitly placed in the System.IO.Unsafe module, and also note that it is not part of the Haskell 2010 Specification. So, there is already a double warning sign around it: first, you have the fact that it is a non-portable implementation-specific extension to the standard, and then you have the word "unsafe" in the module name.
These functions are considered to be "escape hatches" for emergency use by very experienced programmers working on performance-sensitive core libraries, they are not considered to be part of the normal toolset of a Haskell programmer.
In other words, using these functions is considered to be outside the realm of Haskell; whenever you use them, you leave all the protections and guarantees of Haskell behind.
Secondly, of course, there is the System.IO module, which is part of Haskell 2010. This is how you can perform I/O (the most general form of side-effects) in Haskell. Except, technically, you are not performing I/O using the System.IO module. What you are doing is describing purely-functional I/O Actions, and returning these Actions to the runtime.
The runtime then contains an impure evaluator for those Actions. So, the trick that Haskell uses, is that the programmer never performs side-effects. The programmer only describes the side-effects to the runtime, and the runtime then performs those side-effects … but the runtime is not considered to be inside the realm of Haskell and therefore is not bound by the restrictions of Haskell.
How the runtime performs those side-effects is considered to be irrelevant. That is what programming, in the end, is all about: abstraction and reuse. As long as I get a description of how to use some "thing", I don't need to know how that "thing" works internally … in fact, ideally, it should be impossible for me to figure out how that "thing" works internally (IOW it should be impossible to break an abstraction boundary).
Now, of course, most Haskell implementations are open source, so we can just check. E.g. GHC implements the I/O runtime at least partially in C and calls out to the Operating System's I/O routines. (In fact, GHC contains multiple different implementations of the I/O subsystem for e.g. POSIX vs. Windows or single- vs. multi-threaded Runtime System.) Other Haskell implementations are allowed to implement I/O differently. For example, I am assuming that the (now defunct) Haskell.NET did not implement I/O in C but in C#; similarly, I am assuming that the (now defunct) Jaskell did not implement I/O in C but in Java. I assume GHCJS implements I/O in ECMAScript.
In short, most Haskell implementations view the graph of I/O Actions generated by the IO monad as instructions to some form of abstract machine … in other words, they view them as a language, and they deal with them the way you deal with any other language: you either compile it to a language you know how to interpret, or you interpret it directly.
