Why `deref` is effectful?

[cblp]

deref seems to have no side effects. Why is it bound to Ivory type?

There is a freshName call and statement emission in the source of deref.

What if deref was emitting expression? And freshName is not needed, it is a work for the CSE optimizer.

This should make code much easier.

By the way, reading volatile memory must be effectful, but Ivory can't work with volatile currently.

[leepike]

@cblp Thanks for the comment, and sorry for the very late reply.

In talking with @elliottt, there are few reasons:

• It keeps the option open to add volatile support.
• In the beginning, we didn't have the CSE optimizer.
• It prevents some possible confusion with doing a let binding to a deref expression that has different values if used in different locations, if memory is written to in between.

Besides, I think it is too big of a change to entertain at this point.

[cblp]

It keeps the option open to add volatile support.

There may be a separate effectful deref for volatile variable, and a "pure" deref for non-volatile variable only.

[cblp]

It prevents some possible confusion with doing a let binding to a deref expression that has different values if used in different locations, if memory is written to in between.

Hm, this makes sense a little. But it shouldn't be confusing for a haskeller.

Besides, I think it is too big of a change to entertain at this point.

What if I do this?

[leepike]

By "too big of a change", I was more referring to the (at least) ~250k LOCs of Ivory code I know about in the wild.

[cblp]

We can do it in several years. Introduce new function, mark old function as deprecated, remove it some years later.

[cblp]

Hm... I think analogy with readIORef may be involved. Reading from external resource is an impure effect.

[leepike]

Yes, agreed about the analogy.

In any event, I don't think we'll make this change in the GaloisInc version of Ivory we're supporting, given the backwards incompatibility and it hasn't been a hinderance to have it as an effect.