main :: Introduction -> TypeSystem -> Syntax -> Community -> Resources -> IO ()_
Prelude> :t haskell.quest
haskell.quest :: Quest -> Understanding

Simon Peyton Jones, 1987

Philip Wadler, monads as computational patterns

The Haskell Report, 1990

introduction

Haskell is not a product to be marketed or a tool to be evangelized. It is a phenomenon to be understood -- a convergence of mathematical insight and engineering pragmatism that has been unfolding since 1990, when a committee of researchers decided that lazy functional programming deserved a common language. What emerged was not merely a programming language but a way of thinking about computation itself.

The language insists on purity: functions have no side effects, values are immutable, and the type system tracks the boundary between the world of pure computation and the world of observable effects. This is not a limitation. It is the deepest design insight in the history of programming languages.

Where imperative languages describe sequences of mutations -- change this variable, update that pointer, modify this record -- Haskell describes relationships between values. A Haskell program is not a list of instructions. It is a collection of equations. And equations, unlike instructions, can be reasoned about, composed, and proven correct.

 1 module Main where
 2
 3 -- The identity function: the simplest possible abstraction
 4 id :: a -> a
 5 id x = x
 6
 7 -- Composition: the essence of modularity
 8 (.) :: (b -> c) -> (a -> b) -> a -> c
 9 f . g = \x -> f (g x)
10
11 -- The constant function: ignoring context
12 const :: a -> b -> a
13 const x _ = x
_

Hindley-Milner type inference, 1969/1978

Wadler & Blott, type classes, 1989

Curry-Howard correspondence: types are propositions, programs are proofs

typeSystem

Haskell's type system is its crown jewel. Where other languages treat types as annotations or constraints, Haskell treats them as propositions in a logical system. Every well-typed program is a proof. Every type signature is a theorem. The compiler does not merely check your program -- it reasons about it.

The type system is built on algebraic data types, which combine sum types (alternatives) and product types (records) into a single, elegant mechanism. From these primitives, you can build any data structure: lists, trees, graphs, protocols, state machines.

 1 -- Algebraic data types: sum and product types
 2 data Maybe a = Nothing | Just a
 3
 4 data Either a b = Left a | Right b
 5
 6 data Tree a
 7   = Leaf a
 8   | Branch (Tree a) (Tree a)
_ 
 1 -- Type classes: principled polymorphism
 2 class Eq a where
 3   (==) :: a -> a -> Bool
 4   (/=) :: a -> a -> Bool
 5   x /= y = not (x == y)
 6
 7 class Functor f where
 8   fmap :: (a -> b) -> f a -> f b
 9
10 class Functor f => Applicative f where
11   pure  :: a -> f a
12   (<*>) :: f (a -> b) -> f a -> f b
13
14 class Applicative m => Monad m where
15   (>>=) :: m a -> (a -> m b) -> m b
16   return :: a -> m a
17   return = pure
_

Pattern matching originates from ML, 1973

List comprehensions mirror Zermelo-Fraenkel set notation

syntax

 1 -- Pattern matching
 2 length :: [a] -> Int
 3 length []     = 0
 4 length (_:xs) = 1 + length xs

Pattern matching decomposes data by its shape. Every case is explicit. No null checks, no instanceof, no casting.

 1 -- List comprehensions
 2 pythagorean :: Int -> [(Int, Int, Int)]
 3 pythagorean n =
 4   [ (a, b, c)
 5   | c <- [1..n]
 6   , b <- [1..c]
 7   , a <- [1..b]
 8   , a*a + b*b == c*c
 9   ]

List comprehensions read like mathematical set notation. The syntax is the mathematics.

 1 -- Guards: conditional equations
 2 bmi :: Double -> String
 3 bmi x
 4   | x < 18.5  = "underweight"
 5   | x < 25.0  = "normal"
 6   | x < 30.0  = "overweight"
 7   | otherwise = "obese"

Guards replace if-else chains with mathematical piecewise notation.

 1 -- Monadic do-notation
 2 main :: IO ()
 3 main = do
 4   contents <- readFile "input.txt"
 5   let ws = words contents
 6   putStrLn (show (length ws) <> " words")

Do-notation sequences effects while preserving purity. The IO monad tracks the boundary between computation and the world.

 1 -- Where clauses: local definitions
 2 circleArea :: Double -> Double
 3 circleArea r = pi * r ^ 2
 4   where
 5     pi = 3.14159265358979
_

community

resources

main :: Introduction -> TypeSystem -> Syntax -> Community -> Resources -> IO ()_