The Perils of Stateful APIs

Managing stateful resources—database transactions, memory allocations, or lock acquisitions—is notoriously error-prone. Traditional approaches rely on runtime checks or programmer discipline, leading to bugs that surface only in production. What if the type system could enforce correct usage patterns? Haskell developers have long leveraged phantom types for state transitions, but tracking nested states like transaction depth requires more precision. Enter type-level natural numbers.

Phantom Types Meet Arithmetic

The core technique attaches a phantom type parameter n to a resource handle (e.g., DbHandle n), representing the current transaction depth:

data DbHandle (n :: Nat)

openDB :: IO (DbHandle 0)
closeDB :: DbHandle 0 -> IO ()
beginTransaction :: DbHandle n -> IO (DbHandle (n + 1))
commitTransaction :: DbHandle (n + 1) -> IO (DbHandle n)

This API ensures:
1. Databases close only at depth 0
2. Transactions commit only when nested (n + 1)

Attempting invalid operations triggers compile-time errors:

-- Fails: Closing mid-transaction
closeDB =<< commitTransaction =<< beginTransaction handle

GHC rejects this with:

Expected 'DbHandle 0', got 'DbHandle (0 - 1)'

When the Type System Fights Back

GHC's type-level naturals have limitations. Unlike true inductive types, they permit nonsensical operations:

commitTransaction handle  -- Compiles! But handle is at depth 0!

Why? GHC doesn't enforce positivity, allowing negative results (0 - 1). The fix? Explicit constraints:

commitTransaction :: (n >= 1) => DbHandle n -> IO (DbHandle (n - 1))

Now invalid commits fail, but we face redundant constraint warnings in valid code. For example:

-- Correct usage, but warns: 'n >= 1' is redundant
commitTransaction (beginTransaction handle)

These warnings are a trade-off for safety—one many consider worthwhile.

Ergonomic Wrappers and Rank-N Types

Most resource usage follows an "initialize, use, cleanup" pattern. We can abstract this with a rank-N type wrapper:

withDB :: (forall n. DbHandle n -> IO a) -> IO a
withDB action = bracket openDB closeDB action

The forall n ensures the action works at any depth, preventing unsafe operations like premature commits. But GHC's type checker stumbles on arithmetic proofs:

-- Initially fails: Can't prove (n + 1) - 1 = n
withDB $ \h -> commitTransaction (beginTransaction h)

Solution? Sprinkle constraints:

withDB :: (forall n. (n - 1) ~ (n - 1) => DbHandle n -> IO a) -> IO a

Now nested transactions work seamlessly, while invalid operations remain blocked.

Beyond Transactions: A Blueprint for Safety

This pattern extends beyond databases:
- Memory allocation: Track allocated/freed states
- Lock hierarchies: Enforce acquisition order
- Session management: Validate state transitions

For complex scenarios like rollbacks, the author proposes embedding operations in a sum type:

data DBOp n where
  Rollback :: DBOp n -> DBOp n
  Query    :: String -> DBOp n

This allows controlled deviations from the standard flow while maintaining type safety.

The Cost of Correctness

Type-level naturals offer unparalleled safety for resource management, but they come with boilerplate. Redundant constraints and arithmetic quirks require vigilance. Yet, for critical systems, shifting error detection from runtime to compile time is transformative. As Haskell's type system evolves—perhaps with dependent types—these techniques will only become more powerful. For now, they represent a compelling frontier in API design, turning what were once runtime disasters into compiler errors.

Source: Type-Level Naturals and Constraints in Haskell by Fraser Tweedale