🐱 Agda Sized Types: Deep Dive

Alright kittens, I've been meaning to write this up for a while. Let's do a proper deep dive into sized types in Agda — specifically how they help us control coinductive productivity in a way that's actually compositional and modular, unlike Agda's older syntactic guardedness checker.

The core motivation: coinductive types in Agda denote greatest fixpoints. If you want to define infinite structures (streams, potentially infinite trees, etc.), you need corecursion. But Agda is a total language — every program must terminate or be productive. The guardedness checker is the traditional answer, but it has sharp edges.

Let's start with the classic example. A stream without sized types:

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A

-- This works fine
repeat : ∀ {A} → A → Stream A
head (repeat x) = x
tail (repeat x) = repeat x

-- This might be REJECTED by the guardedness checker!
zipWith : ∀ {A B C} → (A → B → C) → Stream A → Stream B → Stream C
head (zipWith f xs ys) = f (head xs) (head ys)
tail (zipWith f xs ys) = zipWith f (tail xs) (tail ys)

The guardedness checker works syntactically — it needs corecursive calls to be directly under a constructor. Once you pass a corecursive result through a helper function, the checker may lose track of the guard. This is where sized types come in.

Sized types track the "depth" of a coinductive structure via an ordinal-like index. The key primitives in Agda are:

-- Enable with: {-# OPTIONS --sized-types #-}
open import Size

-- Size : Set              (the type of sizes)
-- ∞    : Size             (the "infinite" size / greatest element)
-- ↑_   : Size → Size      (successor of a size)
-- Size< i : Set           (sizes strictly less than i)

-- A sized stream:
record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : ∀ {j : Size< i} → Stream A j

Now Stream A i is a stream defined to depth at least i. A value of type Stream A ∞ is a fully productive infinite stream. The sized version of zipWith typechecks beautifully:

zipWith : ∀ {A B C} {i : Size}
         → (A → B → C)
         → Stream A i → Stream B i → Stream C i
head (zipWith f xs ys)         = f (head xs) (head ys)
tail (zipWith f xs ys) {j = j} = zipWith f (tail xs) (tail ys)
-- tail xs : Stream A j, with j : Size< i  ✓ structurally decreasing!

The size index acts as a certificate: tail xs has type Stream A j for j < i, so we're definitely making progress. The type system handles what the syntactic checker couldn't.

I'll follow up with the Abel-Pientka paper discussion. Who's read it?

Oh hell yes, this is exactly the thread I needed. I've been trying to connect sized types to the coinductive program analysis stuff we discuss here. The key thing for me is that sized types make productivity compositional — you can black-box functions as long as they're "size-preserving".

This is huge for program analysis! If you have a coinductive abstract domain (think: abstract interpretation over infinite traces), you want to be able to compose analysis transformers without reexposing all their internals to the guardedness checker every time.

The analogy I use: sized types are to productivity what structural recursion is to termination. They're the semantic, compositional version of a syntactic check. Instead of asking "is the corecursive call syntactically under a constructor?", you ask "does the type guarantee the structure decreases in size?"

On the Abel-Pientka paper — I've read the JFP version ("Well-founded recursion with copatterns and sized types"). The combination of copatterns + sized types is genuinely elegant. Copatterns let you define coinductive types by their observations (what you can destructure out), and sized types give you the compositionality.

Lurker here, finally posting. Can you say more about what Size< i means exactly? I get that it's "sizes strictly less than i" but what is the underlying model? Are we talking actual ordinals?

Great question! Semantically, yes — sizes correspond to ordinal numbers. The idea is that a coinductive type Stream A i represents streams unfolded up to ordinal depth i. Here's the intuition spelled out:

-- Sizes are essentially ordinals, with an extra ∞ element.
-- You have access to:
--   ∞    : Size         -- "fully infinite", the top element
--   ↑ i  : Size         -- successor of i
--   Size< i             -- all sizes j such that j < i

-- Key: ∞ is *not* the largest size — ↑ ∞ would be larger!
-- Actually ∞ behaves as if ∞ : Size< ∞, which is a known quirk.

-- For coinduction: Stream A ∞ is the "real" coinductive type.
-- Stream A (↑ i) means: head is defined, and tail has depth i.
-- Stream A i (for i : Size< j) means: depth < j.

-- Sized corecursion pattern:
myStream : ∀ {i : Size} → Stream ℕ i
head myStream     = 42
tail myStream {j} = myStream {j}
-- j : Size< i, so the recursive call is at a SMALLER size ✓

The paper by Abel and Pientka phrases it precisely: sizes are an abstraction over well-founded ordinal-like orders. You don't need the full power of classical ordinals — you just need a well-founded order with a successor operation. The full power of classical ordinals is not needed to justify the recursion schemes; we only need a well-founded order that is "long enough" and has a successor operation.

I want to bring in the comparison with Coq's guardedness checker since people always ask "why not just use Coq?"

Coq uses a syntactic guardedness check for corecursive definitions (the CoFixpoint mechanism). The rule is roughly: a CoFixpoint definition is productive if every corecursive call appears directly under at least one constructor of the coinductive type.

(* This is ACCEPTED by Coq's guard checker *)
CoFixpoint zeros : Stream nat :=
  Cons 0 zeros.   (* corecursion under Cons ✓ *)

(* This may be REJECTED — call not directly under constructor *)
CoFixpoint bad (f : Stream nat → Stream nat)
               (s : Stream nat) : Stream nat :=
  f (Cons (hd s) (bad f (tl s))).  (* bad: f is opaque *)

The problem is that Coq can't look inside f to verify productivity. Even if f is clearly size-preserving, the syntactic checker has no way to know. You end up having to inline helper functions, use dirty tricks with Delay monads, or restructure your program significantly.

Agda's sized types solve this by encoding the productivity guarantee in the type. A function of type Stream A i → Stream A i is provably size-preserving, and the checker can trust it without looking inside.

Let me now go through the Abel-Pientka paper more carefully. The key paper is:

Andreas Abel & Brigitte Pientka (2016). "Well-founded recursion with copatterns and sized types." Journal of Functional Programming, 26, e2.

The main insight is combining two ideas:

• Copatterns — define coinductive data by their observations (eliminations), not just constructors
• Sized types — track structural depth of (co)inductive data via ordinal-like size indices

Here's a coinductive type defined with copatterns + sized types:

open import Size

-- Sized Stream: parameterized by size i
record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : {j : Size< i} → Stream A j
open Stream

-- map defined using copatterns — each observation defined separately
map : ∀ {A B} {i : Size} → (A → B) → Stream A i → Stream B i
head (map f s)     = f (head s)
tail (map f s) {j} = map f (tail s {j})
-- Recursive call: map f (tail s {j}) : Stream B j, j < i ✓

-- Fibonacci stream (mix of induction + coinduction!)
fib : ∀ {i : Size} → ℕ → ℕ → Stream ℕ i
head (fib m n)     = m
tail (fib m n) {j} = fib n (m + n)
-- Result: 0, 1, 1, 2, 3, 5, 8, ...

What's remarkable here: fib uses copatterns (defining the stream by what you observe from it) and sized types (the j < i ensures productivity). The termination checker sees the recursive call produces a stream of strictly smaller size.

This connects really beautifully to coinductive program analysis. Let me sketch the connection.

In abstract interpretation of potentially infinite/reactive programs (think: process calculi, dataflow systems), your abstract domain often needs to be a final coalgebra. Your analysis functions are then natural transformations between coalgebras — and their compositionality is critical.

With sized types, an abstract analysis function over infinite traces can be typed like:

-- An abstract trace is a coinductive stream of abstract states
record AbsTrace (S : Set) (i : Size) : Set where
  coinductive
  field
    now  : S
    next : {j : Size< i} → AbsTrace S j

-- A size-preserving analysis transformer
-- (compositional by construction!)
Transformer : Set → Set → Set
Transformer S T = ∀ {i : Size} → AbsTrace S i → AbsTrace T i

-- Compose two transformers — productivity guaranteed by types!
_∘ᵀ_ : ∀ {S T U} → Transformer T U → Transformer S T
        → Transformer S U
(g ∘ᵀ f) trace = g (f trace)

The composition g ∘ᵀ f is automatically accepted because each function's type declares it as size-preserving. No manual productivity proofs needed! This is the compositional payoff.

What about the known issues with Agda's sized types implementation? I heard there are consistency problems?

Yeah, this is important to address. The current Agda implementation of sized types is flagged as experimental and has known soundness issues. The most famous one is that ∞ : Size< ∞ is treated as true in the implementation, which leads to paradoxes.

-- In Agda's current implementation:
-- ∞ : Size< ∞  is ACCEPTED (it shouldn't be!)
-- This means you can "unpack" ∞ as if it's smaller than itself.
-- This can lead to non-termination / False proofs in edge cases.

-- Example of what goes wrong conceptually:
-- If ∞ < ∞, then the well-founded recursion on Size is broken
-- because there's no "base case" — ∞ can always go deeper.

-- Agda has an open issue for this (github: infinity-less-than-infinity)
-- A new design is being discussed to fix this properly.

Danielsson's paper "Up-to Techniques using Sized Types" (POPL 2018) explicitly notes this — the current Agda implementation contains bugs related to sized types, specifically that ∞ : Size< ∞ has led to implementation problems.

The practical advice: use {-# OPTIONS --sized-types #-} and be careful. For truly safety-critical proofs, consider the --safe flag (which disables sized types). For most coinductive programming tasks, sized types work fine in practice and the unsoundness is hard to trigger accidentally.

The guardedness vs. sized types debate also extends to the question of which is easier to use. Let me give a concrete example where sized types shine: the Delay monad.

open import Size

-- The Delay monad: a computation that may take finitely many steps
data Delay (A : Set) (i : Size) : Set where
  now   : A → Delay A i
  later : {j : Size< i} → Delay A j → Delay A i

-- bind: sequence two delayed computations
_>>=_ : ∀ {A B} {i : Size}
      → Delay A i
      → (A → Delay B i)
      → Delay B i
now x     >>= f = f x
later d   >>= f = later (d >>= f)
-- d : Delay A j, j < i, so recursive call typechecks! ✓

-- never: a computation that never terminates
never : ∀ {A} {i : Size} → Delay A i
never = later never

Without sized types, getting _>>=_ to pass the guardedness checker requires awkward encoding. With sized types, it's structurally obvious. This is what Abel and Chapman demonstrated in their "Normalization by Evaluation in the Delay Monad" paper.

This is gold. What's the comparison with guarded recursion (Nakano modality, Atkey-McBride, etc.)? I've seen a paper called "Guarded Recursion in Agda via Sized Types" that claims to simulate guarded recursion using sized types?

Yes! That's the Veltri & van der Weide paper from FSCD 2019. The key insight is that sized types can simulate the ▶ (later) modality of guarded type theory. Here's the sketch:

open import Size

-- In guarded recursion: ▶ A is "A available one step later"
-- We simulate it with a Thunk:

record Thunk (F : Size → Set) (i : Size) : Set where
  coinductive
  field
    force : {j : Size< i} → F j
open Thunk

-- Thunk F i is "F, available at any size j < i"
-- This corresponds to ▶ F in guarded recursion!

-- Example: sized Conat using Thunk
data Conat (i : Size) : Set where
  zero : Conat i
  suc  : Thunk Conat i → Conat i

-- infinity: the conatural number ω
infinity : ∀ {i} → Conat i
infinity = suc λ where .force → infinity

This is exactly how the Agda standard library defines Conat in Codata.Sized.Conat! The Thunk type is the key bridge — it wraps a computation that must be forced at a smaller size.

The difference from proper guarded type theory: in guarded recursion (Clocks & Causality style), the modality ▶ is a first-class type constructor with its own introduction/elimination forms and clock quantifiers. Sized types are more like a structural approximation — expressive enough for most uses but without the full clock quantification machinery.

Okay I'm sold. One last question: what's a good "minimal example" that shows why you'd pick sized types over just using the standard library's record ... coinductive without sizing?

Perfect timing. Here's the canonical example — a coinductive parser / language recognizer. This is actually what the Agda docs use to explain sized types, and it's very clean:

open import Size
open import Data.Bool

-- A language over alphabet A is an infinite decision tree
record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool                              -- does ε belong?
    δ : {j : Size< i} → A → Lang j A    -- derivative by character
open Lang

-- Union of two languages (sized → compositional!)
_∪_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν   (a ∪ b)     = ν a ∨ ν b
δ   (a ∪ b) {j} c = δ a {j} c ∪ δ b {j} c

-- Concatenation (here sized types are ESSENTIAL)
_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (a · b)     = ν a ∧ ν b
δ (a · b) {j} c =
  if ν a
  then (δ a {j} c · b) ∪ δ b {j} c   -- ν a true: both derivatives
  else  δ a {j} c · b               -- ν a false: only left
-- All recursive calls are at size j < i. Without sized types,
-- this FAILS the guardedness check (b appears inside if_then_else)!

The _·_ (concatenation) case is the killer example. The corecursive call passes through if_then_else, which is opaque to the guardedness checker. Sized types handle this transparently because all we care about is that the resulting languages have a smaller depth index.

Amazing thread. For people wanting to dive deeper, the reading order I'd suggest:

1. Agda documentation on sized types — start here
2. Abel (2010) — MiniAgda: Integrating sized and dependent types
3. Abel & Pientka (2016) — Well-founded recursion with copatterns and sized types (JFP)
4. Danielsson (2018) — Up-to Techniques using Sized Types (POPL)
5. Veltri & van der Weide (2019) — Guarded Recursion in Agda via Sized Types (FSCD)

Start with the Agda docs, then MiniAgda for the theory, then JFP for the full copatterns story, then the latter two for more advanced applications.

Great discussion everyone! Let me summarize the key takeaways:

• 🐱 Sized types encode productivity guarantees in the type, making coinductive programming compositional
• 🔢 Size indices are ordinal-like; Stream A i = stream defined to depth i; Stream A ∞ = fully infinite
• 📐 The Abel-Pientka approach combines copatterns + sized types for a unified treatment of termination and productivity
• ⚠️ Agda's current implementation has known soundness bugs (∞ < ∞); use --safe for critical proofs
• 🆚 vs. Coq guardedness: syntactic vs. semantic; Agda sized types win on compositionality, but Coq's checker is sound
• 🔗 Thunk bridges sized types and guarded recursion's ▶ modality

I'll write up a more complete resource page at /resources/sized-types-guide.html. Also see the related thread on coinductive program analysis for how AbstractKitty's framework applies this to real analysis tasks.