type level programming with records

Just like in Elm you can define functions like this:

This function give you the value contained in the foo :: String-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 foo of type String 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 # k can be used for every kind k - for example PureScript used rows of effects until recently to enumerate all side-effects a value can produce (see Eff) - 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 Rows 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 Row consists of things and the order of things does not matter - (a,b) and (b,a) 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:

Map Label (NonEmptyList Type)

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 Rows 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 Row 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 getElement 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 getElement helper.

The function splits the problem into two parts or cases:

  • an empty list
  • a list head : tail

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:

  1. Deal with an empty record
  2. Deal with an record that is made up of a head-field/value pair and tail-part
  3. Find some way to extract the nested value from the head
  4. 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 Prim.RowList.

You can think of a RowList as a ordered representation of your Row and just like the lists you know it's either an Nil or a Cons of a label, the type of the label and the tail of the RowList.

The idea is to use this to process your Record'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 RowList to a # Type row you can use the RowToList 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 get 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 flattenBuilder function - it's task is to return a record-Builder that builds up the flattened record from the Record row there.

With flattened I mean with the input field pulled out of the inner records.

  • g rl will be a RLProxy but it is used here more general as a value-level hint to the rl 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 rl. You can get a hint of why I need this if you look at what you would get without this: rl does not occur in Record row -> Builder (Record from) (Record to) and there is no functional dependency or anything else that would help the compiler infer what rl should be. So you help out with RLProxy which is the only (singleton) value in the RLProxy rl type (yes it's a phantom type).

  • Record row will be the source-record with all the nested { input : SomeType } records.

  • from and to are the source and target for the Record.Builder

Clearly you need to (Record to is the Record you want to build) - but why do I need from here, when it's really about Builder (Record ()) (Record to) (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 Flatten class the solution is not to hard:

You can read the constraints like this:

  • if rl is a RowList to the record Record row
  • and if you know how to get a flatten-Builder from a empty record to the flattened Record out
  • where the values are pulled from a Record row (yes the one that is represented by the rl row-list)
  • then this is a function from Record row to Record out.

The implementation asks for the builder using flattenBuilder (note the use of the RLProxy) and then uses Builder.build 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 Flatten - so take a deep breath...


instances for Nil and Cons

The idea behind the type-class and the two instances is to fold the RowList structure into a Record.Builder by composing builders that insert labels/values defined by the Cons-nodes in the RowList representation.

As usual the Nil case is rather easy:

This says: If the RowList 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 (Record.Builders can be composed with <<<, >>> and there is a identity builder).

The Cons 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:

  • first is a Builder that inserts a new field
    • the label has the same name as record-field the instance is looking at via the Cons
    • it's value is taken from the input field of the records you get by extracting the value corresponding to that label from the Record row input.
  • the second one is just the recursive result for the tail of the current Cons case

To get the value this is using the get function from Builder and this comes with some constraints:

  • the label (here name) needs to be a symbol (IsSymbol name)
  • the record-row row needs to have a label with name name - as rows are unordered you can use the Cons type class in Prim.Row and just ignore the remaining-row (I called it ig for ignore here) - Row.Cons name { input :: ty } ig row.

You then can get the value using get namep rec where

  • namep is the proxy value to that symbol name
  • rec :: Record row is the passed source-record.

For the recursive builder flattenBuilder tailp rec you get the constraint Flatten tail row from from' which states: flattenBuilder can extent a Record from to Record from' by inserting all the labels of tail (using the rec as a source for the values). Here I use a little trick: from' marks the target record up to the still missing first label from the Cons case.

The builder first is using insert from Record.Builder which comes with some more constraints:

  • to needs to be build out of from' by adding a label name with type ty (which is the type from the nested input field) - Row.Cons name ty from' to.
  • from' should not already have a label named name - Row.Lacks name from'.

The last constraint there TypeEquals ty' { input :: ty } is a small technical detail: Actually I want to write the instance Flatten (Cons name { input :: ty } tail) row from to but using the record-type in there is not allowed - so I introduced another type-variable ty' 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:

module Main where

import Prelude

import Data.Symbol (class IsSymbol, SProxy(..))
import Effect (Effect)
import Effect.Console (log)
import Prim.Row as Row
import Prim.RowList (kind RowList, Nil, Cons, class RowToList)
import Record (get)
import Record.Builder (Builder)
import Record.Builder as Builder
import Type.Equality (class TypeEquals)
import Type.Row (RLProxy(..))


main :: Effect Unit
main = log $ show result


result :: { bar :: Int, baz :: { text :: String }, foo :: String }
result = 
  flatten { foo : { input : "Answer"}
          , bar : { input : 42 }
          , baz : { input: { text: "everything" } } 
          }


flatten :: forall row rl out . RowToList row rl => Flatten rl row () out => Record row -> Record out
flatten rec = Builder.build (flattenBuilder rlp rec) {}
    where
      rlp = RLProxy :: RLProxy rl


class Flatten (rl :: RowList) (row :: #Type) (from :: #Type) (to :: #Type) | rl -> row from to where
  flattenBuilder :: forall g . g rl -> Record row -> Builder (Record from) (Record to)


instance flattenNil :: Flatten Nil row () () where
  flattenBuilder _ _ = identity


instance flattenCons ::
    ( Flatten tail row from from'
    , IsSymbol name
    , Row.Cons name { input :: ty } ig row
    , Row.Lacks name from'
    , Row.Cons name ty from' to
    , TypeEquals ty' { input :: ty }
    ) => Flatten (Cons name ty' tail) row from to where

    flattenBuilder _ rec = first <<< flattenBuilder tailp rec
      where
        first :: Builder (Record from') (Record to)
        first = Builder.insert namep inner.input

        inner :: { input :: ty }
        inner = get namep rec

        namep = SProxy :: SProxy name

        tailp = RLProxy :: RLProxy tail

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 input but everything but that one is ignored.

So this should give the same result { bar: 42, baz: { text: "everything" }, foo: "Answer" }:

Have fun!