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.
Most developers think of type systems as glorified linting.
-
stringvsnumber - nullable vs non-nullable
- maybe some autocomplete
But in Lean, a type can encode an actual logical property.
Not:
“this variable is a string”
but:
“this string is guaranteed to be non-empty.”
And once that guarantee exists, invalid states become literally unrepresentable.
This is where type inhabitation enters the picture.
1. What Does “Type Inhabitation” Mean?
A type is inhabited if you can construct a value of that type.
For example:
#check Nat
Nat is inhabited because values like:
0
1
42
exist.
Similarly:
#check True
is inhabited because Lean has a proof of True.
But:
#check False
is uninhabited.
There is no valid value of type False.
In Lean, programs and proofs collapse into the same thing:
| Logic | Programming |
|---|---|
| proposition | type |
| proof | value/program |
| proving | constructing |
So asking:
“Can this theorem be proven?”
becomes:
“Can this type be inhabited?”
That sounds abstract until you realize it applies directly to ordinary software.
2. The “Hello {name}” Problem
Suppose you write:
function greet(name: string) {
return `Hello ${name}`
}
What assumptions exist here?
Hidden ones:
-
nameshould not be empty - maybe it should be trimmed
- maybe length-bounded
- maybe validated UTF-8
- maybe sanitized
But the type says only:
string
So the real semantics live:
- in comments,
- conventions,
- tribal knowledge,
- or bugs.
In Lean, we can move the invariant into the type itself.
3. A String That Cannot Be Empty
Here’s a refined type:
structure NonEmptyString where
value : String
proof : value.length > 0
This says:
A NonEmptyString consists of:
- a string value
- proof that the string length is greater than zero
Now this becomes impossible:
⟨"", ?proof⟩
because no proof exists that:
"".length > 0
So Lean rejects construction entirely.
That’s the key idea:
invalid states become uninhabitable.
4. But Real Programs Are Dynamic
At this point most developers ask:
“How can the compiler prove user input is non-empty?”
It usually cannot.
If the input comes from:
- a form,
- database,
- API,
- terminal,
- environment variable,
then the value is only known at runtime.
So the trick is different.
We:
- validate dynamically once,
- convert into a stronger type,
- carry guarantees statically afterward.
This pattern is sometimes called:
Parse, don’t validate.
5. The Smart Constructor
Here’s the canonical approach:
def mkNonEmpty (s : String) : Option NonEmptyString :=
if h : s.length > 0 then
some ⟨s, h⟩
else
none
Let’s unpack this carefully.
The Option Type
Option α means:
Either:
- some α
- or none
Like:
- Rust’s
Option<T> - Haskell’s
Maybe - TypeScript’s
T | undefined
So:
some x
means:
successful construction
while:
none
means:
validation failed
What Does ⟨s, h⟩ Mean?
This constructs the structure itself.
Equivalent to:
{
value := s,
proof := h
}
So:
⟨s, h⟩
creates a valid NonEmptyString.
Then:
some ⟨s, h⟩
wraps it into Option.
6. Why This Actually Matters
Now we can write:
def greeting (name : NonEmptyString) : String :=
s!"Hello {name.value}"
Notice what disappeared:
- null checks
- empty checks
- defensive programming
- comments explaining assumptions
The invariant is now encoded in the type system.
This is a major shift.
Without refinement types:
function greet(name: string)
every caller must remember the rules.
With refined types:
greeting : NonEmptyString → String
the compiler enforces the rules automatically.
7. The Bigger Idea Behind Type Inhabitation
The deeper point is not “empty strings are bad.”
It is this:
Types can describe semantic reality, not just memory layout.
A few examples:
| Type | Invariant |
|---|---|
NonEmptyString |
string is non-empty |
Fin n |
integer is < n
|
AuthenticatedUser |
login already verified |
NonZeroFloat |
safe divisor |
SortedList |
ordering preserved |
VerifiedJWT |
cryptographically validated |
In all these cases:
- raw input enters the system,
- validation happens once,
- stronger types preserve guarantees afterward.
The type system becomes an architecture for trust propagation.
That is far more interesting than “strong typing” in the ordinary sense.
Final Thought
Most codebases are full of invisible assumptions:
- “this should never be null”
- “this list should never be empty”
- “this user should already be authenticated”
- “this index should be in bounds”
Traditional programming treats these as conventions.
Dependent type systems ask a more radical question:
What if invalid states could not even exist?
And once you start thinking that way, ordinary type systems begin to feel strangely underpowered.
What assumptions in your current codebase could become types instead?
*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.
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…