🎯 Learning Objectives
Understand Type Theory Basics
Learn what types are, why they matter, and how they prevent errors before runtime.
Master Dimensional Analysis
See how Fourier's 1822 insight that physical equations must balance dimensionally is actually a type system.
Implement Type-Safe Units
Build a Haskell library where adding meters to seconds is a compile-time error.
Apply Buckingham Pi Theorem
Understand how dimensionless groups emerge automatically from type constraints.
📖 Key Concepts
What is a Type?
A type is a classification of values that specifies what operations can be performed on them. In programming:
5has typeInt— you can add, multiply, compare integers"hello"has typeString— you can concatenate, search strings5 + "hello"is a type error — the operation doesn't make sense
In physics, dimensions ARE types:
5 metershas typeLength3 secondshas typeTime5 meters + 3 secondsis a type error — dimensionally meaningless!
Fourier's Principle of Dimensional Homogeneity (1822)
"Every equation expressing the laws of nature must be dimensionally homogeneous."
This is the first type system for physics! Fourier recognized that physical quantities are not mere numbers—they carry structure (dimensions) that constrains how they can be combined.
The Buckingham Pi Theorem
Any physically meaningful equation involving n variables with k independent dimensions can be rewritten using n - k dimensionless parameters.
Example: The Reynolds number Re = ρvL/μ is dimensionless because:
ρ : [M L⁻³] (density)
v : [L T⁻¹] (velocity)
L : [L] (length)
μ : [M L⁻¹ T⁻¹] (viscosity)
Re = ρvL/μ : [M L⁻³][L T⁻¹][L][M⁻¹ L T] = [M⁰ L⁰ T⁰] = dimensionless ✓💻 Code Examples
Type-Safe Dimensions in Haskell
{-# LANGUAGE DataKinds, TypeFamilies, GADTs #-}
-- Dimensions encoded at the type level
-- (Length, Time, Mass, Temperature, Current, Amount, Luminosity)
type Length = '(1, 0, 0, 0, 0, 0, 0)
type Time = '(0, 1, 0, 0, 0, 0, 0)
type Velocity = '(1, -1, 0, 0, 0, 0, 0) -- L T⁻¹
-- A quantity carries its dimension as a phantom type
newtype Quantity (d :: (Int,Int,Int,Int,Int,Int,Int)) = Quantity Double
-- Base units
meter :: Quantity Length
meter = Quantity 1.0
second :: Quantity Time
second = Quantity 1.0
-- Addition ONLY works for same dimensions
(|+|) :: Quantity d -> Quantity d -> Quantity d
(Quantity x) |+| (Quantity y) = Quantity (x + y)
-- This compiles:
twoMeters = meter |+| meter -- ✓ Both are Length
-- This is a COMPILE ERROR:
-- bad = meter |+| second -- ✗ Cannot unify Length with TimeComputing Velocity (Type-Safe)
-- Division produces correct derived dimension
(|/|) :: Quantity d1 -> Quantity d2 -> Quantity d3
(Quantity x) |/| (Quantity y) = Quantity (x / y)
-- Velocity = Distance / Time
velocity :: Quantity Velocity
velocity = (100 *| meter) |/| (5 *| second)
-- Result: 20 m/s with type Quantity '(1, -1, 0, 0, 0, 0, 0)
-- The type system GUARANTEES dimensional correctness!🤖 AI Learning Prompts
Use these prompts with Claude, ChatGPT, or other AI assistants to deepen your understanding.
"Explain dimensional analysis as if it were a type system. What are the 'types'? What are the 'type errors'? How does Fourier's principle of dimensional homogeneity correspond to type safety in programming?"
"Tell me about Fourier's 1822 work on heat conduction and how he discovered the principle of dimensional homogeneity. Why was this a revolutionary insight? How did it influence later physics?"
"Explain the Buckingham Pi theorem with a concrete example. Show me how to derive the Reynolds number as a dimensionless group. Why do dimensionless numbers appear in physics, and what do they tell us about physical systems?"
"Help me implement a type-safe dimensional analysis library in Haskell. I want adding meters to seconds to be a compile-time error. Explain GADTs, DataKinds, and phantom types as needed."
"Explain the basics of type theory for someone coming from physics. What is a type? What is the difference between static and dynamic typing? What does 'type safety' mean and why does it matter?"
"What are dependent types and how do they extend simple type systems? Give me a preview of how dependent types can encode even more physical constraints—like ensuring a vector has exactly 3 components for 3D space."
"Give me 5 dimensional analysis problems to solve. For each, I should determine: (1) the dimensions of the answer, (2) whether the equation is dimensionally valid, (3) what dimensionless groups can be formed. Then check my work."
"Tell me about the Mars Climate Orbiter disaster of 1999, where a unit conversion error caused the loss of a $327 million spacecraft. How could type-safe dimensional analysis have prevented this? What lessons does this teach about the importance of type systems?"
✏️ Exercises
Exercise 1: Dimensional Checking
Determine whether each equation is dimensionally valid:
- v = at (velocity = acceleration × time)
- E = mc² (energy = mass × speed²)
- F = mv (force = mass × velocity)
- P = ρgh (pressure = density × gravity × height)
Exercise 2: Derive Dimensionless Numbers
The period T of a pendulum depends on length L and gravitational acceleration g. Use dimensional analysis to find the form of T(L, g).
Exercise 3: Implement in Haskell
Extend the Haskell code to include:
- Force = Mass × Acceleration
- Energy = Force × Distance
- Power = Energy / Time
Verify that computing kinetic energy E = ½mv² produces the correct Energy type.