Okay I need to be direct here because this thread has been going in circles for 3 pages.

My thesis: dependent types cannot be productively taught to undergraduates. And I don't mean "it's hard" — I mean the cost/benefit ratio is negative for the vast majority of CS programs.

Think about what a typical undergrad curriculum looks like. You're fighting to get them to understand:

• What a type is at all
• Why immutability matters
• Basic algebraic data types
• Polymorphism and generics
• Monads (lol) — wait, no, nobody teaches that, that's the problem

And someone in this thread wants to throw Vec A (suc n) at them? Seriously? The cognitive overhead of understanding why your type-level natural number increments when you cons an element is enormous. The tooling feedback is confusing. The error messages look like mathematical notation from a textbook they haven't read. Half the time the typechecker just says the goal is ⊤ and you're supposed to feel good about that.

I've taught intro PL courses. I've watched students' eyes glaze over at GADTs in Haskell. Dependent types would be a full massacre. The juice is not worth the squeeze unless you're specifically training type-theorists — which most of us are NOT doing.

The industry doesn't use Agda. The industry barely uses Haskell. Let's be real.

Wait wait wait.

Vec A n is literally just a monad. Or wait — no — it's a comonad. Or — okay it's a functor at minimum. The point is if you just understood monadic structure first you'd see that dependent types are just a natural extension of —

You know what, I've been thinking about this and the Reader monad and dependent function types are the same thing. The environment IS the index. Prove me wrong. (r → a) ≅ Vec a r if you squint correctly and r is a Fin. This is dependent Reader. I will die on this hill.

Also hi AgdaCat that tutorial is actually really good, I learned something, but monads explain it better and you know it

Quick drive-by to drop a relevant link since nobody has mentioned it yet:

Context for those who haven't suffered through it: HoTT treats types as spaces and equality proofs as paths between points in those spaces. The univalence axiom says that equivalent types ARE equal — not just isomorphic, literally identical from the type theory's perspective.

Is this industry-relevant? Absolutely not. Is it one of the most beautiful things human beings have ever written down? Arguably yes. Does it make PracticalPurr's point for them? ...kind of.

The existence of HoTT is evidence that dependent types can go places that are so far from "writing reliable software" that they loop back around to being a completely different discipline. Know your use case.

Okay. I've read the tutorial three times. I'll concede: the examples are not incomprehensible. The Vec example in particular is genuinely elegant. I get why you love this.

But my point stands on pedagogical grounds — not on "is this cool" grounds. The tutorial you wrote is excellent for people who already understand what problem it's solving. Students who don't have war wounds from null pointer exceptions, segfaults, or array index bugs don't feel the pain that dependent types cure. You're selling ibuprofen to people who haven't had the headache yet.

That said... I'll update my position slightly. Not "can't be taught to undergrads" — maybe "shouldn't be the first type system they encounter, and probably shouldn't be the primary teaching tool." Show them the bug first. THEN show them the cure.

This is what good pedagogy looks like: motivate the pain, then introduce the tool. You might actually have something with a course structured that way.

I want to add some nuance here that I think both sides are gesturing at without quite landing:

There's a real distinction between:

   • Dependent types as a verification tool (Agda, Coq, Lean, Idris)
   • Dependent types as a research/foundations vehicle (HoTT, cubical type theory)
   • Lightweight dependent-ish types in mainstream languages (Rust lifetimes, TypeScript template literals, C++ concepts, Liquid Haskell)

PracticalPurr's criticism applies most strongly to the first two. But the third category is already happening in industry and most people don't even realize they're doing a form of dependent typing. Rust's borrow checker is a specialized dependent type system for memory safety. TypeScript's conditional types and infer keyword are dependently-typed at the type level.

So the question isn't "should we teach dependent types" — it's "at what granularity, in what context, and toward what goal?" AgdaCat's tutorial is great for the research track. A course on Rust or TypeScript already teaches dependent-ish intuitions without the full machinery.

This is actually genuinely good pedagogy advice and I hate that I'm agreeing with you right now.

Okay. New framing that I think is actually true and I'll defend it:

TypeTheoryCat nailed it above. The spectrum from "Rust borrow checker" to "full cubical HoTT" is enormous. Both ends are "dependent types" if you squint.

Coming in late but I think there's an angle everyone's missing: the tooling question is as important as the type theory question.

Dependent types in Agda are powerful but the tooling ecosystem is small. The Emacs mode is good but Emacs has a learning curve. VS Code support exists but is behind. The error messages — as PracticalPurr noted — can be brutal.

Compare to: Rust, where the error messages are legendary for their helpfulness. The borrow checker is a specialized dependent-ish type system and rustc will tell you exactly what's wrong and often how to fix it. That's the model. That's what makes sophisticated type systems teachable and usable.

The path forward for dependent types in industry isn't "everyone learns Agda." It's better error messages, better IDE integration, better inference, and gradual adoption through languages that smuggle dependent-type-like features in wearing a mainstream disguise. TypeScript is already doing this. Kotlin contracts tried. Liquid Haskell exists. F* at Microsoft Research is fascinating.

Dependent types won't arrive in industry as "Agda at work." They'll arrive as features in languages people already use, slowly, quietly, until one day someone realizes their type system has been almost-dependently-typed for years.

Alright. I'll actually formalize my updated position since apparently this thread is converging on something.

I'll admit: AgdaCat's tutorial actually changed my mind about teachability. The examples really are elegant once you have the right frame. And StaticAnalysisSis's tooling point is where I was hiding my real concern — it's not the theory, it's the practice.