Refinement Types

2025-12-18 · by Rob Durst

I'm building Caffeine, a compiler written in Gleam that compiles service expectations to reliability artifacts. This post documents the motivation and design of refinement type support in Caffeine.

Motivation

The Basics

One of the core functions of Caffeine is to resolve "cascading" input ➡️ param configurations. Within the docs we define the three different personas for each level of the configuration hierarchy:

1. artifacts -> caffeine core developer

2. blueprints -> observability expert

3. expectations -> service owner

Thus, since it may not be the same person defining each specification here, we, from the initial 0.2.2 release, enabled developers to bind a type to each param. As an example, consider artifact:

{
  "artifacts": [
    {
      "name": "SLO",
      "version": "0.0.1",
      "base_params": {
        "threshold": "Float",
        "window_in_days": "Integer"
      },
      "params": {
        "queries": "Dict(String, String)",
        "value": "String",
        "vendor": "String"
      }
    }
  ]
}

With this, we place a constraint on the input values (even if not super restrictive). Here we had two basic "categories" of types:

primitive types:

Boolean
Integer
Float
String

collection types:

List(T): T must be a primitive
Dict(T, V): T and V must both be primitives

As noted, there are a few restrictions on the collection types themselves. These may be lifted in the future, but the goal here was to simplify the initial design and also not enable arbitrarily nested collections, i.e.:

List(List(Dict(Integer, List(String))))

For an initial rollout, this was nice as it (a) got initial users comfortable with types and (b) forced us to lay the groundwork within the Caffeine compiler to support type checking.

Modifier Types

The more we wrote artifacts, blueprints, and expectations, the more we began to desire some additional param behavior.

Optional Types

It turns out some queries required certain inputs only in some circumstances. One specific example is an http success rate query which might optionally include a "status code exclusion" List(Integer) param.

I.E. consider the following.

sum.http_requests{$$status_codes:exclusion_status_codes:not$$}

For one endpoint we may want to ignore 400 and 401 but for another endpoint all status codes might be valid. With the Optional type, which has a form of:

Optional(T): T can be a primitive or a collection

So for this specific situation we'd specify:

"exclusion_status_codes": "Optional(List(Integer))"

Thus when we resolve the query, if the attribute is excluded in the input specifying configuration, we'd ignore it.

Defaulted Types

While Optional enabled more use cases and extended flexibility, Defaulted seeks to improve developer experience by reducing duplication and boilerplate.

As an example, most queries we'd written thus far relied on an environment param:

"params": {
  "environment": "String"
}

Unsurprisingly, most expectations would then specify: environment: production. In fact, >95% of all SLOs I've written with Caffeine at work fall within this category. So, we introduced Defaulted to handle this redundancy issue. Now, instead of the above, we could specify a default value for the environment param as so:

"params": {
  "environment": "Defaulted(String, production)"
}

With this, where we'd previously had to specify environment: production, we could just drop that input. Some might righteously argue that implicit params might lead to confusion and unintentional errors. However, we believe this is a tradeoff we should at least leave up to the developers and not take a strong stance ourselves (and thus to hold ourselves, the core team, to this standard, there will be no Defaulted types in the standard library... as appealing as that may seem for window_in_days).

As of the 0.2.11 release both of these types are available!

Refinement Types

Ok, so with primitive and collection types we get the basics most folks would expect, and with modifier types we get a few handy types to enable more use cases and enable reduction of repeated common input specification. But what if we want to further guide consumers of our artifacts and blueprints? What if we want to not just constrain the general shape of a value (e.g., "it's an integer") but further restrict which specific values are valid? For this, we need refinement types!

Formally, a refinement type has the form { x : T | P(x) } where T is the base type and P is a predicate that must hold for all values of the refined type. In Caffeine, refinements are compile-time constraints checked when validating expectations (configuration), not a runtime type system. We're starting with decidable, finite refinements (e.g., membership in an explicit set) rather than a general SMT-backed refinement logic.

As an example, let's say we have a String type, such as environment, in which we know the possible values are just a subset. With refinement types we could say:

"environment": "String { x | x in { production, staging, development } }"

Or imagine we have an integer, say window_in_days, which we want to limit to a known set of values:

"window_in_days": "Integer { x | x in { 7, 30, 90 } }"

Looking ahead, we could imagine extending refinements to support other predicates like numeric ranges or collection constraints:

"threshold": "Integer { x | x > 0 and x < 100 }"
"pair": "List(String) { x | length(x) = 2 }"

These are aspirational examples; for now, we're focused on OneOf (set membership) as described below.

This allows the compiler to provide stronger guidance when writing expectations.

Design

The Four L's of Caffeine's Refinement Type Design

From the get-go we started by (a) keeping the type inputs as they are, appending the refinement to the end and (b) surrounding the refinement with curly braces.

EXISTING_TYPE { REFINEMENT }

From here we defined the principles for REFINEMENT, ending up with the "four L's":

1. (L)egible

2. (L)ight Notation

3. (L)ow Effort

4. (L)imited

Legible

We should be able to reason about the predicate by reading it from left to right.

Light Notation

Avoid notation that is "too mathy": prefer in over ∈. The | is fine to divide the bound variable from the predicate. Even if folks don't know that the | means "such that" it should at least be understood at face value as the thing on the left where it is restricted in some way by the thing on the right. (For future refinements that support boolean connectives, we'll prefer and over &&, etc.)

Low Effort

While overly concise syntax might actually diminish legibility, prefer fewer characters to more. We want adding refinements to feel simple and easy, not cumbersome. They should require very little brainpower: even the tired dev after a strenuous day at work should be able to quickly write a REFINEMENT.

Limited

We will start small and expand. In fact, we will do this over two dimensions:

1. type support: start with just primitives where it makes sense

2. refinement support: pick a simple one like OneOf and implement in full (parser, type-checker, error messages, docs) to get the design right. Test with a few folks. Then go from there. Don't overcommit before getting feedback and a full end-to-end implementation.

Starting with OneOf

Here is a full design spec for our first refinement predicate: OneOf (set membership).

Supported Types

To begin, we will just support a subset of primitives: Integer, Float, and String (technically we could support all but Boolean would be weird...).

Full Example

Integer { x | x in { 7, 30, 90 } }

Here the syntax is hopefully fairly straightforward. As we mentioned above, the REFINEMENT is appended to the right of the type, inside curly braces. In this refinement specifically, we have our type variable x to the left of the "such that" divisor line (|). Then we have a predicate that states x must be within some set.

This set has two restrictions:

1. each element must be the type left of the REFINEMENT

2. the set must be non-empty

Furthermore, values within the set are comma delimited.

Composing with Optional and Defaulted

Refinements compose with Optional and Defaulted as follows:

  • Optional(String { x | x in { ... } }): the key may be omitted; if present, the value must satisfy the refinement.

  • Defaulted(String { x | x in { ... } }, "production"): the default value must satisfy the refinement.

  • Refinements apply to the underlying value when present.

Conclusion

The Caffeine refinement types journey is in the early stages of development. We expect OneOf to be released as part of 1.1.0. Stay tuned!

And Happy Holidays!!! 🎄🕎❄️

Tired guy with Christmas lights

Long night of coding followed by festivities... definitely not me right now.