"pure x :: IO a"是纯值还是具有副作用的值? [英] Is `pure x :: IO a` a pure value or one with a side effect?

问题描述

给予

pure id <*> v = v

持有，pure可以做任何可观察且不违反法律的事情吗?

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

如果我定义一个封装IO的类型并说产生一个新线程，那么GHC可以自由地优化它吗?

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

我终于意识到问题实际上是关于拥有非法IO实例的后果...

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

推荐答案

GHC对类型类定律一无所知(与Idris或Coq不同)，这些定律仅作为文档和编程约定存在.因此，实例可能是合法的，也可能是非法的，无论哪种情况，GHC优化都不会改变程序的行为.

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.

如果编写特定的合法实例，则可以添加REWRITE规则以使GHC删除pure id，GHC可能最终还会在特定的Applicative函子上优化pure id.优化的安全性显而易见.

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.

这篇关于"pure x :: IO a"是纯值还是具有副作用的值?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！