DEV Community

Shrijith Venkatramana
Shrijith Venkatramana

Posted on

Type Inhabitation in Lean: Why “Hello {name}” Can Become a Theorem

#webdev #ai #productivity #programming

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
Enter fullscreen mode Exit fullscreen mode

Nat is inhabited because values like:

0
1
42
Enter fullscreen mode Exit fullscreen mode

exist.

Similarly:

#check True
Enter fullscreen mode Exit fullscreen mode

is inhabited because Lean has a proof of True.

But:

#check False
Enter fullscreen mode Exit fullscreen mode

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}`
}
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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⟩
Enter fullscreen mode Exit fullscreen mode

because no proof exists that:

"".length > 0
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

Let’s unpack this carefully.

The Option Type

Option α means:

Either:
- some α
- or none
Enter fullscreen mode Exit fullscreen mode

Like:

  • Rust’s Option<T>
  • Haskell’s Maybe
  • TypeScript’s T | undefined

So:

some x
Enter fullscreen mode Exit fullscreen mode

means:

successful construction

while:

none
Enter fullscreen mode Exit fullscreen mode

means:

validation failed

What Does ⟨s, h⟩ Mean?

This constructs the structure itself.

Equivalent to:

{
  value := s,
  proof := h
}
Enter fullscreen mode Exit fullscreen mode

So:

⟨s, h⟩
Enter fullscreen mode Exit fullscreen mode

creates a valid NonEmptyString.

Then:

some ⟨s, h⟩
Enter fullscreen mode Exit fullscreen mode

wraps it into Option.

6. Why This Actually Matters

Now we can write:

def greeting (name : NonEmptyString) : String :=
  s!"Hello {name.value}"
Enter fullscreen mode Exit fullscreen mode

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)
Enter fullscreen mode Exit fullscreen mode

every caller must remember the rules.

With refined types:

greeting : NonEmptyString → String
Enter fullscreen mode Exit fullscreen mode

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.

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)