Refine, fine, fine

Posted on July 5, 2019

About a month ago I gave a talk about Refined types at a React meetup. Needless to say, it was a resounding success so I thought I would share an adapted version of the slides so that you can all learn to be as learned as me when it comes to such a topic.

Let’s start by listing some things that we as programmers generally agree we don’t particularly like:

Runtime errors caused by Javascript YOLO

Here is some classic code written in the Javascript programming language:

At a casual glance, it would appear to be some rather convoluted code for making a string uppercase.

Therefore, this seems fine:

But this isn’t so great:

What happened? Well it wasn’t really a function for making strings uppercase, it was a function that takes any piece of data, then makes it uppercase if it’s a string, and just breaks weirdly with anything else.

Another thing we don’t really like doing as programmers is…

Overly defensive code around user input

So if your start in programming involved more than a sprinkling of PHP, then you’ll be used to starting all your functions with the manual typechecking dance.

Defense against the dark arts

Another favourite is manually checking our values to check basic mathematical operators aren’t going to explode the whole computer.

How far does something like Typescript get us?

So we can change our weird uppercasing function…

…to only take a string like we intended.

Let’s give it a smash:

Excellent stuff.

And now, if we try and do some wild type stupidity, our code doesn’t even compile:

+1

What about this potentially malformed user input?

This Wild West Cowboy Javascript…

…gets a string type, which means we don’t have to check that name exists…

…but we still need to check whether name is long enough and return a default if not.

What about that classic divide by zero problem?

What can basic types give us here?

We can get rid of the number checks…

…but we’ve still got to check for that zero value. Better, but not great. What if I told you we could do better than this?

Refined

Enter Refined types. A Refined type looks like this:

As it is a newtype it is a wrapper around a value that is used for type purposes at compile time but then erased at run time (so when the program runs, Refined 100 is just 100 as far as memory etc is concerned)

value is the type of actual data we are refining, for example Int or Number.

predicate is a type that lets us better describe the value.

The most interesting thing to note here is that predicate only exists on the type side (ie before the =) and not after - this makes it a phantom type which is only used to add contextual information. Let’s see what that actually means…

Making Refined values

There are a few ways to make Refined values, especially in the Haskell library - we’ll concentrate on two. I’m going to use the types from the Purescript version because a) they’re simpler and b) I made them and am thus less likely to get it wrong.

This is the regular way to make Refined value - you pass it a plain value and it returns either Left with a RefinedError describing the problem, or Right with the Refined value inside.

This ignores the predicate and leaves it to the programmer to go full YOLO and decide whether the predicate will be fine. I have used this to make Monoid classes where I want to add two positive numbers without checking that the outcome will still be positive.

Id

The most basic predicate is id, which doesn’t really do anything.

It’s named after the id (or identity) function - the function that returns whatever it receives, basically doing nothing.

For example, any value that is a value Int can be made into a valid Refined Id Int.

Positive

The Positive predicate, which only allows numbers over 0.

This refinement would pass the predicate:

This clearly very negative number clearly won’t fly. Nice try, ding dongs!

From

We can be even more specific with these types too. The From predicate takes an integer and only allows values equal to or above it.

(A note here - that D10 is a type-level 10. It is provided by the purescript-typelevel package.)

Therefore this 9 is clearly taking the piss and totally won’t refine.

However this 100 is cool with me, and will happily refine.

To

Hopefully it should be fairly intuitive how the To predicate works…

SizeEqualTo, SizeGreaterThan, SizeLessThan

Refinements don’t have to just be about numbers - we can use them on foldable structures too, such as Lists. The refinements let us be specific about sizes of said structure. Therefore we could make a non-empty List of Boolean values with Refined (SizeGreaterThan D0) (List Boolean).

Therefore this list does not refine

…but this one is fine.

And, Or

These type signatures are starting to get pretty hefty, but we can do better than that - we’ve also got And and Or for combining them.

Let’s only allow whole numbers from 1 to 100

Or indeed, allow all whole numbers EXCEPT 1 to 100.

This type describes the roll of a dice.

Or this one, which describes the first bunch of prime numbers, and is all a bit silly to be honest.

Back to our stupid contrived problems…

Now with the power of Refined types, our defensive printName function is pretty much unnecessary…

Plus we can make a type to make division safe from fear, at last..

Automatic JSON validation

So let’s say we have this data type using Refined

…if we want to use it as an API request, sounds like a lot of work right? Maybe not! Because refined instances have fromJSON and toJSON instances for Aeson (or for Argonaut in Purescript) then we can automatically decode them from JSON and make the decoding fail if the predicate does not pass.

This way, anywhere in our app, name will always be non-empty. and age will always be 18 or more.

Well, shit.

Yep. For more details, check out the Refined Haskell library or indeed the purescript-refined library which I ported from the Haskell one.