Effectful Programming in Haskell

This chapter introduces Haskell with emphasis on types that track effects (for example monads and IO) and equational reasoning. We will see how Haskell’s strict separation between pure and effectful code is not merely a stylistic choice — it is what makes large-scale equational reasoning and machine-assisted verification practical.

Goals¶

• Relate pure functional programming to verification.

• Use a concise example to illustrate effects and monads.

• Explore the Maybe and Either monads as a further aspect.

• Link to GHC documentation, Learn You a Haskell, and modern Haskell tooling.

1 Pure Functions and Equational Reasoning¶

A pure function has two properties:

1. Its output depends only on its inputs — no hidden state, no globals.

2. It has no side effects: it does not read from a file, print to the terminal, modify a mutable variable, or throw an exception that alters program state.

In mathematics, you can freely substitute equals for equals: if $f(x) = x + 1$ and $x = 3$, then $f(x) = f(3) = 4$. This is called equational reasoning and it is completely safe because $f$ does nothing except compute a value.

In an imperative language this substitution is not always safe:

# Python — side-effecting function; substitution can break meaning
count = 0
def increment():
    global count
    count += 1
    return count

x = increment()   # x = 1, count = 1
y = increment()   # y = 2, count = 2
# x ≠ y even though both are "increment()"

Haskell makes purity the default. Every top-level definition in Haskell is a pure expression unless its type explicitly says otherwise. This default unlocks three verification superpowers:

2 A First Look at Haskell¶

2.1 Running Haskell¶

The standard compiler is GHC (Glasgow Haskell Compiler). The modern way to install it is through GHCup, a toolchain manager analogous to rustup:

# Install GHCup, GHC, Cabal, and Stack in one step
curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh

For a quick scratchpad, use GHCi, the interactive REPL:

ghci

GHCi, version 9.8.2: https://www.haskell.org/ghc/  :? for help
ghci> 2 + 2
4
ghci> :type "hello"
"hello" :: String

2.2 Types and Type Signatures¶

Every Haskell expression has a type, inferred automatically by GHC. You can annotate types explicitly with :::

-- | Double an integer.
double :: Int -> Int
double n = n * 2

-- | Add two integers.
add :: Int -> Int -> Int
add x y = x + y

You can verify types in GHCi:

ghci> :type double
double :: Int -> Int
ghci> :type add 3
add 3 :: Int -> Int

2.3 Pattern Matching and Recursion¶

Haskell encourages defining functions by cases using pattern matching:

-- | Factorial, defined by pattern matching.
factorial :: Integer -> Integer
factorial 0 = 1
factorial n = n * factorial (n - 1)

GHC checks that patterns are exhaustive — covering every possible input — which prevents a whole class of runtime crashes common in other languages.

3 The Problem of Effects¶

Pure functions are great for reasoning, but real programs must interact with the world: read files, accept user input, write to a database, send network requests. These are effects — observable interactions with state or the environment beyond the function’s return value.

Haskell’s answer is to make effects visible in the type. A function that can perform I/O is given a return type wrapped in IO:

-- Pure — type says nothing about the outside world
square :: Int -> Int
square x = x * x

-- Effectful — the IO wrapper tells the reader (and GHC) this touches the world
greet :: IO ()
greet = putStrLn "Hello, world!"

The type IO () is read: “an I/O action that produces a value of type () (unit, like void in C)”. The type IO String would be an action that produces a String after performing some I/O.

This boundary is the key insight: purity is the default; effects are opt-in, and opting in is visible in every type signature along the call chain.

4 Monads — Sequencing Effectful Computations¶

4.1 Motivation¶

Suppose you want to chain two I/O actions: first read a line of input, then print a personalised greeting. In pure code you can just compose functions. With IO values you need a way to sequence them — “do this action, then, using whatever it produced, do the next action.”

This sequencing pattern is captured by the Monad type class. The two essential operations are:

For IO specifically:

-- Manually sequenced with >>=
greetUser :: IO ()
greetUser =
  putStr "Enter your name: " >>= \_ ->
  getLine >>= \name ->
  putStrLn ("Hello, " ++ name ++ "!")

4.2 do-Notation¶

Writing >>= chains by hand gets unwieldy. Haskell provides do-notation as syntactic sugar that looks like imperative code but desugars to >>=:

-- Same function, written with do-notation
greetUser :: IO ()
greetUser = do
  putStr "Enter your name: "
  name <- getLine                       -- bind: extract the String from IO String
  putStrLn ("Hello, " ++ name ++ "!")

The <- arrow in do-notation corresponds exactly to the \name -> lambda in the bind chain. Crucially, this is still pure Haskell — the do-block builds a description of a computation that the runtime will execute. Nothing is executed until main (the program entry point) runs it.

main :: IO ()
main = greetUser

4.3 The Monad Laws¶

Every instance of Monad must satisfy three algebraic laws, which are the formal basis for equational reasoning about monadic code:

-- Left identity:  return a >>= f   ≡   f a
-- Right identity: m >>= return     ≡   m
-- Associativity:  (m >>= f) >>= g  ≡   m >>= (\x -> f x >>= g)

These laws guarantee that >>= behaves like sequential composition: you can refactor a chain of monadic actions — extracting sub-chains into named helpers, or inlining them — without changing the program’s meaning. This is equational reasoning applied to effectful code.

5 Verified Error Handling: Maybe and Either¶

One of Haskell’s most practically valuable monads is Maybe, which encodes optional values without null pointers.

5.1 The Maybe Type¶

data Maybe a = Nothing | Just a

A value of type Maybe Int is either Nothing (absence of a value) or Just 42 (a present value). There is no null — the type itself forces you to handle both cases.

-- | Safe integer division: returns Nothing on divide-by-zero.
safeDiv :: Int -> Int -> Maybe Int
safeDiv _ 0 = Nothing
safeDiv x y = Just (x `div` y)

ghci> safeDiv 10 2
Just 5
ghci> safeDiv 10 0
Nothing

5.2 Chaining with the Maybe Monad¶

The Maybe monad propagates Nothing automatically through a chain of computations — the monadic equivalent of short-circuit evaluation:

-- | Look up a value, double it, then halve it — failing safely at any step.
compute :: Int -> Int -> Int -> Maybe Int
compute x y z = do
  a <- safeDiv x y   -- Nothing if y = 0
  b <- safeDiv a z   -- Nothing if z = 0
  return (a + b)

ghci> compute 100 5 2
Just 30
ghci> compute 100 0 2
Nothing
ghci> compute 100 5 0
Nothing

Without Maybe, each division would need its own if check. With the monad, the failure plumbing is handled automatically — and, crucially, it is impossible to forget. A pure Int -> Int -> Int function cannot represent failure; you must choose a richer type.

5.3 Either for Structured Errors¶

Maybe discards the reason for failure. Either preserves it:

data Either e a = Left e | Right a

By convention, Left carries an error value and Right carries a success value. (Remember it as: “right is right.”)

data DivError = DivideByZero | NegativeInput deriving (Show)

safeDiv' :: Int -> Int -> Either DivError Int
safeDiv' _ 0 = Left DivideByZero
safeDiv' x y
  | x < 0 || y < 0 = Left NegativeInput
  | otherwise       = Right (x `div` y)

ghci> safeDiv' 10 2
Right 5
ghci> safeDiv' 10 0
Left DivideByZero
ghci> safeDiv' (-4) 2
Left NegativeInput

The Either DivError monad sequences these checks exactly like Maybe does, but a caller receiving a Left always knows why the computation failed — this information is encoded in the type and cannot be lost.

6 Equational Reasoning in Practice¶

Let us verify a small property of our safeDiv function using equational reasoning — the same style used in formal verification tools like Liquid Haskell and Agda.

Claim: safeDiv x 1 = Just x for all Int x.

Proof:

safeDiv x 1
  = Just (x `div` 1)    -- by the second equation of safeDiv (1 ≠ 0)
  = Just x              -- by the arithmetic law  x `div` 1 = x

Each step substitutes equals for equals. This works because safeDiv is pure: there is no hidden state that could make the second call behave differently from the first, so the substitution is always valid.

Compare this to proving a property of an imperative function that mutates a counter — you would need to reason about the entire machine state at every step, an exponentially harder task.

7 Putting It Together — A Small Complete Program¶

Below is a self-contained program that exercises IO, do-notation, Maybe, and pattern matching together:

module Main where

import Text.Read (readMaybe)

-- | Safe division, as defined earlier.
safeDiv :: Int -> Int -> Maybe Int
safeDiv _ 0 = Nothing
safeDiv x y = Just (x `div` y)

-- | Prompt the user for an Int, retrying on bad input.
readInt :: String -> IO Int
readInt prompt = do
  putStr prompt
  line <- getLine
  case readMaybe line of
    Just n  -> return n
    Nothing -> do
      putStrLn "Not a valid integer. Please try again."
      readInt prompt

main :: IO ()
main = do
  x <- readInt "Numerator:   "
  y <- readInt "Denominator: "
  case safeDiv x y of
    Nothing -> putStrLn "Error: division by zero."
    Just q  -> putStrLn ("Result: " ++ show q)

Notice the separation of concerns enforced by the type system:

• safeDiv is pure (Maybe Int, no IO) — it can be reasoned about and tested without any runtime.

• readInt is effectful (IO Int) — it interacts with the terminal.

• main is the single point that connects them.

This separation is not a convention — GHC will reject any attempt to call putStrLn from inside safeDiv or to embed a pure function’s result in an IO context without an explicit return.

8 Modern Haskell Tooling¶

9 Summary¶

Haskell’s design forces a clear boundary between pure logic and effectful interaction. This boundary is what makes equational reasoning — and ultimately formal verification — tractable: the pure core of a program can be proved correct in isolation, and the effectful shell can be kept thin and auditable.

References and Further Reading¶

• Lipovača, M. Learn You a Haskell for Great Good! — a friendly, illustrated introduction to Haskell. Freely available online.

• GHC Team. GHC User’s Guide — authoritative reference for the compiler and language extensions.

• GHC Team. GHCi Reference — interactive environment documentation.

• Marlow, S. Parallel and Concurrent Programming in Haskell — extends the monad story to concurrency.

• Vazou, N. et al. Refinement Types for Haskell (Liquid Haskell) — connects the purity of Haskell to machine-checked proofs.

• Hackage. transformers package and mtl package — standard libraries for monad transformer stacks.