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.
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.
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.