Intrinsically Typed Interpreters in Agda — a walkthrough

🐾

AgdaAdorer

✦ Sigma Type Senpai

Posts: 1,423
Joined: 3 yrs ago
Rep: ★★★★★

🦄 AGDA WIZARD

📜 PLFA CERTIFIED

📖 [WALKTHROUGH] Intrinsically Typed Interpreters in Agda 2025-03-15 · 09:14 UTC #1 🔗

Hewwo everyone!! 🐱✨ I've been wanting to write this up for a while and finally found time. This is a walkthrough of how to write intrinsically typed (also called well-scoped, well-typed) interpreters in Agda, where the Agda type system itself enforces the object language's type system. No separate type safety proof needed — it's correct by construction!

I'll assume you know basic Agda syntax and have some familiarity with dependent types. If not, go read PLFA first!! (The DeBruijn chapter is especially relevant here.)

§1 — What does "intrinsic" even mean?

There are two broad approaches to mechanising a typed language:

Extrinsic (a.k.a. à la Church/raw terms): define an untyped AST first, then write a separate typing relation, then separately prove type safety.
Intrinsic (a.k.a. à la Curry/typing derivations): bake the types directly into the AST so that only well-typed terms can be constructed.

With the intrinsic approach, Γ ⊢ A is the type of terms that have type A in context Γ. There are no ill-typed terms — they simply don't exist as values of this type. The Agda type-checker is doing all the work for you.

Key insight: Poulsen et al. (POPL 2018) put it well — using intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. No separate proof needed!

§2 — The Object Language: STLC with ℕ

We'll interpret the Simply Typed Lambda Calculus with natural numbers. First, let's define the types of our object language:

-- Object-language types data Ty : Set where ℕ̂ : Ty _⇒_ : Ty → Ty → Ty -- Typing contexts are snoc-lists of types Ctx : Set Ctx = List Ty -- De Bruijn variables: a proof that type A is in context Γ data _∈_ : Ty → Ctx → Set where here : ∀ {A Γ} → A ∈ (A ∷ Γ) there : ∀ {A B Γ} → A ∈ Γ → A ∈ (B ∷ Γ)

Now the intrinsically typed term representation. Notice how the type and context are indices of the _⊢_ datatype — a value of type Γ ⊢ A is by definition a term of type A in context Γ:

-- Intrinsically typed terms: Γ ⊢ A means "a term of type A in context Γ" data _⊢_ : Ctx → Ty → Set where -- Variables: a proof that A appears in context Γ `_ : ∀ {Γ A} → A ∈ Γ → Γ ⊢ A -- Lambda abstraction ƛ_ : ∀ {Γ A B} → (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B) -- Application _·_ : ∀ {Γ A B} → Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B -- Natural number literal `ℕ : ∀ {Γ} → ℕ → Γ ⊢ ℕ̂ -- Successor `suc : ∀ {Γ} → Γ ⊢ ℕ̂ → Γ ⊢ ℕ̂

The beautiful thing: you simply cannot construct a term Γ ⊢ A that is ill-typed. The type indices prevent it at Agda's compile time! 🎉

§3 — The Semantic Domain

We need to interpret object-language types as Agda types. We use a function ⟦_⟧ᵀ:

-- Interpret object-language types as Agda types ⟦_⟧ᵀ : Ty → Set ⟦ ℕ̂ ⟧ᵀ = ℕ ⟦ A ⇒ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ -- Environments: a mapping from each variable to its semantic value data Env : Ctx → Set where [] : Env [] _∷_ : ∀ {A Γ} → ⟦ A ⟧ᵀ → Env Γ → Env (A ∷ Γ) -- Look up a variable in an environment lookup : ∀ {Γ A} → A ∈ Γ → Env Γ → ⟦ A ⟧ᵀ lookup here (v ∷ _) = v lookup (there x) (_ ∷ ρ) = lookup x ρ

§4 — The Interpreter

And here it is — the payoff! The interpreter eval maps a well-typed term in an environment to a value in the semantic domain. The type signature says it all:

-- The interpreter: type-safe by construction! eval : ∀ {Γ A} → Γ ⊢ A → Env Γ → ⟦ A ⟧ᵀ eval (` x) ρ = lookup x ρ eval (ƛ t) ρ = λ v → eval t (v ∷ ρ) eval (f · a) ρ = eval f ρ (eval a ρ) eval (`ℕ n) ρ = n eval (`suc t) ρ = suc (eval t ρ)

Look at how tiny this is! No error cases, no Maybe, no partial functions. Every case is total and obviously terminating. The type safety guarantee isn't proved — it's witnessed by the type of eval itself.

In the next posts I'll talk about the comparison with extrinsic typing and we can discuss the trade-offs! 🐾

❤️ 34 🐱 28 💜 19 🤯 12 ✨ 22

Quote Edit Report

🐈

IntrinsicNeko

◆ Dependent Cutie

Posts: 892
Joined: 2 yrs ago
Rep: ★★★★☆

🌸 NEKO MODE

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 09:52 UTC #2 🔗

omg AgdaAdorer I've been waiting for someone to write this up properly!! 🐾💕

Something I want to highlight for readers who are seeing this for the first time: the key insight is in the type of lookup. Compare these two versions:

-- Extrinsic version: can fail! Returns Maybe lookupEx : ℕ → List Val → Maybe Val lookupEx zero (x ∷ _) = just x lookupEx (suc n) (_ ∷ xs) = lookupEx n xs lookupEx _ [] = nothing -- 😱 out-of-bounds! -- Intrinsic version: TOTAL, no Maybe needed lookup : ∀ {Γ A} → A ∈ Γ → Env Γ → ⟦ A ⟧ᵀ lookup here (v ∷ _) = v -- always succeeds! lookup (there i) (_ ∷ ρ) = lookup i ρ

The A ∈ Γ proof acts as a statically verified index into the environment. Since the proof only exists when A really is in Γ, the empty-list case is impossible and Agda knows it — no need to handle it!

❤️ 21 ✨ 15

Quote Report

👻

GhostlyGADT

◇ Phantom Indexer

Posts: 2,105
Joined: 4 yrs ago
Rep: ★★★★★

👻 GADT GHOST

🔮 INDEXED

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 10:31 UTC #3 🔗

Great thread! Want to add some historical/theoretical context since we're being thorough ✨

The intrinsic approach traces back to Reynolds, who distinguished intrinsic semantics (meaning assigned to typing judgments) from extrinsic semantics (meaning assigned to raw program phrases, including ill-typed ones). In Agda, this philosophy maps directly onto indexed datatypes.

The connection to GADTs in Haskell is also worth mentioning! In Haskell, you'd write something like:

-- Haskell GADT version (for comparison) data Expr env t where Var :: Elem env t → Expr env t Lam :: Expr (a, env) b → Expr env (a -> b) App :: Expr env (a -> b) → Expr env a → Expr env b Lit :: Int → Expr env Int

The Agda version is more powerful because Env can be truly heterogeneous via dependent types — each slot in the environment has a different Agda type corresponding to its object-language type, tracked precisely by the index. In Haskell, this requires tricks like HList.

Also, totality in Agda means the interpreter provably terminates — something Haskell can't guarantee. So you get a proper denotational semantics, not just a function that might loop.

💜 18 🤓 14 👻 9

Quote Report

🌸

TotallyTyped

✿ Termination Chan

Posts: 561
Joined: 1 yr ago
Rep: ★★★☆☆

🌿 TOTAL FN LOVER

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 11:08 UTC #4 🔗

Quick question!! When we interpret a language with recursion (like PCF), the interpreter can't be total anymore right? How do you handle that with the intrinsic approach? uwu

AgdaAdorer wrote:

Every case is total and obviously terminating.

That's true for STLC, which strongly normalises. But I've seen people add a "fuel" or "step counter" argument to handle potentially diverging languages. Does that break the elegance?

❓ 7 💭 5

Quote Report

🐾

AgdaAdorer

✦ Sigma Type Senpai

Posts: 1,423
Joined: 3 yrs ago
Rep: ★★★★★

🦄 AGDA WIZARD

Re: Intrinsically Typed Interpreters in Agda [OP] 2025-03-15 · 11:45 UTC #5 🔗

TotallyTyped wrote:

Does adding a fuel counter break the elegance?

Great question TotallyTyped!! 🌸 The fuel / step-counter trick is the standard solution. You add a ℕ parameter representing how many steps remain, and return a Maybe result:

-- Interpreter for a language with potential non-termination data Ty : Set where ℕ̂ : Ty _⇒_ : Ty → Ty → Ty μ_ : Ty → Ty -- recursive types eval : ∀ {Γ A} → ℕ -- fuel → Γ ⊢ A → Env Γ → Maybe ⟦ A ⟧ᵀ eval zero _ _ = nothing -- out of fuel eval (suc n) (` x) ρ = just (lookup x ρ) eval (suc n) (ƛ t) ρ = just (λ v → eval n t (v ∷ ρ)) eval (suc n) (f · a) ρ with eval n f ρ | eval n a ρ eval (suc n) (f · a) ρ | just fv | just av = fv av eval (suc n) (f · a) ρ | _ | _ = nothing

The key point: the typing invariant is still enforced intrinsically! The Maybe only captures "ran out of fuel" — it never represents a type error. If the computation does complete, the result is guaranteed to have the right type. The nothing branch purely means "timed out."

For terminating fragments (STLC, System T, etc.), you don't need the fuel at all. For general recursion, you need it — but you don't lose the type safety guarantee, just totality of the interpreter itself.

There's also the approach using coinduction / corecursion in Agda (via Conat / partiality monads) for a smoother presentation. The Delay monad by Capretta, or the partiality monad of Danielsson, are popular choices here!

❤️ 27 ✨ 20 🐱 16

Quote Edit Report

👻

GhostlyGADT

◇ Phantom Indexer

Posts: 2,105
Joined: 4 yrs ago
Rep: ★★★★★

👻 GADT GHOST

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 12:20 UTC #6 🔗

On the extrinsic vs intrinsic trade-offs — want to be a bit of a devil's advocate here 👻

Intrinsic typing is wonderful but it has some real pain points worth knowing:

Substitution is hard. In the extrinsic setting, substitution is just a function on raw terms. Intrinsically, you need to prove substitution preserves types — and this gets gnarly fast. You end up with things like simultaneous substitutions (renamings, weakenings) that require careful treatment.
Languages with dependent types as object languages are particularly painful because object-level type equality bleeds into the meta-level. Definitional equality issues arise.
Parsing / elaboration. Your parser still works on raw strings! You have to elaborate raw terms into typed ones, which requires writing a type-checker that produces typing derivations. That's essentially a separate proof anyway.

That said, for clean STLC-like languages that are the subject of a PL formalization, intrinsic is almost always worth it. The Agda community consensus seems to be: intrinsic where possible, extrinsic only when the object language makes it too painful.

See also Allais et al. "A type and scope safe universe of syntaxes with binding" (ICFP 2018) for a very general framework!

💜 13 🤔 8 👻 6

Quote Report

🐈

IntrinsicNeko

◆ Dependent Cutie

Posts: 892
Joined: 2 yrs ago
Rep: ★★★★☆

🌸 NEKO MODE

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 13:04 UTC #7 🔗

GhostlyGADT wrote:

Substitution is hard. In the extrinsic setting, substitution is just a function on raw terms.

Yes!! This is where PLFA's DeBruijn chapter earns its keep. The substitution lemma for intrinsically-typed STLC goes through a simultaneous substitution / renaming approach:

-- Renaming: map variables under context extension Rename : Ctx → Ctx → Set Rename Γ Δ = ∀ {A} → A ∈ Γ → A ∈ Δ rename : ∀ {Γ Δ A} → Rename Γ Δ → Γ ⊢ A → Δ ⊢ A rename ρ (` x) = ` ρ x rename ρ (ƛ t) = ƛ rename (ext ρ) t rename ρ (f · a) = rename ρ f · rename ρ a rename ρ (`ℕ n) = `ℕ n rename ρ (`suc t) = `suc (rename ρ t) -- Extend renaming under a binder ext : ∀ {Γ Δ B} → Rename Γ Δ → Rename (B ∷ Γ) (B ∷ Δ) ext ρ here = here ext ρ (there x) = there (ρ x) -- Simultaneous substitution Subst : Ctx → Ctx → Set Subst Γ Δ = ∀ {A} → A ∈ Γ → Δ ⊢ A

It's more machinery than raw-terms substitution, but once it's built, it's shockingly reusable. The renaming/substitution framework is basically generic across all STLC-like languages.

✨ 16 ❤️ 11

Quote Report

🌸

TotallyTyped

✿ Termination Chan

Posts: 561
Joined: 1 yr ago
Rep: ★★★☆☆

🌿 TOTAL FN LOVER

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 13:55 UTC #8 🔗

Thank you for the fuel explanation AgdaAdorer!! That makes total sense now 🌸

Can I ask about normalisation by evaluation (NbE) in the intrinsic setting? Is the approach similar? I know NbE is related to interpreters but I keep getting confused about what the "semantic domain" looks like when you're going back to normal forms...

💭 8 🌸 4

Quote Report

🐾

AgdaAdorer

✦ Sigma Type Senpai

Posts: 1,423
Joined: 3 yrs ago
Rep: ★★★★★

🦄 AGDA WIZARD

Re: NbE in the intrinsic setting [OP] 2025-03-15 · 14:30 UTC #9 🔗

NbE (Normalisation by Evaluation) is a natural extension of the intrinsic interpreter! 🌟 The idea is that instead of evaluating into plain Agda values, you evaluate into a semantic domain that contains "neutral" stuck terms (unreducible applications to free variables). Then you "quote" back into normal forms.

In the intrinsic setting, the semantic domain is stratified by type:

-- Normal forms and neutral terms (intrinsically typed) mutual data Nf : Ctx → Ty → Set where nf-lam : ∀ {Γ A B} → Nf (A ∷ Γ) B → Nf Γ (A ⇒ B) nf-ne : ∀ {Γ} → Ne Γ ℕ̂ → Nf Γ ℕ̂ nf-ℕ : ∀ {Γ} → ℕ → Nf Γ ℕ̂ -- Neutrals: variable applied to arguments data Ne : Ctx → Ty → Set where ne-var : ∀ {Γ A} → A ∈ Γ → Ne Γ A ne-app : ∀ {Γ A B} → Ne Γ (A ⇒ B) → Nf Γ A → Ne Γ B -- Semantic domain: Agda functions at function type, Nf at base type ⟦_⟧ᴺ : Ty → Ctx → Set ⟦ ℕ̂ ⟧ᴺ Γ = Nf Γ ℕ̂ ⟦ A ⇒ B ⟧ᴺ Γ = ∀ {Δ} → Γ ⊆ Δ → ⟦ A ⟧ᴺ Δ → ⟦ B ⟧ᴺ Δ

The Γ ⊆ Δ (weakening / thinning) in the function case is the key trick — it lets you pass semantic values through renamings so they can absorb new free variables. This is called the Kripke semantics trick!

For a full intrinsic NbE in Agda, check out Andreas Abel's work on normalization by evaluation, or the PLFA chapters on properties! It's absolutely gorgeous when it comes together 🥹✨

🤯 24 ❤️ 19 ✨ 17

Quote Edit Report

👻

GhostlyGADT

◇ Phantom Indexer

Posts: 2,105
Joined: 4 yrs ago
Rep: ★★★★★

👻 GADT GHOST

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 15:10 UTC #10 🔗

Want to mention the PLFA DeBruijn chapter explicitly since TotallyTyped mentioned they're new to this — it's the single best resource for learning intrinsic typing in Agda from scratch. It starts with a raw term representation and then pivots to the full intrinsic treatment side by side, so you really see what changes.

Direct link: plfa.inf.ed.ac.uk — DeBruijn chapter

Also: for people who want to see this scale up to mutable state and references (not just pure lambda calculi), the POPL 2018 paper "Intrinsically-typed definitional interpreters for imperative languages" by Poulsen et al. is a must-read. They scale up the technique using scope graphs and frames to handle things like:

Mutable references (STLC + Ref)
Imperative objects with subtyping (Middleweight Java)
Store-passing / heap-indexed monads

📚 11 💜 9

Quote Report

🐈

IntrinsicNeko

◆ Dependent Cutie

Posts: 892
Joined: 2 yrs ago
Rep: ★★★★☆

🌸 NEKO MODE

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 16:02 UTC #11 🔗

One more thing I want to add for completeness — the Allais et al. "Type and scope safe programs and their proofs" (ICFP 2018) paper is worth mentioning! They define a generic framework called syntaxes with binding that abstracts over the kind of semantic traversal (renaming, substitution, printing, evaluation, NbE...) in a single universe. It's basically the "final boss" of intrinsically-typed STLC formalizations 👻✨

With their setup, you define your syntax once and get all traversals for free as instances of a generic fold. Super elegant but requires knowing your way around universe polymorphism and record-based abstraction in Agda.

Speaking of which — has anyone done a walkthrough of universe polymorphism on this forum? That would pair really nicely with this thread UwU

🌸 14 ✨ 12

Quote Report

🌸

TotallyTyped

✿ Termination Chan

Posts: 561
Joined: 1 yr ago
Rep: ★★★☆☆

🌿 TOTAL FN LOVER

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 17:20 UTC #12 🔗

Okay I tried implementing this myself following AgdaAdorer's post and I got confused at one point — when writing the ƛ case of eval, is there a reason the lambda returns an Agda function ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ rather than closing over the environment?

-- AgdaAdorer wrote: eval (ƛ t) ρ = λ v → eval t (v ∷ ρ) -- Why isn't it: eval (ƛ t) ρ = closure (t, ρ)?

I'm used to writing eval as producing an explicit Val type that has a closure case... is this "higher-order abstract syntax" or something different?

❓ 6

Quote Report

🐾

AgdaAdorer

✦ Sigma Type Senpai

Posts: 1,423
Joined: 3 yrs ago
Rep: ★★★★★

🦄 AGDA WIZARD

Re: Closures vs. HOAS [OP] 2025-03-15 · 18:05 UTC #13 🔗

TotallyTyped wrote:

Why isn't it: eval (ƛ t) ρ = closure (t, ρ)?

Great catch!! 🐾 This is one of the most elegant aspects of the approach — we're using Higher-Order Abstract Syntax (HOAS), or more precisely, we're representing object-level functions as Agda functions directly.

When our semantic domain for function types is just ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ (an Agda function), we let Agda handle the closure for us. The lambda λ v → eval t (v ∷ ρ) IS the closure — ρ is captured by Agda's own closure mechanism!

This is actually a major advantage: we don't need to implement environments, closures, or closure conversion at the meta-level at all. We inherit these from Agda. This is sometimes called a "definitional interpreter" style:

-- Explicit closure Val approach (more work!) data Val : Ty → Set where num : ℕ → Val ℕ̂ clo : ∀ {Γ A B} → (A ∷ Γ) ⊢ B → Env Γ → Val (A ⇒ B) -- vs. our approach: just use ⟦_⟧ᵀ directly as Agda functions! -- ⟦ A ⇒ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ ← Agda function, no Val needed

The explicit closure approach is fine and sometimes necessary (e.g., when you want to print/serialise closures, or when the host language doesn't have good enough closures). But for the purposes of a clean semantic model, the Agda-function approach is much more beautiful 🌸

❤️ 22 🤯 18 ✨ 15

Quote Edit Report

👻

GhostlyGADT

◇ Phantom Indexer

Posts: 2,105
Joined: 4 yrs ago
Rep: ★★★★★

👻 GADT GHOST

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 19:44 UTC #14 🔗

Phenomenal thread. Bookmarked and linking in the Recommended Reading wiki immediately 👻

Quick summary of the key takeaways for anyone skimming:

🐾 Intrinsic typing encodes object-language types as Agda indices — ill-typed terms literally cannot be constructed.
💜 De Bruijn variables as membership proofs (A ∈ Γ) make lookup total — no Maybe.
🌸 The interpreter eval : Γ ⊢ A → Env Γ → ⟦ A ⟧ᵀ is type-safe by construction — no separate proof!
✨ Fuel/step-counters handle non-terminating languages while preserving the typing guarantee.
👻 Trade-offs exist: substitution is harder, elaboration is needed, dependent object languages are painful.

📌 20 ❤️ 17 💜 13

Quote Report

🐈

IntrinsicNeko

◆ Dependent Cutie

Posts: 892
Joined: 2 yrs ago
Rep: ★★★★☆

🌸 NEKO MODE

Re: Intrinsically Typed Interpreters in Agda 2025-03-15 · 21:37 UTC #15 🔗

Agreed with GhostlyGADT, this is one of the best threads we've had this quarter! 🐈💕 @AgdaAdorer — any chance of a follow-up post covering bidirectional type-checking to elaborate raw terms into these intrinsically-typed terms? That would complete the pipeline perfectly: parse → elaborate (bidirectional) → intrinsically-typed eval!

Also linking relevant threads for newcomers: Dependent Types Crash Course · PLFA Reading Group · Agda Setup Guide for Beginners

🐱 16 🌸 12

Quote Report

🐱 Intrinsically Typed Interpreters in Agda — a walkthrough