Type-Level Programming

Course 2 · Ch 7

A lighter chapter after Chapter 6's honest heaviness — and a genuine convergence with ts4-5's own branded types

A deliberately lighter touch after haskell2-6's own honest complexity. This chapter previews what "type-level programming" even means, and lands on a real, satisfying convergence with a completely different type system this site already covers.

What "Type-Level Programming" Means, Briefly

Ordinary programming works with values at runtime. Type-level programming means using the type system itself to encode and enforce constraints, with the compiler doing the real work during type-checking rather than at runtime. Kept light and practical here, not a deep academic treatment.

Phantom Types

data Tagged tag a = Tagged a   -- tag never actually appears on the right-hand side!

tag appears in the declaration but is never actually stored or used in any of the real data — a phantom type. It exists purely to let the compiler distinguish otherwise-identical values, like Tagged "Meters" Double versus Tagged "Feet" Double, catching an accidental mix-up at compile time with zero runtime cost, since tag is never stored anywhere real.

Direct Comparison to ts4-5's Own Branded Types

ts4-5's own TypeScript branded types use genuinely the same trick — a phantom property existing only at the type level to prevent two structurally-identical types from being accidentally interchanged. This is the same core idea, arrived at independently in a structural type system (TypeScript) and a nominal one (Haskell) — worth naming the convergence explicitly, since it shows the idea is useful enough to be reinvented across genuinely different type-system philosophies.

A Practical Example — Preventing Unit Mix-Ups

newtype Meters = Meters Double
newtype Feet = Feet Double

addMeters :: Meters -> Meters -> Meters
addMeters (Meters a) (Meters b) = Meters (a + b)

-- addMeters (Meters 5) (Feet 3)   -- REAL compile error, not a runtime mismatch

A real, concrete, motivating example: the compiler catches an attempt to add Meters and Feet directly, a genuine practical safety win with zero runtime overhead — newtype wrappers compile away completely.

GADTs — Generalized Algebraic Data Types

{-# LANGUAGE GADTs #-}

data Expr a where
    IntLit  :: Int -> Expr Int
    BoolLit :: Bool -> Expr Bool
    Add     :: Expr Int -> Expr Int -> Expr Int

-- Add (IntLit 5) (BoolLit True)   -- REAL compile error — Add requires two Expr Int

A real, honest step up in power from haskell1-6's own plain data declarations: GADT syntax lets each constructor specify its own, more specific return type, rather than every constructor sharing the same generic one. This makes a genuinely type-safe mini expression language possible, where an ill-typed expression like adding an Int to a Bool is a real compile error — directly useful groundwork for Chapter 8's own capstone interpreter.

{-# LANGUAGE GADTs #-} — Another Honest Extension Flag

Same honest spirit as haskell2-5's own MultiParamTypeClasses acknowledgment: GADTs require an explicit extension flag, not part of core Haskell 2010 — worth naming plainly rather than presenting as if it had always just been part of the language.

Concept	haskell1-6's plain ADTs	GADTs	TypeScript (ts4-5)
Constructor return types	all share the same generic type	each constructor specifies its own	n/a — structural typing
Phantom-type-style tagging	possible, but GADTs unneeded for it	n/a	branded types — same core idea
Core language or extension	core Haskell 2010	requires {-# LANGUAGE GADTs #-}	core TypeScript feature

Reach for a phantom type or newtype whenever values share a representation but shouldn't mix

Units, IDs belonging to different entity types, and similar cases are exactly where a lightweight phantom type or newtype wrapper buys real compile-time safety for zero runtime cost.

Don't reach for GADTs unless plain ADTs genuinely can't express the constraint

GADT syntax is real, genuine additional complexity — worth it specifically when different constructors truly need different, more specific return types (like the Expr a example), not as a default replacement for ordinary data declarations.

Coding Challenges

Challenge 1

Define newtype wrappers UserId and ProductId, both wrapping an Int, and write a function that only accepts a UserId. Attempt to call it with a ProductId instead and show the resulting compile error.

📄 View solution

Challenge 2

Define the Expr a GADT from the chapter (IntLit, BoolLit, Add) plus a new constructor If :: Expr Bool -> Expr a -> Expr a -> Expr a, and write an eval :: Expr a -> a function that correctly evaluates a small expression using it.

📄 View solution

Challenge 3

Write a short comment explaining the real convergence between Haskell's phantom types and ts4-5's own branded types, addressing specifically how the same "compiler-only tag" idea gets expressed differently in a nominal type system versus a structural one.

📄 View solution

Chapter 7 Quick Reference

Type-level programming uses the type system itself to enforce constraints, resolved during compilation, not at runtime
Phantom types carry a type parameter that's never actually stored, existing purely to prevent mix-ups at compile time, zero runtime cost
Genuinely the same core idea as ts4-5's own branded types — independently converged upon across a nominal and a structural type system
newtype wrappers (Meters/Feet) are a real, practical, zero-cost way to prevent unit/ID mix-ups
GADTs let each constructor of a data type specify its own, more specific return type — a real step up from haskell1-6's plain ADTs, useful for a type-safe mini expression language
GADTs require an explicit language extension, same honest-wart spirit as haskell2-5's own MultiParamTypeClasses
Next chapter: the capstone — a real small Haskell program combining ADTs, typeclasses, monads, and IO from across both courses