\( \DeclareMathOperator{\tr}{tr} \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} % For +---- metric \newcommand{\BDpos}{} \newcommand{\BDneg}{-} \newcommand{\BDposs}{\phantom{-}} \newcommand{\BDnegg}{-} \newcommand{\BDplus}{+} \newcommand{\BDminus}{-} % For -+++ metric \newcommand{\BDpos}{-} \newcommand{\BDposs}{-} \newcommand{\BDneg}{} \newcommand{\BDnegg}{\phantom{-}} \newcommand{\BDplus}{-} \newcommand{\BDminus}{+} \)
UP | HOME

IO Monad - SML

Table of Contents

1. Introduction

We typically abstract away effects in a monad, and IO is one of the most basic effects for programmers.

Recall the basic idea for using monads: if we have a function with a side-effect (like printing a message to the screen), then let us denote its type with a squiggle arrow f : A ~> B. Pure functions without side-effects would be written as pure_fn : A -> B with the usual arrow.

Suppose now that we wanted to curry a function with a side-effect f : A * B ~> C, what would its type look like? We would guess it either looks like g : A -> (B ~> C) or h : A ~> (B ~> C). We would also expect applying only one argument would not produce any side-effect, only when both arguments are provided would a side-effect be produced. This would be the first case, g : A -> (B ~> C) describes f : A * B ~> C curried.

Now, we can recall () * A is isomorphic as a type to A. This means that f : A ~> B is isomorphic to a function with type f2 : A * () ~> B. Currying this function gives us g2 : A -> (() ~> B). Now we introduce a monad with type B impure = () ~> B which means we have our impure function isomorphic to the pure function g2 : A2 -> B impure.

For IO operations, the monadic bind amounts to ordering the IO operations and executing them in the order given. For our purposes in this exploration, it suffices to explore teletype IO (i.e., printing a string to the terminal, reading text from the keyboard, and nothing else).

In an eager language, the IO monad is a weak monad. This is proven in chapter 8 of Andrew Gordon's PhD dissertation. Think about the situation when a bottom value has been encountered, but will not be needed in the next IO operation. Lazy languages can carry on without a problem. Eager languages cannot.

However, lazy IO breaks equational reasoning…which is pretty much why we would want monadic IO (for the equational reasoning!).

The IO monad makes sense for a single-core processor, but how would we extend this to work with multiple threads executed in parallel?

Our implementation will also be incomplete compared to what, say, Haskell offers. There are avenues for further investigation.

Would it be possible to extend the IO monad implemented in Standard ML to include IORef operations? If so, could we do it without relying on native ref types?

2. Andrew Gordon's IO Monad

We can construct the IO Monad in Standard ML, which has been done in Andrew Gordon's PhD thesis. There the construction uses an abstract type: 

infix 1 >> >>=
abstype 'a Job = JOB of unit -> 'a
with
    (* exec : 'a Job -> 'a *)
    fun exec (JOB f)  = f ()
    (* return : 'a -> 'a Job *)
    fun return x      = JOB (fn _ => x)
    (* (>>=) : 'a Job * ('a -> 'b Job) -> 'b Job *)
    fun (JOB f) >>= q = JOB (fn _ => exec (q (f ())))
    (* getStr : int -> TextIO.vector Job *)
    fun getStr n      = JOB (fn _ => TextIO.inputN(TextIO.stdIn, n))
    (* putStr : string -> unit Job *)
    fun putStr s      = JOB (fn _ => print s)
end

(* (>>) : 'a Job * 'b Job -> 'b Job *)
fun p >> q  =  p >>= (fn _ => q);

(* gettingLine : string -> string Job *)
fun gettingLine s =
    getStr 1 >>= (fn c => if c = "\n"
                          then return(s)
                          else gettingLine (s^c));

(* getLine : string Job *)
val getLine = gettingLine "";

val main : unit Job =
    putStr "First name: " >> getLine >>= (fn first =>
    putStr "Second name: " >> getLine >>= (fn second =>
    putStr ("Hello "^first^" "^second^"\n")));
(* exec main; *)

3. Using Modules

We can encode the IO Monad using SML's Module system. The signature for a Monad would be: 

signature MONAD = sig
    type 'a m;
    val return : 'a -> 'a m;
    val bind : 'a m -> ('a -> 'b m) -> 'b m;
end;

The IO Monad requires a few more public-facing methods. 

signature IO_MONAD =
sig
    include MONAD;
    val exec : 'a m -> 'a;
    val getStr : int -> TextIO.vector m;
    val putStr : string -> unit m;
end;

Observe we just switched the Job constructor to m. The implementation details are straightforward.

4. Concluding Remarks

We can also implement an IO monad using Free monads, since free monads provide a way to abstract away impure functions inside a pure monad. This would not be performant in Haskell.

But there is also a way to implement an IO monad using monad transformers. This is what the PureIO proof-of-concept library does in Haskell.

We have so far not discussed blocking IO too much, but that's because blocking IO comes about from threads and multiple processes. Essentially something else is reading or writing to a file (or stream or socket or…) and we have to wait until the resource is free. When will it become important to model this in an IO monad?

5. References

  • Andrew Gordon,
    "Functional Programming and Input/Output".
    Ph.D. Thesis, Cambridge, 1994; Eprint.
  • Andrew Gordon,
    "PFL+: A Kernal Scheme for Functions I/O".
    UCAM tech report 160, dated February 1989 PDF
  • Simon Peyton Jones,
    "Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell".
    in Engineering theories of software construction, IOS Press, 2001; Eprint and pdf.
    • Discusses the IO monad using a "two tier" semantics, with process semantics for the IO part and some denotational semantics for a lazy lambda calculus.
  • PureIO — a pedagogical IO monad implemented in Haskell
  • free-io/Free.hs implementation using Free monads

Last Updated 2025-02-26 Wed 16:56.