Is `pure x :: IO a` a pure value or one with a side effect?

Question

Given

pure id <*> v = v

holds, can pure do anything observable and not break the law?

If I define a type that encapsulates IO and say, spawn a new thread, is GHC free to optimize it away?

EDIT: I finally realized that the question actually is about consequences of having an unlawful instance of IO...

Florencia

I think free theorems might have a result about this? It's been a while since I've read the paper. – Rooseveltroost

Answer 1

GHC does not know anything about type class laws (unlike e.g. Idris or Coq), those only exist as documentation and programming convention. Hence, an instance can be lawful or unlawful, and in either case GHC optimization will not alter program behavior.

If you write a specific lawful instance, then you can perhaps add a REWRITE rule to get GHC to remove pure id, and GHC may also end up optimizing pure id away in specific Applicative functors, where the safety of this optimization is apparent.

Albigenses

I understand that GHC does not check or take advantage of laws in general. But this is a very simple case where "optimization" could be made even by mistake. Is there any guarantee that no such optimization takes place unless instructed in code? – Florencia

Correct answer to a twisted question :) – Florencia

Answer 2

I have to separate your question into two questions:

Is pure x :: IO a a pure value or one with a side effect?

A virtually pure value. In this code, x's type is a, which is a pure value.
And pure's type is a -> IO a, which wraps the argument with IO but actually without any side effect.
So pure x :: IO a seems to have a side effect in its type, but actually doesn't have.

... can pure do anything observable and not break the law?

No. pure just applies id against the result of side effect caused by v.
As long as the instance follows the Applicative law, it is not pure but v that causes the side effect.

I guess you take x in pure x for v :: IO a in pure id <*> v.
The former is a completely pure value whose type is a, and the latter is not a pure value: an action which can cause a side effect returning a value whose type is a.

And the final question:

If I define a type that encapsulates IO and say, spawn a new thread, is GHC free to optimize it away?

Sorry, I'm not sure of the optimization.

Throwback