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.

• string vs number
• 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:

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:

• name should 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:

1. a string value
2. 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:

1. validate dynamically once,
2. convert into a stronger type,
3. 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:

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.

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

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