Types are sets. Functions are morphisms between them. The category Hask has Haskell types as objects and pure functions as arrows. Every type is extended with bottom (⊥), the value representing non-termination.
Types as sets
A type is a set of values. Bool is the two-element set {True, False}; Integer is an infinite set. Functions between types are mappings between sets, and that gives us the category Set: objects are sets, morphisms are functions. Programming types live in exactly this structure.
Scheme
; Types are sets of values; Bool = {#t, #f} — a two-element set; A function from Bool picks two values from the target set
(define (bool->string b)
(if b "yes""no"))
; This function IS a morphism in Set: {#t, #f} -> {"yes", "no"}
(display "True -> ") (display (bool->string #t)) (newline)
(display "False -> ") (display (bool->string #f)) (newline)
; How many functions from Bool to Bool?; Each of 2 inputs can map to 2 outputs: 2^2 = 4
(define id-bool (lambda (b) b))
(define not-bool (lambda (b) (not b)))
(define always-t (lambda (b) #t))
(define always-f (lambda (b) #f))
(display "id: ") (display (id-bool #t)) (display " ") (display (id-bool #f)) (newline)
(display "not: ") (display (not-bool #t)) (display " ") (display (not-bool #f)) (newline)
(display "const-T: ") (display (always-t #t)) (display " ") (display (always-t #f)) (newline)
(display "const-F: ") (display (always-f #t)) (display " ") (display (always-f #f))
Python
# Types are sets of values# bool = {True, False}def bool_to_string(b):
return"yes"if b else"no"print(f"True -> {bool_to_string(True)}")
print(f"False -> {bool_to_string(False)}")
# All 4 functions from bool to bool
fns = {
"id": lambda b: b,
"not": lambda b: not b,
"const-T": lambda b: True,
"const-F": lambda b: False,
}
for name, f in fns.items():
print(f"{name}: True->{f(True)}, False->{f(False)}")
Pure functions
A pure function always returns the same output for the same input and has no side effects. Only pure functions count as morphisms in a category. Impure functions (I/O, mutation, randomness) break composability: if f's output depends on hidden state, g ∘ f is not determined by the types alone.
Scheme
; Pure: same input, same output, no side effects; A pure function IS a morphism — it composes reliably
(define (square x) (* x x))
(define (add1 x) (+ x 1))
; Composition works because both are pure
(define (add1-then-square x) (square (add1 x)))
(define (square-then-add1 x) (add1 (square x)))
(display "square(5) = ") (display (square 5)) (newline)
(display "add1(5) = ") (display (add1 5)) (newline)
(display "add1-then-square(5) = ") (display (add1-then-square 5)) (newline)
(display "square-then-add1(5) = ") (display (square-then-add1 5)) (newline)
; Memoization test: a pure function can always be memoized; because calling it twice with the same input is identical
(display "square(5) again = ") (display (square 5))
; Same answer, guaranteed. That's purity.
Python
# Pure functions compose reliablydef square(x): return x * x
def add1(x): return x + 1print(f"square(5) = {square(5)}")
print(f"add1(5) = {add1(5)}")
print(f"add1(square(5)) = {add1(square(5))}")
print(f"square(add1(5)) = {square(add1(5))}")
# Impure function — breaks composability
counter = 0def impure_add(x):
global counter
counter += 1return x + counter
print(f"impure_add(5) = {impure_add(5)}") # 6print(f"impure_add(5) = {impure_add(5)}") # 7 — different!# Same input, different output. Not a morphism.
Bottom — the value that never arrives
Every Haskell type secretly includes one extra value: bottom (⊥), representing non-termination. A function that loops forever or throws an exception returns bottom. This makes Hask different from Set: in Set, every function terminates. In Hask, a function Bool → Bool can return True, False, or ⊥. Functions that may return bottom are partial; those that always return a proper value are total.
Scheme
; Bottom: non-termination extends every type; In Hask, Bool = {#t, #f, ⊥}; A total function: always returns a value
(define (safe-not b) (if b #f#t))
; A partial function: sometimes returns bottom
(define (partial-not b)
(if b #f
(let loop () (loop)))) ; infinite loop = bottom
(display "safe-not(#t) = ") (display (safe-not #t)) (newline)
(display "safe-not(#f) = ") (display (safe-not #f)) (newline)
(display "partial-not(#t) = ") (display (partial-not #t)) (newline)
; partial-not(#f) would loop forever — that's bottom
(display "partial-not(#f) = ... (would never return)")
Void — the empty set
The type Void has no values: the empty set. You cannot call a function that takes Void as input, because you have nothing to pass it. But you can declare one: absurd :: Void → a. From falsity, anything follows. This is the Curry-Howard correspondence in action.
Scheme
; Void: the empty type — no values exist; absurd : Void -> a (can be defined but never called); We can't construct a Void value, so we simulate with a tag
(define (absurd v)
(display "ERROR: absurd: Void has no values") (newline))
; Functions FROM Void: you can declare them but never run them; Functions TO Void: impossible (no value to return); The empty set has exactly one function to any set:; the empty function (vacuously defined on zero inputs)
(display "Void is the empty set.") (newline)
(display "There is exactly 1 function from {} to any set:") (newline)
(display " the empty function (maps nothing to nothing)") (newline)
(display "|functions: Void -> A| = 1 for any A") (newline)
(display "|functions: A -> Void| = 0 (unless A is also Void)")
Unit — the singleton set
The type () (unit) has exactly one value. Functions from unit to a type A are in one-to-one correspondence with elements of A: each such function "picks" one value. The function unit :: a → () discards its argument and returns the single value. It is the unique morphism to the terminal object.
Scheme
; Unit: the singleton set with one value; Functions from unit to A correspond to elements of A; In Scheme, we use 'unit as the single value
(define unit-val 'unit)
; A function () -> Integer just picks a number
(define (f44 u) 44)
(define (f0 u) 0)
(display "f44(unit) = ") (display (f44 unit-val)) (newline)
(display "f0(unit) = ") (display (f0 unit-val)) (newline)
; The function a -> () always returns unit (terminal morphism)
(define (to-unit x) unit-val)
(display "to-unit(42) = ") (display (to-unit 42)) (newline)
(display "to-unit("hello") = ") (display (to-unit "hello")) (newline)
(display "to-unit(#t) = ") (display (to-unit #t)) (newline)
; |functions: () -> A| = |A| (one per element); |functions: A -> ()| = 1 (the unique terminal morphism)
(display "() is the terminal object in Set and Hask.")
Python
# Unit type: Python has None as its unit valuedef f44(): return44# () -> int: picks 44def f0(): return0# () -> int: picks 0print(f"f44() = {f44()}")
print(f"f0() = {f0()}")
# The function a -> () discards its argumentdef to_unit(x): returnNoneprint(f"to_unit(42) = {to_unit(42)}")
print(f"to_unit('hello') = {to_unit('hello')}")
print(f"to_unit(True) = {to_unit(True)}")
# There's only one such function — it's the terminal morphism
Bool — the two-element set
Bool has exactly two values. Functions to Bool are predicates: they classify inputs into true/false. Functions from Bool select a pair of values from the target type. Bool is the simplest interesting type: big enough to branch on, small enough to enumerate.
Scheme
; Bool = {#t, #f} — the two-element set; Functions TO Bool are predicates
(define (is-even? n) (= (remainder n 2) 0))
(define (is-positive? n) (> n 0))
(display "is-even?(4) = ") (display (is-even? 4)) (newline)
(display "is-even?(7) = ") (display (is-even? 7)) (newline)
; Functions FROM Bool select two values
(define (bool->color b) (if b "red""blue"))
(define (bool->int b) (if b 10))
(display "bool->color(#t) = ") (display (bool->color #t)) (newline)
(display "bool->color(#f) = ") (display (bool->color #f)) (newline)
; |functions: Bool -> A| = |A|^2 (pick two elements with replacement); |functions: A -> Bool| = 2^|A| (every subset defines a predicate)
(display "|Bool -> Bool| = 4") (newline)
(display "|Bool -> {r,g,b}| = 9") (newline)
(display "|{a,b,c} -> Bool| = 8")
All examples use total functions in Scheme and Python. The bottom example simulates non-termination with an infinite loop but never runs it. Milewski's treatment works in Hask, where every type includes bottom and the category is technically CPO-enriched rather than Set. The examples on this page stay in Set (no bottom, no laziness): the four Bool→Bool functions enumerated above are exactly the four morphisms in Set. In Hask, additional "functions" return bottom on some inputs, raising the count.
Ready for the real thing? Read Chapter 2. Start with "What Are Types?" for the sets-and-functions picture, then "Examples of Types" for Void, Unit, and Bool.
Framework connection: Types are the handshake between pipeline stages. The target type of one morphism must match the source type of the next, and the Natural Framework enforces this at every stage boundary. (The Handshake)
sets. Functions are morphisms between them. The category Hask has Haskell types as objects and pure functions as arrows. Every type is extended with bottom (⊥), the value representing non-termination.
The Handshake)