· 5 min read
Infinity on demand
Haskell’s infinite lists are finite producers whose usefulness depends on productivity, short-circuiting consumers, fair enumeration, and forgetting prefixes the program has already used.
Ask GHCi for take 8 [0..] and it answers immediately. The notation makes an endless row look as though it already exists somewhere behind the prompt, waiting to be sliced. There is no infinite list waiting behind [0..]; there is a rule for producing another cell when the consumer asks.
Haskell makes infinity useful by arranging finite observations of an unbounded process. The property that keeps the trick honest is productivity: every request for the next constructor must reach one after finite work. Lose that property and the type can still say “infinite” while the program waits forever.
The tail is a promise#
GHC itself carries an internal infinite-list type with no empty constructor. Stripped to the part that matters, the design looks like this:
data Infinite a = Inf a (Infinite a)naturalsFrom :: Integer -> Infinite IntegernaturalsFrom n = Inf n (naturalsFrom (n + 1))takeInf :: Int -> Infinite a -> [a]takeInf 0 _ = []takeInf n (Inf x xs) = x : takeInf (n - 1) xs- 1Every value exposes one element and another
Infinite; there is noNilcase. - 2The outer
Infappears before the recursive tail is demanded. - 3The consumer supplies the finite budget. Only that many tails need evaluation.
The recursive call in naturalsFrom sits in the lazy tail. Constructing the first cell leaves the second as suspended work. I love how little machinery this needs: the ellipsis in [0..] does an outrageous amount of conceptual work, while the heap receives only the portion evaluation reaches.
The type still cannot guarantee progress. GHC's internal filter for Infinite may reject elements until it finds one to emit. Apply filter (const False) to repeat 1 and even head diverges. Its no-empty shape says nothing about how long the program searches before producing another constructor.
The consumer chooses the ending#
The same unbounded producer can answer one consumer and hang under another. Ask for its end and you have asked for a constructor it never promised.
| Expression | What it must inspect | Outcome |
|---|---|---|
take 5 [0..] | Five constructors | Returns [0,1,2,3,4] |
take 5 (map (* 2) [0..]) | One input per output | Returns a prefix |
any (> 1000) [0..] | Until the first match | Returns True |
foldr (&&) True (repeat False) | The first False | Returns False |
foldl' (+) 0 [0..] | The final constructor | Never returns |
head (reverse [0..]) | The end before the first output | Never returns |
head (filter (< 0) [0..]) | A matching element | Never returns |
The Data.Foldable documentation draws this line explicitly. A strict left fold must reach the last element before returning, so its input has to be finite. A lazy right fold can return when its combining function ignores the recursive result, which is why one False settles the infinite conjunction above.
Infinite data works well for questions with finite evidence: find the first match, sample a signal, generate the next test case, or take a prefix for display. Asking for length, last, or a complete strict sum waits for a boundary the producer never promised.
Productive can still be unfair#
Producing forever is weaker than exploring everything. A nested search over two infinite lists keeps yielding pairs, yet the inner list monopolizes the program and the first coordinate never advances.
unfairPairs = [(x, y) | x <- [0..], y <- [0..]]fairPairs = [ (x, total - x) | total <- [0..] , x <- [0..total] ]take 6 unfairPairs -- [(0,0),(0,1),(0,2),(0,3),(0,4),(0,5)]take 6 fairPairs -- [(0,0),(0,1),(1,0),(0,2),(1,1),(2,0)]The diagonal version spends a finite amount of time on each total before moving on, so every pair of natural numbers eventually appears. Property-test enumerators and search code need this distinction: a generator can remain productive while starving every branch after the first infinite one.
GHC's internal module handles the same problem in allListsOf. It emits all one-element lists, then all two-element lists, then the next length, instead of diving into one endless extension. Its output order decides whether every candidate gets a turn.
The machine stays finite#
An unbounded producer still runs on a bounded heap. A pipeline can operate on a small live prefix when the consumer releases old cells. Keep a reference to the beginning and the reachable prefix stays live; the list type alone cannot promise constant space.
Floating-point infinity is one finite encoding used in numeric operations. An infinite list describes continuing structure and survives only because the program never asks to hold all of it at once. I would not use the same word for those two representations without checking which one an API means.
GHC's source places data Infinite a = Inf a (Infinite a) near a filter whose result carries that same type. Give the filter a predicate that never accepts and the first constructor never arrives. The type removes Nil. The predicate can still search forever before returning Inf.