Types are theorems.
Programs are proofs.

Purity

In Haskell, a function is a mathematical function. Given the same inputs, it will always produce the same output. There are no hidden dependencies, no ambient state mutations, no temporal coupling. This constraint, which appears limiting at first, turns out to be the most liberating design decision in the history of programming language design. When effects are tracked in the type system, the compiler becomes your most trusted collaborator.

module Purity where
import Data.List (foldl')
-- A pure function: no side effects, total, referentially transparent
fibonacci :: Integer -> Integer
fibonacci 0 = 0
fibonacci 1 = 1
fibonacci n = fibonacci (n - 1) + fibonacci (n - 2)
-- Laziness makes infinite structures finite in practice
fibs :: [Integer]
fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
-- Every value is immutable. Every computation is a declaration.
golden :: Double
golden = (1 + sqrt 5) / 2
-- Equational reasoning: we can substitute equals for equals
sumSquares :: [Int] -> Int
sumSquares = foldl' (+) 0 . map (^ 2)

Laziness

Haskell evaluates nothing until it must. This is not indolence; it is strategic patience. Lazy evaluation means that data structures are promises, not values -- they materialize only at the moment of consumption. This permits the programmer to define infinite structures, to separate the description of a computation from its execution, and to compose producers and consumers without worrying about intermediate allocation.

module Laziness where
-- The natural numbers: all of them
nats :: [Integer]
nats = [0..]
-- The Sieve of Eratosthenes, rendered as a one-liner
primes :: [Integer]
primes = sieve [2..]
  where
    sieve (p:xs) = p : sieve [x | x <- xs, x `mod` p /= 0]
    sieve []     = []
-- Streams that generate themselves
data Stream a = Cons a (Stream a)
headS :: Stream a -> a
headS (Cons x _) = x
tailS :: Stream a -> Stream a
tailS (Cons _ xs) = xs
iterateS :: (a -> a) -> a -> Stream a
iterateS f x = Cons x (iterateS f (f x))

Type Classes

Where other languages reach for interfaces or abstract classes, Haskell offers type classes -- a mechanism for ad-hoc polymorphism that is simultaneously more principled and more expressive than anything in the object-oriented tradition. A type class is a contract written in the language of types, and an instance is a proof that a specific type satisfies that contract. The hierarchy from Functor through Applicative to Monad is not an arbitrary taxonomy but a ladder of increasing power, each rung precisely defined.

class Functor f where
  fmap :: (a -> b) -> f a -> f b
class Functor f => Applicative f where
  pure  :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b
class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return = pure
-- Laws that every instance must obey:
-- fmap id      = id                    (identity)
-- fmap (f . g) = fmap f . fmap g       (composition)
-- A concrete instance: the list functor
instance Functor [] where
  fmap = map
instance Applicative [] where
  pure x    = [x]
  fs <*> xs = [f x | f <- fs, x <- xs]

Monads

A monad is not a burrito. A monad is not a space suit. A monad is a design pattern for composing computations that carry context. In Haskell, monads are how we sequence operations, handle errors gracefully, manage state explicitly, and interact with the outside world -- all while maintaining the purity guarantees that make our programs trustworthy. The bind operator threads context through a computation the way gravity threads mass through spacetime: invisibly, inevitably, and with mathematical precision.

module Monads where
import Control.Monad ((>=>))
-- The Maybe monad: computation that might fail
safeDivide :: Double -> Double -> Maybe Double
safeDivide _ 0 = Nothing
safeDivide x y = Just (x / y)
-- Composing fallible computations with do-notation
compute :: Double -> Double -> Double -> Maybe Double
compute x y z = do
  a <- safeDivide x y
  b <- safeDivide a z
  pure (a + b)
-- IO: the monad that touches the world
greet :: IO ()
greet = do
  putStrLn "What is your name?"
  name <- getLine
  putStrLn ("Hello, " <> name <> ".")
-- State: explicit mutation without impurity
newtype State s a = State { runState :: s -> (a, s) }
get :: State s s
get = State (\s -> (s, s))
put :: s -> State s ()
put s = State (\_ -> ((), s))

Composition

The deepest insight of functional programming is that complex systems are built from simple, composable parts. In Haskell, function composition is not a technique -- it is the fundamental operation. The dot operator joins two functions into one. The fish operator composes monadic functions. At every level of abstraction, the same principle holds: build small things that work, then compose them into larger things that also work. This is not optimism; it is a theorem.

module Composition where
import Data.List (sort, nub)
import Text.Read (readMaybe)
import Control.Monad ((>=>))
-- Function composition: the essence of modularity
process :: [String] -> String
process = unlines
        . map ("  " <>)
        . filter (not . null)
        . sort
        . nub
-- Kleisli composition: composing monadic functions
pipeline :: String -> Maybe Int
pipeline = readMaybe >=> validate >=> transform
  where
    validate n
      | n > 0     = Just n
      | otherwise = Nothing
    transform = Just . (* 2) . (+ 1)
-- Higher-order composition: functions that build functions
on :: (b -> b -> c) -> (a -> b) -> a -> a -> c
on f g x y = f (g x) (g y)
-- The ultimate composition: a program is a value
main :: IO ()
main = interact (unlines . map process . lines)