This content originally appeared on DEV Community and was authored by Shrijith Venkatramana
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
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
A type tells us what kind of value something is.
For example:
List<Int>
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
With dependent types:
values can also appear inside types
That sounds abstract initially, but the examples make it much clearer.
Understanding Vec Nat 3
Suppose you see:
Vec Nat 3
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
So these are different types:
Vec Nat 3
Vec Nat 5
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];
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)
This means:
appending a vector of size
n
to a vector of sizem
produces a vector of sizen + 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)
But there is an implicit rule:
a.columns == b.rows
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
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]
Potential issue:
What if xs is empty?
Usually this becomes:
- a runtime exception,
- a defensive check,
- or a convention.
In Lean-like systems:
head : Vec α (n + 1) → α
This says:
headonly accepts non-empty vectors.
Why?
Because:
n + 1
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
Suppose a user uploads some JSON.
Initially, the data may effectively have a type like:
UntrustedInput
Then validation happens.
After validation, the type changes:
AuthenticatedUser
ValidConfig
NonEmptyList
Vec Nat 3
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
But in many languages, all of them are still just:
String
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
but:
proof + enforcement
That is the deeper shift.
Final Thoughts
When programmers first encounter dependent types, the syntax can look intimidating:
Vec : Type → Nat → Type
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.
HexmosTech
/
git-lrc
Free, Micro AI Code Reviews That Run on Commit
| 🇩🇰 Dansk | 🇪🇸 Español | 🇮🇷 Farsi | 🇫🇮 Suomi | 🇯🇵 日本語 | 🇳🇴 Norsk | 🇵🇹 Português | 🇷🇺 Русский | 🇦🇱 Shqip | 🇨🇳 中文 |
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
git-lrc-intro-60s.mp4See git-lrc catch serious security issues such as leaked credentials, expensive cloud operations, and sensitive material in log statements
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…
This content originally appeared on DEV Community and was authored by Shrijith Venkatramana
Shrijith Venkatramana | Sciencx (2026-05-19T16:52:47+00:00) Dependent Types for Programmers: A Practical Introduction Using Lean 4. Retrieved from https://www.scien.cx/2026/05/19/dependent-types-for-programmers-a-practical-introduction-using-lean-4/
Please log in to upload a file.
There are no updates yet.
Click the Upload button above to add an update.