It is never safe to cheat

Anyone who has spent time trying to implement an FRP library knows the unsafePerformIO story. You may use unsafePerformIO as long as you ensure that the result maintains purely functional semantics. It’s possible to create impure values with unsafePerformIO. It is up to you to “prove” that you have created a pure one. Seems like a decent trade-off.

unsafeperformio

I put “prove” in quotes for a reason. If you’re doing something nontrivial (i.e. you’re not just using unsafePerformIO . return), you need an operational semantics for IO to prove this. But that’s not all! You are probably depending on some external state inside the unsafePerformIO, which depends on the time and order in which thunks are evaluated. But thunks aren’t part of the operational semantics of IO, they are part of the operational semantics of pure values in Haskell — something we quite explicitly do not have. So you need not only to embrace the ill-definedness of IO, but in fact tie yourself down to a particular operational interpretation of Haskell!

Let’s say I write an HNF evaluator for Haskell. Your unsafePerformIO magic will probably not work on this style of evaluator because the meaning of thunks — and the way they are executed — is quite different in this style.

There are more invariants on a Haskell function than purity and referential transparency. We can of course only implement computable functions. They have to be monotone and continuous. And they might be other things, as well, which someone one day will come along and prove by leveraging properties of the type system, exposed primivites, etc. (see ST for prior art). But they have not accounted for your magic, so their analysis does not include any program using your library.

We are pure functonal programmers. We have chosen a language which vastly restricts what we are allowed to do, because we understand the benefits we reap as a result. However, pretending to understand when we are allowed to cheat only buys us the benefits we know about now, but precludes future benefits from work in the field. By using unsafePerformIO — even in a safe way (or so you think) — you avert the exponential growth of our field.

If you find you can’t express something you feel you should be able to, I suggest one of two things: (1) look deeper until you find an incidental limitation of the language, and attempt to solve it at the language level, or (2) look deeper until you understand why you actually shouldn’t have been able to do that, revealing the truth from behind the curtain of zealous ignorance. In my experience, (2) is much more often successful.

On a more practical note, most of said limitations are about performance, which is not in the semantics’ domain of discourse. It makes sense that our languages wouldn’t be good at such things. Instead of introducing a hack, why not push the field forward and think about what a language which can talk about such things would look like? Each time you run into a limitation, you have a new use case, and thus a new perspective on the problem.

Until that problem is solved, though, your library users might have to pay the price of not having as elegant an interface. But by restricting yourself thusly, you are protecting yourself from your own ignorance, at least knowing that what you have made should, in fact, be makeable.

In summary: It is never safe to cheat.

About these ads

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s