Let me point out another concern with autolifting: it makes it easy to overlook sharing. In the pure world, sharing is unobservable; not so when effects are involved. Let me take the example using the code posted in your first message:
t1 = let x = 1 + 2 in x + x
The term t1 is polymorphic and can be evaluated as an Int or as a distribution over Int:
t1r = t1 ::Int -- 6 t1p = t1 ::Prob Int -- Prob {getDist = [(6,1.0)]}
That looks wonderful. In fact, too wonderful. Suppose later on we modify the code to add a non-trivial choice:
t2 = let x = coin 0.5 + 1 in x + x -- Prob {getDist = [(4,0.25),(3,0.25),(3,0.25),(2,0.25)]}
The result isn't probably what one expected. Here, x is a shared computation rather than a shared value. Therefore, in (x + x) the two occurrences of 'x' correspond to two _independent_ coin flips. Errors like that are insidious and very difficult to find. There are no overt problems, no exceptions are thrown, and the results might just look right. Thus the original code had to be translated into monadic style more carefully: `let' should not have been translated as it was. We should have replaced let with bind, using either of the following patterns:
t2b1 = do x <- coin 0.5 + 1; return $ x + x -- Prob {getDist = [(4,0.5),(2,0.5)]}
t2b2 = coin 0.5 + 1 >>= \xv -> let x = return xv in x + x -- Prob {getDist = [(4,0.5),(2,0.5)]}
After all, let is bind (with the different order of arguments): see Moggi's original computational lambda-calculus. Our example points out that monadifying Int->Int function as m Int -> m Int can be quite dangerous. For example, suppose we have a pure function fi:
fi :: Int -> Int fi x = x + x
and we simple-mindedly monadified it:
fp :: Monad m => m Int -> m Int fp x = liftM2 (+) x x
We can use it as follows: after all, the function accepts arguments of the type m Int:
tfp = fp (coin 0.5) -- Prob {getDist = [(2,0.25),(1,0.25),(1,0.25),(0,0.25)]}
The result shows two independent coin flips. Most of the readers of the program will argue that in an expression (x + x), two occurrences of x should be _correlated_. After all, that's why we use the same name, 'x'. But they are not correlated in our translation. Furthermore, translating let as bind is suboptimal. Consider
t3b2 = coin 0.5 + 1 >>= \xv -> let x = return xv in (5 :: Prob Int) -- Prob {getDist = [(5,0.5),(5,0.5)]}
although we don't use the result of a coin flip, we performed the coin flip nevertheless, doubling the search space. We know that such doubling is disastrous even for toy probabilistic problems. These issues are discussed at great length in the paper with Sebastian Fischer and Chung-chieh Shan, ICFP 2009. http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet