To make invalid states unrepresentable is a core design goal of the software at Bellroy. With that in mind, a type we often employ for textual data – of which we have a lot – is NonEmptyText. It is just what it sounds like: a value of this type is a string with at least one character.

Which, with the right LANGUAGE incantations, does actually work. This requires UndecidableInstances to work, which is not harmful in and of itself, but does open up the possibilities of what can go wrong.

Additionally, since IsNonEmptySymbol is a type family, it can’t directly be used like an ordinary typeclass constraint – for instance, it can’t be packaged into a Dict, or used with functions like Data.SOP.hcfoldMap; it’s not something you can just “ask for an instance of” like an ordinary typeclass, despite returning a Constraint like one.

The final step then to this trick is writing IsNonEmptySymbol as a typeclass:

When GHC resolves the IsNonEmptySymbol constraint given an empty string, it finds both: _ => instance IsNonEmptySymbol "" and instance IsNonEmptySymbol a. If we omitted the OVERLAPPING pragma, that would be where GHC raises an error; it wouldn’t know which instance to actually choose, and would complain that there are overlapping possibilities – which is fine, since the only case where there is an overlapping instance is in the case we want to forbid, when the input is "".

So the effect of the OVERLAPPING pragma here is that GHC is does choose the instance we “want”; the one with the custom type error. The instance then raises our custom error message informing the user that a non-empty string was expected.

Our internal bellroy-data package – containing data such as information about known freight and shipping providers, accounting systems, product data, tax codes, etc. – had thousands of TH splices like $$(NonEmptyText.makeTH _). Moving to the RequiredTypeArgument approach shaved off around 10% of the compilation time for that package.

We can re-use (almost) the exact same code to validate that a given Natural is positive to make a type-checked Positive constructor. In general we can use this technique for any type we can define a type-level predicate for.

From here you might be able to imagine, for instance, type-level string parsing to define for instance type-safe term syntax for constructing URIs: it will work, but you’ll run into GHC’s default reduction limit of 20 quite quickly; an O(n) type-level validator over a n-length string has a hard-cap of 20 “reduction” (i.e., parsing) steps and thus parsing cannot proceed beyond 20 characters – that is, also assuming your parsing steps themselves aren’t counting towards that limit.

In general non-trivial algorithms are also quite awkward to express in type families; you have no way to write let-bindings for instance, or do pattern matching with a case-like syntax: if you need either, they must be expressed with some combination of extra type arguments and helper type families. This also needs a bit of plumbing to work as a typeclass as in the above IsNonEmptySymbol class we created.

Nevertheless, if you’ve gotten this far, you’re probably interested in what that can look like: behold 🪄, type-level parsing for DynamoDB table-names:

So far, so good. But enumerating every single invalid string will take some time; we need an algorithmic approach rather than how IsNonEmptySymbol worked above. As above, we’d prefer to encapsulate this into a typeclass of kind Type -> Constraint. The approach I use here is to use a type-family to direct the resolution of an inner typeclass. So this approach works as a unary typeclass (desirable) and surfaces custom type error messages to the programmer (excellent).

Now we actually need to implement this IsValidTableName__ type family which looks like IsValidTableName__ (input :: Symbol) :: Bool.

Finally, we can actually use this:

The singletons-th package could be used here to promote actual term-level functions like the IsValidTableName function, but a point here is to demonstrate how that would actually work under the hood.