Inconsistent sharing behavior for effects in Haskell

[MajaRet]

Description

Haskell displays some rather inconsistent behavior regarding the sharing of impure values. For example, consider the following Haskell program:

shareFunction = let g = \_ -> trace "effect" 21 in g () + g ()

Evaluating it in GHCI gives the following result:

> shareFunction
effect
effect
42

The effect is triggered each time the shared function is evaluated.

On the other hand, consider this program, which uses const instead of an anonymous function:

shareConst = let g = const $ trace "effect" 21 in g () + g ()

When this version is evaluated, the effect is only triggered once:

> shareConst
effect
42

To add to this, if the same expression is defined within the REPL and evaluated, it behaves like its counterpart with the lambda again:

> let shareConst = let g = const $ trace "effect" 21 in g () + g ()
> shareConst
effect
effect 
42

Similar results can be observed with non-deterministic expressions in Curry (compiled with PAKCS).

Given that these inconsistencies exist, we cannot accurately model Haskell's behavior in Coq in all situations. We will have to investigate the rules and inconsistencies more closely and then decide on the semantics we want to model.

Update: In fact, expressions defined in the REPL do not appear to feature sharing for let expressions at all:

> let x = trace "effect" 1 in x + x 

is evaluated to

effect
effect
2

Lambdas still cause sharing:

> (\x -> x + x) (trace "effect" 1) 
effect
2