Type-checked non-empty strings

By Mike Ledger | 2026-06-23 | Technology

This post is a Haskell koan.

While I will eventually dive into the motivation and background, the primary aim here is to demonstrate a niche but highly effective technique we've implemented and loved. It is, in essence, perfect material for a technical blog.

The Core Objective

We developed a constructor for non-empty strings that is verified at the type level. By replacing thousands of TemplateHaskell (TH) calls with this method, we achieved a ~10% reduction in build times for a massive, data-centric package.

Comparison: The Evolution of Validation

At Bellroy, a fundamental architectural pillar is ensuring that invalid states are unrepresentable. To support this, we frequently use the NonEmptyText type, which guarantees a string contains at least one character.

---

The Technical Implementation

This approach is the culmination of various GHC features evolving over the last 15 years. Specifically, RequiredTypeArguments (introduced in GHC 9.10) allows us to treat type-level string literals as if they were values passed to a function.

Step 1: The Type Family Approach

We can trigger a custom compile-time error using Unsatisfiable if the type-level string is empty:

type family IsNonEmptySymbol symbol :: Constraint where 
  IsNonEmptySymbol "" = Unsatisfiable ( Text "Expected a non-empty string" ) 
  IsNonEmptySymbol _  = ( ():: Constraint ) -- Success: empty constraint

Using this, the make function looks like this:

-- Note: RequiredTypeArguments allows the syntax below
make :: forall symbol - ( IsNonEmptySymbol symbol) = NonEmptyText 
make symbol = NonEmptyText (fromString (symbolVal ( Proxy :: Proxy symbol)))

test :: NonEmptyText 
test = make hello!

Step 2: Overcoming Limitations

While the above works (requiring UndecidableInstances), it has drawbacks:

1. It is a type family, meaning it cannot be wrapped in a Dict.
2. It cannot be used with functions like Data.SOP.hcfoldMap.
3. You cannot "request an instance" of it like a standard typeclass.

Step 3: The Typeclass Pivot

To fix this, we redefine the check as a typeclass using OVERLAPPING instances:

class IsNonEmptySymbol symbol 

-- The specific case for empty strings
instance {-# OVERLAPPING #-} 
  IsNonEmptySymbol "" = Unsatisfiable ( Text "Expected a non-empty string" )

-- The general case for any other string
instance IsNonEmptySymbol a 

How it works: When GHC encounters an empty string, it sees two possible instances: the specific "" instance and the general a instance. Without OVERLAPPING, GHC would simply complain about ambiguity. With it, GHC chooses the most specific one—the one that triggers our custom error message.

---

Real-World Impact

Our internal bellroy-data package—which manages complex datasets like shipping providers, tax codes, and accounting systems—contained thousands of splices resembling $$(NonEmptyText.makeTH _).

The Result:

• Migrated to RequiredTypeArguments.
• Removed TH overhead.
• Reduced compilation time by ~10%.

---

Expanding the Pattern

This logic isn't limited to strings. We can apply this to any type with a type-level predicate.

• Positive Numbers: Create a type-checked Positive constructor for Natural numbers.
• Complex Validation: Type-safe URI construction or syntax validation.

The Constraints of Type-Level Logic

However, there are significant hurdles when moving toward complex algorithms:

1. Reduction Limit: GHC has a default reduction limit of 20. A validator with $O(n)$ complexity over a string of length $n$ will hit a hard cap at 20 characters.
2. Syntax Limitations: Type families lack let bindings and case expressions. Any complex logic must be simulated via helper families and additional type arguments.

Example: DynamoDB Table Name Validation

Despite the friction, it is possible. Here is a glimpse at validating DynamoDB table names (which must match /^[a-zA-Z_.-]{3,255}$/):

{-# LANGUAGE DataKinds, QuantifiedConstraints, RequiredTypeArguments, TypeFamilies, UndecidableInstances #-}

import Data.Proxy
import Data.String (fromString)
import Data.Text ( Text )
import Data.Type.Bool qualified as Bool
import GHC.TypeError
import GHC.TypeLits

newtype TableName = TableName Text deriving ( Show )

make :: forall name - ( IsValidTableName name) = TableName 
make name = TableName (fromString (symbolVal ( Proxy :: Proxy name)))