GADTs: Dependent Types at Home? Or a Poor Substitute?

Alright, I want to finally have the argument we've been dancing around in multiple threads. Are GADTs in Haskell/OCaml actually sufficient for most dependent typing needs, or are they just a poor imitation that leaves you reaching for singletons, type families, and a bottle of painkillers?

Let me start with the canonical example everyone reaches for. Here's a well-typed expression AST in Haskell:

This is genuinely powerful! The type system guarantees that If branches always have matching types and that Add only accepts integer sub-expressions. You literally cannot construct an ill-typed term — the GADT enforces it.

But here's where I want to push: does this scale to what you'd want real dependent types for? What about length-indexed vectors where head is provably safe? What about a type that depends on a runtime value?

My thesis: GADTs are great for about 70% of the use cases people reach for dependent types to solve. The remaining 30% requires something like Agda/Lean/Idris — and trying to fake it in Haskell with DataKinds + singletons is masochism. Discuss.

I'd argue your 70% figure is optimistic specifically because it ignores the ergonomics cost. The ceiling hit with GADTs isn't just expressiveness — it's that the accidental complexity explodes the moment you try to go beyond type-indexed types.

The classic example: length-indexed vectors. In Agda this is trivial:

In Haskell you get very close with DataKinds + GADTs but there's a crucial difference:

This works! But notice: the Nat in Haskell's version lives at the type level, not the value level. The moment you need to compute the length from a runtime value, you're reaching for singletons and the whole house of cards collapses into ceremony.

In Agda, terms and types live in the same universe. In Haskell, the term/type distinction is enforced and GADTs can only paper over it, not eliminate it. That's the fundamental gap.

Coming at this from the OCaml side — OCaml has had native GADT support since version 4.00, and I want to push back on the idea that "GADTs can't do state machines well." They absolutely can, and it's one of the cleanest uses!

The compiler will reject any invalid transition at compile time. You can't call CloseConn on a Closed connection — it's a type error. This is exactly the kind of invariant enforcement GADTs were made for.

One thing that trips people up: OCaml requires those type a b. locally abstract type annotations when working with GADTs in recursive functions. The inference doesn't always figure it out automatically. Minor papercut but it's worth knowing about upfront.

Great thread. Let me lay out what I think the actual hierarchy is, because people keep conflating three separate things:

1. Phantom Types
Just a type parameter that doesn't appear at runtime. Zero overhead, zero extra power. Useful for tagging (e.g. Tagged Celsius Float vs Tagged Fahrenheit Float). You don't even need GADTs for these.

2. GADTs
Allow constructors to refine the type index. Pattern matching causes type refinement — when you match a constructor, the type checker learns more specific information. This is the key mechanic. Great for typed ASTs, safe heterogeneous containers, and typed state machines as TabbyMonad showed.

3. Full Dependent Types (Agda/Lean/Idris)
Types can contain arbitrary terms. A function's return type can depend on a runtime value. You can express theorems and carry proofs as values. This is a fundamentally different tier.

The key distinction that most people miss: GADTs let you index types by types. Dependent types let you index types by values. In Haskell's GADTs, your type indices are always types (or type-level literals). You can't write a type that says "a vector of exactly n elements where n is this specific runtime Int." You need the singleton machinery to bridge the gap.

This is the clearest formulation I've seen of the distinction. But I want to push on one thing: how often does the average Haskell programmer actually need value-level type dependencies vs. type-level type dependencies?

I'd argue most real-world use cases fall into the GADT bucket. The GHC roadmap even acknowledges that the existing extensions (DataKinds, PolyKinds, TypeFamilies, GADTs) let you emulate dependent types, but the compile-time and run-time costs of these techniques, as well as the associated accidental complexity, limit their applicability in practice.

The Dependent Haskell effort aims to fix this properly — eventually we'll have proper Σ-types and Π-types in Haskell. Until then, GADTs are the best tool we have in production Haskell, and they're genuinely excellent for a wide range of problems.

The question is: should you reach for Agda when GADTs aren't enough, or should you try to fight Haskell's type system harder with singletons?

Reach for Agda. Every time. Don't fight Haskell.

I say this as someone who spent six months trying to encode a type-safe interpreter with full type-preservation guarantees in Haskell. The singletons library is impressive engineering, but look at what you have to write:

The Agda version uses Fin (length xs) as the index type — the second parameter's type literally depends on the value of the first. In Haskell you need the Demote type family to map type-level encodings to their term-level counterparts. It's possible, but it's never simple.

What kills me is the dual-maintenance problem: if your proofs need to match your production code, you end up using Agda for modelling and formal verification, and then reimplementing the same functionality in Haskell. That's not a win. The whole point of types-as-proofs is that you only write it once.

Lurker here, finally posting because I think there's a practical angle being missed: for most production code, GADTs are strictly better than full dependent types because inference still works!

One of the big differences between Haskell and Agda: due to Agda's more expressive type system, type inference is woefully undecidable. Those top-level signatures aren't optional in Agda. In Haskell with GADTs, GHC can still infer a lot for you. You pay less annotation tax.

Also: GHC can compile to fast native code. Agda compiles via Haskell. Lean4 is better but still not as mature an ecosystem. For shipping production software that needs some type-level invariants but not Curry-Howard proofs, GADTs in Haskell/OCaml are the pragmatic choice.

The GADT sweet spot IMO:
✓ Typed ASTs / interpreters
✓ Protocol state machines
✓ Heterogeneous collections (existentials)
✓ Type-safe printf / format strings
✓ Safe list operations (non-empty lists, etc.)
✗ Arbitrary arithmetic on lengths at type level
✗ Proofs about program correctness
✗ Anything requiring value-level → type-level reflection at runtime

Fair point on inference ergonomics. But I want to flag one more subtle and important distinction: GADTs in Haskell are similar to inductive families in Agda/Coq — but only modulo dependent types.

Specifically, GADTs are similar to the inductive families of data types found in dependently typed languages, except that the latter have an additional positivity restriction which is not enforced in GADTs. You can write GADTs that would be rejected in Agda for violating the positivity condition, and those types could allow you to write non-terminating programs or even exploitable unsoundness.

Agda enforces totality — all functions must terminate and all pattern matches must be exhaustive. This makes Agda programs actual proofs, not just type-annotated programs. Haskell's laziness and undefined mean that "it typechecks" and "it's correct" are never the same statement in the same way.

So: GADTs give you a taste of the good stuff, but without the totality checker, you can still write lies. The type-as-proof analogy only fully holds in a total language.

Scala 3 perspective incoming: Scala 3.0 introduced the possibility to write GADTs with the same syntax as algebraic data types, which is actually genuinely ergonomic compared to Haskell's where-clause syntax. Odersky made a big deal of this.

But honestly even in Scala 3, GADTs feel like a power user feature. The type inference story is even more fraught than Haskell's. I've hit cases where the compiler just gives up and you need absurd type annotations.

The thing I appreciate about the OCaml approach (as TabbyMonad showed) is that the locally abstract type annotation pattern at least makes the failure mode explicit — you know exactly when you need to help the typer. In Scala you get these long chains of "expected X but got Y" errors that take forever to decipher.

For the original question though: I think GADTs are "dependent types at home" in the same way that a microwave is "an oven at home." Useful! Gets the job done 80% of the time! But don't try to bake a soufflé in it. (The soufflé is a total correctness proof.)

Let me add the embedding angle since nobody's mentioned it yet. One of GADTs' most powerful applications is embedding other languages in a type-safe way — higher-order abstract syntax (HOAS).

This is genuinely the killer app for GADTs: the App constructor enforces that the function type and argument type are compatible. It's impossible to construct an ill-typed lambda term using this representation. The GADT embeds the object language's type system into the host language's type system.

For this use case, full dependent types would give you no additional expressiveness. GADTs are the right tool. The debate only starts when you need to reason about the languages you're embedding — at which point you want Agda's equational reasoning. Different tools for different jobs, nya~.

MittensML's microwave analogy is sending me. I'm putting that in my conference talk slides with full credit.

Let me try to synthesize where we've landed so far before the thread inevitably goes 156 posts deep:

GADTs excel at: typed ASTs, HOAS embedding, state machine encoding, safe heterogeneous containers, format strings (fun with phantom types!), EDSL design where you want Haskell's type system to enforce your DSL's type system.

GADTs strain at: runtime-to-type reflection (needs singletons), length-indexed operations with runtime-variable lengths, anything requiring type-level arithmetic proofs.

GADTs fail at: full proof-relevant programming, propositional equality proofs, structural induction on type families, anything requiring totality checking.

The real answer to the thread title: GADTs are not dependent types at home. They are their own genuinely powerful thing that overlaps with ~60-70% of dependent type use cases. Calling them "poor substitutes" is uncharitable; calling them "sufficient substitutes" is wrong. They are a distinct and valuable tool. nya~