Why is Record Builder safe?

Anyone know whether part of the reason record-builder is safe is because its operations are all linear? I ask because this issue needs a review: https://github.com/purescript/purescript-record/pull/44#issuecomment-386327711

I am trying to contribute docs which explain this – future people will ask “Why is this safe? You’re using lots of FFI/unsafeCoerce, so I can’t be sure…”

My understanding is that Record.Builder exposes a pure interface, but implements it using lots of FFI magic. What keeps the interface pure and prevents the magic from blowing up is just careful implementation and testing that no side effects can be observed through the interface.

This also implies trust that whoever implemented the library took care to hide the FFI usage properly.

As was mentioned, this is somewhat analogous to how code that uses ST and memoization works: using side-effects under the hood while keeping the interface pure.

I"ve done some hand waving about the topic once here: https://stackoverflow.com/questions/35985693/combine-records-in-purescript/44139963#44139963 .
For sure I’ve missed linearity part which seems really important so if we get something more precise and accurate here I’m going to link this thread from my stack overflow answer :wink:

Linearity is the key here. If a function argument is consumed exactly once, and that function is the only consumer of its input, then it is safe to modify the argument in-place.

I wrote a bit about the idea here. Using Category (i.e. the BCI basis if you add flip) is very much a watered-down version of linear lambda calculus, but enough for our purposes.

4 Likes