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)!
Why do we need all that?
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.
error, as in the first case, is a commonly frowned upon anti-pattern. 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.
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
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
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 hard-coded input values. Theoretically, this must be possible to do at compile-time.
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
Refined is a type which “refines” some other type with a certain type-level 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 type-literals 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
The library comes with two functions for construction of
refineTH. Both use a
Predicate type-class 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 compile-time using Template Haskell. As an example here’s how you’d use it with our previously defined function:
Compile-time checking and no overhead!
What is a predicate?
A predicate is a type, which requires no value-level implementation. Instead, to be used with the functions of the library it requires instance(s) of the
E.g., here’s a predicate, which ensures that a
String is lower-case:
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:
unrefine function bears zero overhead, since it mearly unwraps
refineTH function bears zero runtime overhead as well, since it simply packs a value into