haskeller.net

Introduction

The Elegant Art of Functional Programming

Haskell is a purely functional programming language where every function is a mathematical function, every type tells a story, and every program is a proof. Named after the logician Haskell Curry, it represents the culmination of decades of research into programming language design.

Unlike imperative languages that describe how to compute, Haskell describes what to compute. This distinction, seemingly subtle, cascades into a fundamentally different way of thinking about software — one where correctness is not an afterthought but a structural guarantee.

In Haskell, the type system is not merely a safety net; it is a design language. Types guide composition, constrain behavior, and eliminate entire categories of bugs before a single line runs. The compiler is not your adversary — it is your collaborator.

main :: IO ()
The type of every Haskell program's entry point — an IO action producing nothing.

pure :: a -> f a
Lift a value into a computational context.

A functor F mapping objects and morphisms between categories

a -> b

Types as a Design Language

In Haskell, types are not annotations bolted onto existing code. They are the architecture of your program. Before writing a single implementation, a Haskell programmer writes type signatures — and those signatures often contain enough information to derive the implementation mechanically.

Consider the humble identity function. Its type, id :: a -> a, admits exactly one implementation. There is no room for bugs, no edge case left unconsidered. The type is the specification.

Haskell

-- Algebraic data types compose
data Maybe a = Nothing | Just a

-- Pattern matching is exhaustive
safeDivide :: Double -> Double -> Maybe Double
safeDivide _ 0 = Nothing
safeDivide x y = Just (x / y)

-- Type classes generalize behavior
class Functor f where
  fmap :: (a -> b) -> f a -> f b

Parametric polymorphism guarantees that a function of type a -> a cannot inspect its argument. It must treat all types uniformly. This property, known as theorems for free, means that types alone can prove deep properties about program behavior.

Hindley-Milner type inference means you rarely need to write type signatures. But you should — they are documentation that the compiler checks.

const :: a -> b -> a
Two type variables, one implementation. The type tells the whole story.

fmap

Functors: Mapping Between Worlds

A functor is a structure-preserving map between categories. In Haskell, this translates to a deceptively simple interface: given a way to transform values, a functor lets you transform values in a context without breaking that context apart.

Lists are functors. Trees are functors. Optional values are functors. IO actions are functors. The pattern is universal, and recognizing it transforms the way you write code — from manipulating data structures to composing transformations.

Haskell

-- The functor law: fmap id = id
-- Structure is preserved

fmap (+1) [1, 2, 3]       -- [2, 3, 4]
fmap (+1) (Just 5)       -- Just 6
fmap (+1) Nothing         -- Nothing

-- Composition: fmap (f . g) = fmap f . fmap g
fmap (show . (+1)) [1,2,3]
  -- ["2","3","4"]

The functor laws are not merely conventions — they are the mathematical guarantee that mapping preserves structure. A lawful functor cannot reorder elements, drop values, or introduce side effects. The abstraction constrains just enough to remain universally useful.

In category theory, a functor maps both objects (types) and morphisms (functions) while preserving composition and identity.

<$> is the infix operator for fmap — a visual reminder that you are lifting a function into a context.

A natural transformation η : F ⇒ G between functors

m a -> (a -> m b) -> m b

Monads: Sequencing the Pure

The monad is perhaps the most discussed abstraction in all of programming — and the most misunderstood. It is not a burrito, not a box, not a metaphor. It is a mathematical structure that captures the pattern of sequencing computations that produce values in a context.

Where a functor lets you transform values inside a context, a monad lets you chain operations that themselves produce contextualized values. The bind operator, >>=, is the key: it threads a value out of one computation and into the next, while the context (failure, state, IO, nondeterminism) is handled automatically.

Haskell

-- The Monad type class
class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return :: a -> m a

-- Maybe monad: short-circuit on Nothing
lookup "name" env >>= parse >>= validate

-- Do notation: syntactic sugar for >>=
do
  name  <- lookup "name" env
  parsed <- parse name
  validate parsed

The genius of monads in Haskell is that they make effects explicit in the type. An IO String is not a String — it is a recipe for obtaining a String through side effects. This distinction, enforced by the type system, means that pure code and effectful code cannot be accidentally mixed. Purity is the default; effects are opt-in and visible.

The monad laws: return a >>= f ≡ f a
m >>= return ≡ m
(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

Philip Wadler introduced monads to functional programming, bringing a concept from category theory into practical use.

Monad: unit (η) and join (μ) natural transformations

Programs

id :: a -> a
id x = x

fst :: (a, b) -> a
fst (x, _) = x

compose :: (b -> c)
         -> (a -> b)
         -> (a -> c)
compose f g x = f (g x)

absurd :: Void -> a
-- no cases needed

Proofs

A ⇒ A
Proof: Assume A. Then A. □

A ∧ B ⇒ A
Proof: ∧-elimination (left). □

(B ⇒ C) ∧ (A ⇒ B)
  ⇒ (A ⇒ C)
Hypothetical syllogism. □

⊥ ⇒ A
Ex falso quodlibet. □

The Curry-Howard Correspondence: every program is a proof, every type is a proposition

1 / 4