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:
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:
And now, if we try and do some wild type stupidity, our code doesn’t even compile:
What about this potentially malformed user input?
…gets a string type, which means we don’t have to check that
…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 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
predicate is a type that lets us better describe the
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.
The most basic predicate is
id, which doesn’t really do anything.
It’s named after the
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 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!
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.)
9 is clearly taking the piss and totally won’t
100 is cool with me, and will happily
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
Boolean values with
Refined (SizeGreaterThan D0) (List Boolean).
Therefore this list does not
…but this one is fine.
These type signatures are starting to get pretty hefty, but we can do better than that - we’ve also got
Or for combining them.
Let’s only allow whole numbers from
Or indeed, allow all whole numbers EXCEPT
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
…if we want to use it as an API request, sounds like a lot of work right? Maybe not! Because
refined instances have
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.
Yep. For more details, check out the Refined Haskell library or indeed the purescript-refined library which I ported from the Haskell one.