type level programming with records
Just like in Elm you can define functions like this:
This function give you the value contained in the -field of a record - the type-checker will make sure that the argument-record will have exactly one such field:
But if you call this function with a record that does not contain a field named of type it will not type-check:
The type-feature behind this is called row polymorphism.
Using PureScript you can write much more interesting functions that deal with records. For example there are quite a few libraries (one being purescript-foreign-generic) that will - among other uses - convert JSON into records just based on the record-type.
a simpler example
Instead of trying to recreate this, I want to demonstrate some of the advanced techniques using the following example:
Recently I found this question on the purescript-beginners channel of the functional programming slack board:
Is it possible to write something that does this kind of transformation?
Of course it is - and I want to show you how. So grab yourself some tea, take a big breath and brace yourself!
advice for the reader
I had a hard time explaining this - so if you don't understand some parts it is clearly my fault not yours!
Please read on and come back later when a part is troubling you to much.
It might also help to grab the code at the end of the post and play with it - what happens if you remove some instance or constraint?
If all else fails: Feel free to contact me - I will do my best to explain and clarify - you'll even help future readers!
Thank you!
Rows
First you have to understand how records are represented on the type level and for this you need to know about rows of types.
Remark: Rows itself - symbolized as can be used for every kind - for example PureScript used rows of effects until recently to enumerate all side-effects a value can produce (see ) - but for this article I'm only interested in rows of types - and I take the liberty of writing just row when I mean row of types.
If you look up in the purescript documentation you'll find this:
A row of types represents an unordered collection of named types, with duplicates.
This gives you a few hints: It's an unordered collection - that means a consists of things and the order of things does not matter - and are considered the same. In addition those things are types and they have names (also called labels). The last hint is, that this collection can have more than one type per label (the duplicates). Indeed it's hinted as:
which is a great mnemonic in my opinion.
In PureScript an example for this would be
But watch out: you moved up a (type-) level - even if you see here, it's not a value on the left and a type on the right, it's a type on the left and a kind on the right (You can think about a kind as being the type of types).
That sadly means, that instead of dealing with a program, that is type-checked at compile-time and then is evaluated at run-time you enter the place where what you write has an impact on the types (and the type-checker) and so you have to prove the compiler, that what you are doing is sensible. Those proofs in PureScript often involves type classes and functional dependencies (used with type classes) and I'm afraid this example is no exception.
Records
At first glance records in PureScript are quite simple, because they directly corresponds to JavaScript objects. Under the hood are used - for example
is syntactic sugar for
There is a slight constraint though: a record may only contain a field once - so here the underlying may only have one type per label.
solving the problem
taking a step back
To give you a better idea of what I'm trying to do on the type level, I want to start by looking at a similar problem on the value level. So instead of thinking about a record of records, assume you have a list of singleton lists and your task is to flatten them:
On a basic level - not using higher-order functions - a simplified solution could look like this:
Yeah I know - this will not work in PureScript as it's partial and I could have used a more complicated pattern match to get rid of the function but please ignore that for a moment. It's not really important, that this code would not compile in PureScript - the important point is the case-split and the helper.
The function splits the problem into two parts or cases:
- an empty list
- a list
and then it computes the result by
- getting the singleton element from the head-item
- combining this value with the result to a recursive call to itself.
Back to the original question I want to apply the same idea:
- Deal with an empty record
- Deal with an record that is made up of a head-field/value pair and tail-part
- Find some way to extract the nested value from the head
- Building up a new record with that together with a recursive strategy for the tail.
PureScript helps you with every one of that sub problems:
RowList
The first two are dealt with using the classes from .
You can think of a as a ordered representation of your and just like the lists you know it's either an or a of a label, the type of the label and the tail of the .
The idea is to use this to process your 's row-type on the type level (using instances of a class) just like you would use the two cases in the well known list operations. The two cases in the function translates into two instances as you will see bellow.
In order for you to get the corresponding to a row you can use the type class that the purescript compiler will automatically solve for you.
getting values and building records
For the other two problems I'm gonna use the purescript-record packages: Its function let's you retrieve a value from a generic records and you can build up the resulting record by using the functions from the Record.Builder module.
the foundation
OK, I'll just throw the mentioned type class that will deal with the two cases at you:
What's that about? Well obviously what I want is the function - it's task is to return a record- that builds up the flattened record from the there.
With flattened I mean with the field pulled out of the inner records.
- will be a but it is used here more general as a value-level hint to the type.
What's a Proxy? Well proxies helps the compiler to relate values to types using so called singletons. I hope I'll find some time to write about this too but for now please just accept, that it's needed there to help the compiler infer the type of . You can get a hint of why I need this if you look at what you would get without this: does not occur in and there is no functional dependency or anything else that would help the compiler infer what should be. So you help out with which is the only (singleton) value in the type (yes it's a phantom type).
-
will be the source-record with all the nested records.
-
and are the source and target for the
Clearly you need ( is the Record you want to build) - but why do I need here, when it's really about (a builder from the empty record to the desired target record)? Please be patient for a short while - it will hopefully get clear once I get to the instances.
Read it as some kind of accumulator - like you would use for tail-recursive algorithms - for now.
If you have this class the solution is not to hard:
You can read the constraints like this:
- if is a to the record
- and if you know how to get a flatten-Builder from a empty record to the flattened
- where the values are pulled from a (yes the one that is represented by the row-list)
- then this is a function from to .
The implementation asks for the builder using (note the use of the ) and then uses to generate the resulting record from a empty record .
While the type might look horrible it's easy to use:
will return
What remains is to give instances for - so take a deep breath...
instances for Nil and Cons
The idea behind the type-class and the two instances is to fold the structure into a by composing builders that insert labels/values defined by the -nodes in the representation.
As usual the case is rather easy:
This says: If the representation is empty then this instance knows how to return a builder that extents a empty row to a empty one by just returning it's input (s can be composed with , and there is a identity builder).
The case is a bit more involved:
I think it's easier if you first look at the implementation: It returns a composition of two record-builders:
- is a Builder that inserts a new field
- the label has the same name as record-field the instance is looking at via the
- it's value is taken from the field of the records you get by extracting the value corresponding to that label from the input.
- the second one is just the recursive result for the tail of the current case
To get the value this is using the function from and this comes with some constraints:
- the label (here ) needs to be a symbol ()
- the record-row needs to have a label with name - as rows are unordered you can use the type class in and just ignore the remaining-row (I called it for ignore here) - .
You then can get the value using where
- is the proxy value to that symbol
- is the passed source-record.
For the recursive builder you get the constraint which states: can extent a to by inserting all the labels of (using the as a source for the values). Here I use a little trick: marks the target record up to the still missing first label from the case.
The builder is using from which comes with some more constraints:
- needs to be build out of by adding a label with type (which is the type from the nested field) - .
- should not already have a label named - .
The last constraint there is a small technical detail: Actually I want to write the instance but using the record-type in there is not allowed - so I introduced another type-variable and added the type-equality-constraint instead.
That's it - let this settle for a bit and then have another look: it's a lot of constraints but they all follow from what needs to be done and with some time and practice you can follow those leads.
source code
Here is the little program in case you want to play with it:
small exercise
If you want, you can try to extent this in such a way that the inner records can have any number of fields aside from but everything but that one is ignored.
So this should give the same result :
Have fun!