Ensuring correctness through the type system

Written by John Mikael Lindbakk - 02/03/2026 12:00

Typing is something many developers take for granted, and many see it as a nuisance rather than a valuable skill.

I have opinions.

The problem

Let's take this classic example in Java:

public void sendEmail(String emailAddress) {
    // Code...
}

Given this code, what does emailAddress actually contain? Is it an actual address, or does it contain the entire play of Hamlet?

Maybe more importantly, a valid email address doesn't have to be about the structure of the string. We may have to check whether the address belongs to a user in our system, whether we've sent an email before and possibly cover our bases legally. There's more to this than the simple question of "Is this a valid email?"

The simple answer is "We don't know". The solution is to verify the address. My challenge here is, why even allow this to be a potential scenario? Why don't we utilise the type system to ensure correctness?

Yaron Minsky of OCaml fame has said the following:

Make Illegal States Unrepre­sentable

I agree. The Java code allows for an illegal email address to be represented, but it should never be allowed in the first place.

Some might then simply add some validations at the border of the application and call it a day. Something like this:

public class EmailSenderController {

    private EmailSender emailSender;

    public EmailSenderController(EmailSender emailSender) {
        this.emailSender = emailSender;
    }

    public void sendEmail(String emailAddress) {
        throwIfAddressIllegal(emailAddress);
        emailSender.sendEmail(emailAddress);
    }

    private void throwIfAddressIllegal(String emailAddress) {
        // Code...
    }
}

The above works, but its shoddy design solves the issue locally without considering codebase growth and maintenance. Now we end up in a situation where every part of the application that may want to send an email also needs to validate its email, but that requirement is implicit - nothing is forcing that validation. We just have to remember to do it, and if we don't, then things can go very wrong.

Even if we extract the throwIfAddressIllegal method into a more reusable form, like an "EmailValidationService", it won't do much good because different parts of the application still have to remember to call it. Correctness is not enforced.

Other developers may suggest that we do the opposite and move the validation into sendEmail. This also makes sense on many levels:

public void sendEmail(String emailAddress){
    throwIfAddressIllegal(emailAddress);
    // Code...
}

Now the calling code will have the emailAddress validated, whether they like it or not!

This is, for the most part, fine, except that we're pulling dependencies inwards. Let's consider various requirements that might be needed:

There's a lot that might be needed, and by forcing sendEmail to handle the validation, we are also pulling all the needed dependencies into that class.

Our two approaches so far have both had serious downsides:

  1. Pushing the burden of correctness outward causes problems for reusability.

  2. Pulling the burden of correctness inwards creates dependency bloat.

The solution: Types to the rescue

It seems that the ideal solution would be to push the burden of correctness outward, while still enforcing the correctness checks. How can we do that? Well, with types of course!

Let's take the example above, but with a little twist:

public void sendEmail(Email emailAddress){
    // Code...
}

Notice how we're using an Email type over a String? This means we've limited the use of our method and are forcing the calling code to create the Email type.

Let's take a look at what one such email type could look like:

public class Email {
    private String email;
    public Email(String email) {
        throwIfAddressIllegal(email);
        this.email = email;
    }

    private void throwIfAddressIllegal(String email) {
      // Code...
    }
}

Note

For simplicity, I'm using the "throw as return" pattern here, which is an anti-pattern. The error-as-value discussion is out-of-scope for this post. I just wanted to highlight that I'm aware that the design here is lacking and that we're making a shortcut.

In simple terms, we require correctness through our API design.

This is the actual power of a robust typing system: the ability to drive correctness through the usage of types!

Taking it further

We don't have to limit ourselves to one type; we can chain types:

public class Email {
    // ...
    public Email(String email) {
        // Checks if valid email
    }
}

public class UserEmail {
    // ...
    public UserEmail(Email email) {
        // Checks if email belongs to registered user
    }
}


public class VerifiedUserEmail {
    // ...
    public VerifiedUserEmail(UserEmail email) {
        // Checks if the email is verified
    }
}

//Etc...

I'm not suggesting that we should embrace over-encapsulation. Not at all. I suggest we drive correctness through the APIs. Pushing the complex bits outwards.

In the example above, we've gone so far as to have VerifiedUserEmail, which normally would be a boolean property called "isVerified". Some would see the above as "too granular", and in some situations, they might be correct.

Let's say the "verification" check needs to hit a completely different service, which means another I/O call across the wire. Then maybe putting parts of that complexity into its own type might not be the worst idea.

The point here is that this is context-dependent, but I would urge developers to push correctness through types. It is a much more robust approach than relying on the calling code to do its due diligence or bloating the callee with dependencies.

But what about non-OOP languages?

In the above example, we looked at Java, a classic OOP language. It is easy to confuse the "correctness-through-types" idea with OOP, but it has nothing to do with it.

Let's take Gleam as an example: a functional, typed language. In Gleam, we have what is called opaque types, or in simple terms: Types with private constructors. We can use these types to do the same as we did with Java:

pub opaque type Email {
    Email(value: String)
}

pub opaque type UserEmail {
    UserEmail(value: Strig)
}


pub opaque type VerifiedUserEmail {
    VerifiedUserEmail(value: String)
}


pub fn new_email(email: String) -> Result(Email, Nil) {
    // Check if valid email and return Email type if valid
}

pub fn new_user_email(email: Email) -> Result(UserEmail, Nil) {
    // Check if user registered
}


pub fn new_verified_user_email(email: UserEmail) -> Result(VerifiedUserEmail, Nil) {
    // Check if the email address is verified
}


pub fn send_email(email: VerifiedUserEmail) {
    // Sends email
}

In the code example above, the only way to create an Email type is to go through the new_email function. We also see that to call new_user_email, we already need to use the Email type, and we need to call new_user_email to get an instance of UserMail, which we can pass to new_verified_user_email.

This more or less creates a function chain that other parts of the system have to use if they want to send an email:

pub fn main(input: String) -> Result(Nil, String) {
 input
 |> new_email
 |> result.try(new_user_email)
 |> result.try(new_verified_user_email)
 |> result.map(send_email)
}

As such, even without OOP, we can drive correctness using types.

What about dynamically typed languages?

At this point, one might imagine that this is why people like strongly typed languages... and yes, that is the case, but that doesn't mean you're fresh out of luck if you happen to work with a language that is not strongly typed.

Languages such as Python have type hints, and Ruby has sorbet. These are type checkers that live outside the language itself, or are at least optional. They're an addition one may use, but with them one can achieve similar protections as in strongly typed languages during development.

Let's use Clojure.spec as an example:

;; A raw email is just a string
(s/def ::email string?)

;; A verified flag
(s/def ::verified boolean?)

;; A registered user email
(s/def ::user-email
  (s/keys :req [::email]))

;; A verified user email
(s/def ::verified-user-email
  (s/keys :req [::email ::verified]))

Now that we have our "types" in place, we can start creating our functions:

(s/fdef valid-email?
  :args (s/cat :email string?)
  :ret boolean?)
(defn valid-email? [email]
  ;; check email format
)


(s/fdef registered-user-email
  :args (s/cat :email string?)
  :ret (s/nilable ::user-email))
(defn registered-user-email [email]
  ;; return {:email email} if user exists
)


(s/fdef verified-user-email
  :args (s/cat :user-email ::user-email)
  :ret (s/nilable ::verified-user-email))
(defn verified-user-email [user-email]
  ;; return {:email ..., :verified true} if verified
)


(s/fdef send-email
  :args (s/cat :email ::verified-user-email)
  :ret nil?)
(defn send-email [email]
  ;; actually send the email
)

Now we can write tests for our functions and verify that their inputs and outputs adhere to the expected types.

The point here is that driving correctness through types isn't really about statically typed languages or OOP, but about the ability to enforce contracts at boundaries.

Note

There is a discussion to be had about whether contracts or type is even required. After all, shouldn't testing themselves be enough? This question will quickly lead to whether developers today can be trusted, and the fact that I find their ability to write good enough tests to be lacking.

The overall conclusion I have come is that yes, testing will do the job. In theory. In practice the industry have a long way to go when it comes to discipline. While I can trust individuals to do the right thing I find myself struggling giving the same trust to entire teams.

So, types are pretty cool, eh?

There are two patterns I see pretty often:

// Code that checks if function can be called...
// Calling function...

and

// Data coming into function as parameters...
// Data being validated within the function...

Both of these come with downsides. The former forces developers remember to perform certain checks before calling a method. The latter may require a whole bunch of dependencies to verify the parameters, in addition to the actual functionality the function is supposed to perform.

Drive non-trivial correctness through types, so misuse becomes impossible rather than merely discouraged.