Pure functions referring an array can be impure due to FFI

I found a problem of PureScript’s Array while I was thinking about the purity of my functions for the Table type after reading this thread.

For example:

module ExampleImpure where

import Prelude

import Effect (Effect)
import Effect.Console (log)
import Data.Array as Array

foreign import push1 :: Array Int -> Effect Unit

main :: Effect Unit
main = do
  let xs = []
      -- `f` should be pure, but the result of `f 0` changes by
      -- the push1 function!
      f y = Array.length xs + y

  log $ "BEFORE push1: " <> show (f 0)
  push1 xs
  log $ "AFTER push1: " <> show (f 0)

And ExampleImpure.js:

exports.push1 = xs => () => xs.push(1);

Then running ExampleImpure shows this output:

BEFORE push1: 0
AFTER push1: 1

Here the result of f implicitly gets mutated by the FFI function even though f is typed as a pure function.

This behavior sounds very natural if you know that [] in PureScript is just an array in JavaScript, but is never ideal and could cause a bug hard to find.

There are several solutions of this problem:

  1. Wrap any functions reading an Array with Effect.
    • But this would be infeasible and make Array useless!
  2. Use another immutable type in a library for Array (and its literal).
  3. Do nothing. FFI functions can always be an exception!
    • But adding some warnings about this problem somewhere would be good.

IMO the last option is the most practical and this problem isn’t so big that we have to make such a big change. But as far as I searched there are no public warnings of it, that’s why I shared here.

This problem actually applies to more than Array; everything except types that are immutable in JS too, like Int, Number, and String, are vulnerable. I’m not very knowledgeable about how to prevent mutations of vulnerable types, but I’m pretty sure it would increase the code size a lot for little benefit, so it’s unlikely to happen. Also, note that I am speaking only about the JS backend. This may not apply to other backends.

1 Like

PureScript has the Array type and it treats it as an immutable array of values. The runtime representation of this type is the same as for the regular JavaScript array. This shouldn’t be a problem because the type system should ensure an Array never gets mutated.

However, when you write foreign import ..., you’re telling the compiler “Hey, here’s this value in the JavaScript FFI file. Treat it as if it has this PureScript type. Trust me!” The compiler doesn’t check if the given type signature makes sense for the provided value or if you’re mutating provided arguments that should be immutable. It has to trust you that you’ve made sure the signature is correct and everything checks out. In the case of push1, it doesn’t. You’ve lied to the compiler! :angry: :angry: :angry:

How do we get around this limitation? We need to stop lying! Much like unsafeCoerce and friends, FFI allows us to do things which would otherwise be impossible or impractical due to type system limitations. Since we’re skirting around the type checker in these cases, we’re the ones who have to make sure everything stays sane under the hood.

8 Likes

Putting this into non-FFI code, you’re writing this:

import Control.Monad.ST as ST
import Data.Array.ST as STA

main :: Effect Unit
main = do
 let xs = []
 log $ "Before: " <> show (Array.length xs)

 -- not sure whether this will run the ST code
 -- but assume it does for example's sake
 let runMe = void $ ST.run do
    xsArr <- STA.unsafeThaw xs
    STA.push 1 xsArr

 log $ "After: " <> show (Array.length xs)

This isn’t a problem with Array per say but a problem with the one who mutated the array elsewhere.

unsafeThaw = “trust me” thaw.

3 Likes

I was very confused as to what was going on, specifically because of the 1-2 output. So I tried it myself and got what I would expect to happen, which was an output of

BEFORE push1: 0
AFTER push1: 1

Did you make a mistake or do you actually get 1 and 2? No one else seems to have brought this up.

2 Likes

Thank you! I’ve fixed!