Announcing the refinement types library

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?

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:

slice :: Int -> [a] -> [[a]]
slice n l =
  splitAt n l & \(a, b) -> a : slice n b

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:

1. Fail with `error` if `n` is invalid:

   slice :: Int -> [a] -> [[a]]
   slice n =
     if n >= 1
       then
         let slice' l = splitAt n l & \(a, b) -> a : slice' b
             in slice'
       else error $ "Invalid `n`: " <> show n

2. Check the `n` parameter and replace invalid values with a default one:

   slice :: Int -> [a] -> [[a]]
   slice n =
     slice'
     where
       n' = if n >= 1 then n else 1
       slice' l = splitAt n' l & \(a, b) -> a : slice' b

3. Wrap the result in `Maybe` depending on whether `n` is valid:

   slice :: Int -> [a] -> Maybe [[a]]
   slice n l =
     if n >= 1
       then 
         let slice' l = splitAt n l & \(a, b) -> a : slice' b
             in Just $ slice' l
       else Nothing

   But actually the following uncommon construct would make more sense as per my taste:

   slice :: Int -> Maybe ([a] -> [[a]])
   slice n =
     if n >= 1
       then
         let slice' l = splitAt n l & \(a, b) -> a : slice' b
             in Just $ slice'
       else Nothing

Turns out, each of the above solutions has its problems. Failing with 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.

Smart constructors

So, as we’ve established, we need to isolate the problems of validation and list slicing. Here we go:

newtype PositiveInt =
  PositiveInt { positiveIntValue :: Int }

positiveInt :: Int -> Maybe PositiveInt
positiveInt n =
  if n > 0 
    then Just $ PositiveInt n
    else Nothing

slice :: PositiveInt -> [a] -> [[a]]
slice n l =
  splitAt (positiveIntValue n) l & \(a, b) -> a : slice n b

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

1. 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.

2. 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:

import Refined

slice :: Refined Positive Int -> [a] -> [[a]]
slice n l =
  splitAt (unrefine n) l & \(a, b) -> a : slice n b

So what is Refined and what is Positive here? 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:

type ProperFraction =
  Refined (And (Not (LessThan 0)) (Not (GreaterThan 1))) Double

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 Refined values?

Constructing values

The library comes with two functions for construction of Refined values: refine and 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:

sliceToTriplets :: [a] -> [[a]]
sliceToTriplets = slice $$(refineTH 3)

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 Predicate type-class.

E.g., here’s a predicate, which ensures that a String is lower-case:

import Data.Char

data LowerCase

instance Predicate LowerCase String where
  validate _ value = 
    if all isLower value
      then Nothing
      else Just "Not all chars are 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:

type LowerCaseString =
  Refined LowerCase String

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!