DEV Community

Shrijith Venkatramana
Shrijith Venkatramana

Posted on

Dependent Types for Programmers: A Practical Introduction Using Lean 4

#ai #productivity #programming #webdev

Hello, I'm Shrijith Venkatramana. I'm building git-lrc, an AI code reviewer that runs on every commit. Star Us to help devs discover the project. Do give it a try and share your feedback for improving the product.

If you are learning Lean 4, sooner or later you encounter something like this:

Vec : Type → Nat → Type
Enter fullscreen mode Exit fullscreen mode

And suddenly the tutorials start talking about:

  • proofs,
  • propositions,
  • type theory,
  • dependent types,
  • Curry–Howard correspondence.

For many programmers, this is where things become foggy.

The strange thing is that the underlying idea is actually very practical.

Dependent types are fundamentally about this:

making more program assumptions visible to the compiler.

This article builds the idea gradually from an ordinary programmer’s mental model.

The Normal Way We Think About Types

In most languages, we think of types like categories.

42 : Int
"hello" : String
Enter fullscreen mode Exit fullscreen mode

A type tells us what kind of value something is.

For example:

List<Int>
Enter fullscreen mode Exit fullscreen mode

means:

“a list of integers.”

But notice what the type does not tell us:

  • how many integers,
  • whether the list is empty,
  • whether it is sorted,
  • whether it has been validated,
  • whether authentication has happened,
  • whether certain invariants hold.

Those become:

  • comments,
  • runtime checks,
  • tests,
  • conventions,
  • assumptions.

The Core Idea of Dependent Types

Dependent types change one thing:

types are allowed to depend on values.

That is why they are called dependent types.

Normally:

values belong to types
Enter fullscreen mode Exit fullscreen mode

With dependent types:

values can also appear inside types
Enter fullscreen mode Exit fullscreen mode

That sounds abstract initially, but the examples make it much clearer.

Understanding Vec Nat 3

Suppose you see:

Vec Nat 3
Enter fullscreen mode Exit fullscreen mode

This means:

“a vector containing exactly 3 natural numbers.”

Break it apart:

  • Vec → vector type constructor
  • Nat → element type
  • 3 → required length

The important part is this:

the length is part of the type itself
Enter fullscreen mode Exit fullscreen mode

So these are different types:

Vec Nat 3
Vec Nat 5
Enter fullscreen mode Exit fullscreen mode

The compiler can distinguish them.

That is the conceptual shift.

“But C Arrays Already Have Sizes”

Good observation.

C already gets somewhat close:

int arr[3];
Enter fullscreen mode Exit fullscreen mode

So what makes dependent typing different?

The difference is that the values become usable inside the type system itself.

For example:

append : Vec α n → Vec α m → Vec α (n + m)
Enter fullscreen mode Exit fullscreen mode

This means:

appending a vector of size n
to a vector of size m
produces a vector of size n + m

The type system is now reasoning symbolically about values.

That is much more expressive than ordinary static typing.

Why This Matters

Most software bugs are really violations of assumptions.

Consider matrix multiplication.

You might write:

matrixMultiply(a, b)
Enter fullscreen mode Exit fullscreen mode

But there is an implicit rule:

a.columns == b.rows
Enter fullscreen mode Exit fullscreen mode

Normally:

  • you document this,
  • test this,
  • or check it at runtime.

With dependent types, you can encode the relationship structurally:

Matrix m n
Matrix n p
Enter fullscreen mode Exit fullscreen mode

Now invalid multiplication does not typecheck.

The compiler understands the invariant itself.

That is the real promise of dependent typing:

move important assumptions from comments into machine-checked structure.

Non-Empty Lists

Here is another example.

In ordinary programming:

def head(xs):
    return xs[0]
Enter fullscreen mode Exit fullscreen mode

Potential issue:

What if xs is empty?
Enter fullscreen mode Exit fullscreen mode

Usually this becomes:

  • a runtime exception,
  • a defensive check,
  • or a convention.

In Lean-like systems:

head : Vec α (n + 1) → α
Enter fullscreen mode Exit fullscreen mode

This says:

head only accepts non-empty vectors.

Why?

Because:

n + 1
Enter fullscreen mode Exit fullscreen mode

can never be zero.

The impossible case disappears from the program structure entirely.

“But Real Programs Use Dynamic User Input”

This is one of the most common misunderstandings.

People often assume dependent typing only helps when everything is known at compile time.

But in practice, the workflow is usually:

dynamic validation
        ↓
static guarantee afterward
Enter fullscreen mode Exit fullscreen mode

Suppose a user uploads some JSON.

Initially, the data may effectively have a type like:

UntrustedInput
Enter fullscreen mode Exit fullscreen mode

Then validation happens.

After validation, the type changes:

AuthenticatedUser
ValidConfig
NonEmptyList
Vec Nat 3
Enter fullscreen mode Exit fullscreen mode

The important idea is this:

once something has been checked, the type system remembers the fact.

That is incredibly useful.

Real-World Intuition

Many systems already rely on informal “refined” types.

For example, programmers mentally distinguish between:

raw string
validated email
escaped SQL
sanitized HTML
authenticated user
Enter fullscreen mode Exit fullscreen mode

But in many languages, all of them are still just:

String
Enter fullscreen mode Exit fullscreen mode

Dependent typing allows those distinctions to become explicit and enforceable.

What Lean Is Really Exploring

Lean is often presented as:

  • a theorem prover,
  • a mathematical tool,
  • or a proof assistant.

But from a programmer’s perspective, a more useful framing is:

Lean explores what happens when program invariants become part of the language itself.

Not:

comments + conventions + hope
Enter fullscreen mode Exit fullscreen mode

but:

proof + enforcement
Enter fullscreen mode Exit fullscreen mode

That is the deeper shift.

Final Thoughts

When programmers first encounter dependent types, the syntax can look intimidating:

Vec : Type → Nat → Type
Enter fullscreen mode Exit fullscreen mode

But the underlying idea is surprisingly concrete.

Dependent types are about expressing richer facts directly in the type system:

  • sizes,
  • protocol states,
  • validation status,
  • permissions,
  • invariants,
  • safety guarantees.

And once those facts become part of the type system, entire classes of bugs become much harder to represent.

That is why languages like Lean are interesting even beyond theorem proving.

They are exploring a different model of software correctness itself.

*AI agents write code fast. They also silently remove logic, change behavior, and introduce bugs -- without telling you. You often find out in production.

git-lrc fixes this. It hooks into git commit and reviews every diff before it lands. 60-second setup. Completely free.*

Any feedback or contributors are welcome! It's online, source-available, and ready for anyone to use.

GitHub logo HexmosTech / git-lrc

Free, Micro AI Code Reviews That Run on Commit



AI agents write code fast. They also silently remove logic, change behavior, and introduce bugs -- without telling you. You often find out in production.

git-lrc fixes this. It hooks into git commit and reviews every diff before it lands. 60-second setup. Completely free.

See It In Action

See git-lrc catch serious security issues such as leaked credentials, expensive cloud operations, and sensitive material in log statements

git-lrc-intro-60s.mp4

Why

  • 🤖 AI agents silently break things. Code removed. Logic changed. Edge cases gone. You won't notice until production.
  • 🔍 Catch it before it ships. AI-powered inline comments show you exactly what changed and what looks wrong.
  • 🔁 Build a…
View on GitHub

Top comments (0)