Have you ever looked for a numeric type with a zero to hundred range to describe percentage? Maybe a zero to one to describe a proper fraction of something? A positive integer (without the zero) to enumerate something? A vector of a specific length? Here that comes and not only with the Haskell refinement types library (on GitHub, on Hackage)!
Contents
Why do we need all that?
The problem
I’ll start with an example. Let’s write ourselves a neat utility, which will slice a list into chunks of a given length:
Quite trivial, right? Not so fast. Let’s consider, what this function will do when it receives a negative Int
. Turns out, it really doesn’t make much sense for it. What about a zero? It will generate an infinite list of empty lists  not a very useful result either.
So, what we need is a positive integer. Sadly Haskell does not define any such type. This means that we’ll have to use Int
, but we cannot define our function for all of its possible values. In other words, our function is partial.
So, what are the possible approaches here? I know three popular ones:
 Fail with `error` if `n` is invalid:
 Check the `n` parameter and replace invalid values with a default one:
 Wrap the result in `Maybe` depending on whether `n` is valid: But actually the following uncommon construct would make more sense as per my taste:
Turns out, each of the above solutions has its problems.
Failing with error
, as in the first case, is a commonly frowned upon antipattern. It’s not very consistent to add meaning to senseless values as we do in the second case either. Wrapping results in a Maybe
in such a trivial function might make someone itchy to fall back to either of the preceding solutions. However, of all the above solutions the seasoned Haskellers would choose the ones using Maybe
, because they are safe and they make sense.
On top of all the mentioned problems you can notice the one that all three cases share: they extend the primary problem of slicing the list with a problem of input validation. But isn’t the isolation of concerns the cornerstone of our good practices? It’s not even hard to notice how much more code the three solutions require compared to the original one.
There must be a better way to approach this! And indeed there has been one for quite some time.
Smart constructors
So, as we’ve established, we need to isolate the problems of validation and list slicing. Here we go:
The trick here is for the API not to export the constructor of PositiveInt
, but only the positiveInt
checked construction function and the positiveIntValue
extractor.
So despite there being more code now, we have an isolation of concerns. The slice
function is now only concerned with what it should do, it is safe and it is no longer partial! The PositiveInt
stuff can be extracted into another library and reused for other purposes. That is separation of concerns in action and that is what functional programming is all about.
But, as you might expect, we’re not quite finished yet. There are problems with PositiveInt
too.
Problems of smart constructors

Having only the checked construction at our disposal means that we’ll be wasting resources on the redundant runtime validation when we specify hardcoded input values. Theoretically, this must be possible to do at compiletime.

Even the way it’s referred to, Smart Constructor is a pattern. What is the right thing to do when you spot one? Right! Abstract.
While solving the above two problems I came up with a library, which, as it accidentally turned out, essentially defined Refinement Types. Please, meet
The “refined” library
Not gonna waste your time here’s how you’d solve the above problem using it:
So what is Refined
and what is Positive
here? Refined
is a type which “refines” some other type with a certain typelevel predicate. Positive
is one such predicate. User is free to use the predefined set of predicates coming with the library, or define his own.
Predicates are composable with the predefined logical predicates. E.g., here’s how you can define a Double
refined to a range from zero to one:
Yes, the library uses typeliterals to make working with numbers neater, so you’ll need GHC 7.8 and higher.
You might have noticed, how we extract the wrapped value using the unrefine
function, but how to construct the Refined
values?
Constructing values
The library comes with two functions for construction of Refined
values: refine
and refineTH
. Both use a Predicate
typeclass instance to validate the value. The first one validates the value at runtime, producing either a failure message or a valid Refined
value  nothing special, same thing as in the Smart Constructor pattern. The neat thing is how refineTH
validates the value at compiletime using Template Haskell. As an example here’s how you’d use it with our previously defined function:
Compiletime checking and no overhead!
What is a predicate?
A predicate is a type, which requires no valuelevel implementation. Instead, to be used with the functions of the library it requires instance(s) of the Predicate
typeclass.
E.g., here’s a predicate, which ensures that a String
is lowercase:
As you might have guessed, the validate
function detects an error in the value. The first parameter is the unpopulated value of the predicate type  you can simply ignore it.
You can use our newly defined predicate like this:
Performance concerns
The unrefine
function bears zero overhead, since it mearly unwraps newtype
. The refineTH
function bears zero runtime overhead as well, since it simply packs a value into newtype
.
Happy refining!