Proposal: make Ref.new pure in Effect and ST

Change Proposals
#1

I propose adding the following two functions to the refs and st packages:

  • new' :: forall s. s -> Ref s
  • new' :: forall a r. a -> STRef r a

And then rewrite the current new as new a = pure $ new' a.

The proposal comes from extensive work with purescript-event and finding myself often needing to create an event with a push function in a non-effectful context. The signature for create is currently create :: forall a. Effect (EventIO a), but the Effect just exists so that Ref.new can be called: otherwise, it could be written create :: forall a. Unit -> EventIO a.

The effectful nature of new creates a weird situation in the internals of the event library, where unsafePerformEvent is called in a pure function just to make an event. This usage of unsafePerformEvent winds up being is necessary in other situations as well when working with purescript-events. If new were a pure function, on the other hand, event creation could be pure as well.

So that’s the upside of the proposed new'. The downside is that it gets into murky waters of what a pure function is. If the definition of a pure function is that it must always return the same output for a given input, you can argue that new' :: a -> Ref a is pure because the two references, at their moment of creation, are equal. At the same time, it doesn’t make sense for Ref a to have an Eq instance, so even though the function is conceptually pure, it is not demonstrably pure.

Back to the upside, this change would get rid of several unsafePerformEffect-s spread over various libraries and web apps.

Thoughts?

#2

Maybe this is nitpicky but IMHO for something to be considered pure it needs to be referential transparent - meaning you can replace the assigned name with the expression without changing the meaning of the code.

In this sense I think new' cannot be pure as you cannot replace the assigned name with the call to new' without changing the program.

I understand the need but I’d prefer to keep it pure.

2 Likes
#3

That’s an interesting take on it - I still need to fully process it, but there’s an argument that the condition “you can replace the assigned name with the expression without changing the meaning of the code” holds here.

Example 1

a :: Int
a =
  let
    b = new' 0
    c = b
  in
    42

b :: Int
b =
  let
    b = new' 0
    c = new' 0
  in
    42

In Example 1, both a and b yield 42, even though one replaces the assigned name with the expression and the other doesn’t.

Example 2

a :: Effect Int
a = do
  let
    b = new' 0
    c = b
  write c 42
  read b

b :: Int
b = do
  let
    b = new' 0
    c = new' 0
  write c 42
  read b

In example 2, the programs are different. However, we are in the Effect context in example 2, where there is no contract that two executions of the same program will yield the sam result.

**

It could be, however, that I don’t fully understand the meaning of Effect. My intuitive understanding comes from Learn You a Haskell where the author contrasts pure functions to the IO monad:

While this may seem a bit limiting when you’re coming from an imperative world, we’ve seen that it’s actually really cool. In an imperative language, you have no guarantee that a simple function that should just crunch some numbers won’t burn down your house, kidnap your dog and scratch your car with a potato while crunching those numbers.

When we are in Effect, we are in the land of kidnapped dogs and scratched cars, so all bets are off, whereas in the pure function from Example A it’s impossible to change the control flow of the program.

#4

I guess it depends on your take on Effect/IO - I think there is a way to interpret Effect-values in a way that the value/expression itself is pure - side-effect only enter when the runtime evaluates main - at least that’s my understanding on Haskell-IO and why Haskell is still considered a pure language.

But you are right - this case is a bit mind-boggling and confusing.

But if you have new as an Effect then I think you can still argue that new 42 is referential transparent as this is not the reference but an Effect generating a new reference and it’s indeed irrelevant if I write

a :: Effect Int
a = do
   let new42Ref = new 42
   r1 <- new42Ref
   r2 <- new42Ref
  ...

or

a :: Effect Int
a = do
   r1 <- new 42
   r2 <- new 42
  ...

Don’t know if this is helpful but can you see the point?

I think/feel that’s it is clear that new indeed involves some side-effects (create a new/fresh initialized reference) and that it’s type should reflect that.

3 Likes
#5

That’s a good point, it’s a good argument for disallowing the pure version.

#6

Newb here

This is interesting.

I’ve generally thought of Ref as exposing underlying implementation details that you otherwise can safely abstract away in a pure language. There’s some extra bit of information (an opaque token of some sort) that you put alongside the value a Ref holds that lets you use the Ref, right?

new' :: a -> Ref a is pure because the two references, at their moment of creation, are equal

My gut-check here goes the opposite way. If a is the same, the returned Ref a still needs to somehow generate that token (for example, a memory location I suppose). In the pure new' that token must also be identical (how else could you memoize new'?). Which isn’t very useful.

My expectation is that every new Ref I make is unique.

At the same time, it doesn’t make sense for Ref a to have an Eq instance

If it were possible to inspect the token, then token equality would be Ref equality? I would think that two refs with the same token, but different values should be a bug. Two Refs with different tokens may hold equal values for a time but are fundamentally not the same thing.

1 Like
#7

Ref can’t be created purely because you need a value restriction (see any ML which has refs). If it’s allowed to be “pure”, then you can implement unsafe coerce.

2 Likes
#8

To be clear:

maybeRef :: forall a. Ref (Maybe a)
maybeRef = new Nothing

maybeString = maybeRef :: Ref (Maybe String)
maybeInt = maybeRef :: Ref (Maybe Int)

example = do
  Ref.write (Just "ok") maybeString
  someInt <- Ref.read maybeInt
  pure $ add 1 <$> someInt

The type with Effect restricts it so that the result can’t itself be polymorphic, replicating the ML value restriction.

In order to be pure and sound, type abstraction through forall would have to be runtime relevant, and actually introduce a new reference when applying a type.

8 Likes
#9

Exactly. You can also read it in the documentation of GHC’s unsafePerformIO: System.IO.Unsafe

1 Like