<div>Thank you for highlighting these problems; I should really test my own code</div><div>more thoroughly. After reading these most recent examples, the translation to</div><div>existing monads is definitely too neat, and a lot of semantics of the monad are</div>
<div>&#39;defaulted&#39; on. In particular for the probability monad examples I see I had</div><div>the mistaken impression that it would preserve the random-world semantics of</div><div>the do-notation whereas autolifting actually imposes a random-evaluation</div>
<div>semantics, which would not be how I envision an autolifted probabilistic DSL.</div><div><br></div><div>Overall, I think I pretty much got caught up in how cool it was going to be to</div><div>use &lt;$&gt;, &lt;*&gt;, join/enter/exit as primitives to make any monad-based DSL work</div>
<div>&#39;concisely&#39; in an environment of existing typeclasses. That is kind of the</div><div>thing I want to do at a high level; implement DSLs like probabilistic</div><div>programming languages as primitives that that play transparently with existing</div>
<div>expressions.</div><div><br></div><div>But now it seems clear to me that this autolifting approach will not be useful</div><div>with any monad where it is important to control sharing and effects, which is</div><div>critical in the probability monad (and all others I can think of); in fact it</div>
<div>seems necessary to incur the do-notation &#39;overhead&#39; (which I now see is not</div><div>overhead at all!) to work with them meaningfully at all, no matter how &#39;pure&#39;</div><div>they look in other settings. Because of this we see that the Prob monad as it</div>
<div>is defined here is mostly unusable with autolifting. Again, thanks for the</div><div>examples; I think I now have a much better intuition for do/bind and why they</div><div>are required.</div><div><br></div><div>At this point, however, I would still want to see if it is possible to do the</div>
<div>autolifting in a more useful manner, so that the user still has some control</div><div>over effects. Things like the share combinator in the paper you linked will</div><div>probably be very useful. I will definitely go over it in detail.</div>
<div><br></div><div>From my previous experience however, this might also be accomplished by</div><div>inserting something between the autolifting and the target monad. </div><div><div><br></div><div>I think it would be more helpful now to talk more about where I&#39;m coming from.</div>
<div>Indeed, the probability monad examples feature heavily here because I&#39;m coming</div><div>off of implementing a probabilistic programming language in Python that worked</div><div>through autolifting, so expressions in it looked like host language</div>
<div>expressions. It preserved the random-world semantics because it was using a</div><div>&quot;quote&quot;-like applicative functor to turn a function composition in the language</div><div>into an expression-tree rep of the same. I am not sure yet how to express it in</div>
<div>Haskell (as I need to get more comfortable with GADTs), but pure would take a</div><div>term to an abstract version of it, and fmap would take a function and abstract</div><div>term to an abstract term representing the answer. One would then have the call</div>
<div>graph available after doing this on lifted functions. I think of this as an</div><div>automatic way of performing the &#39;polymorphic embedding&#39; referenced in </div><div><br></div><div>[Hofer et al 2008] Polymorphic Embedding of DSLs.</div>
<div><br></div><div>By keeping IDs on different abstract terms, expressions like X + X (where X =</div><div>coin 0.5) would take the proper distributions under random-world semantics. </div></div><div><br></div><div><div>
In general for monads where the control of sharing is important, it can be seen</div><div>as limiting the re-running of effects to one per name. Each occurence of a name</div><div>using the same unwrapped value. </div><div>
<br></div><div>I had the initial impression, now corrected, that I could just come up with an</div><div>autolifting scheme in Haskell, use it with the usual probability monad and</div><div>somehow get this random-world semantics for free. No; control of sharing and</div>
<div>effects is in fact critical, but could be done through using the autolifting as</div><div>a way to turn expressions into a form where control of them is possible. </div><div><br></div></div><div>For now, though, it looks like I have a lot of things to read through. </div>
<div><br></div><div><div>Again, thanks Oleg and everyone else for all the constructive feedback. This</div><div>definitely sets a personal record for misconceptions corrected / ideas</div><div>clarified per day. </div></div>
<div><br></div><div><div><div class="gmail_quote">On Wed, Nov 17, 2010 at 12:08 AM,  <span dir="ltr">&lt;<a href="mailto:oleg@okmij.org">oleg@okmij.org</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
Let me point out another concern with autolifting: it makes it easy to<br>
overlook sharing. In the pure world, sharing is unobservable; not so<br>
when effects are involved.<br>
<br>
Let me take the example using the code posted in your first message:<br>
<br>
&gt; t1 = let x = 1 + 2 in x + x<br>
<br>
The term t1 is polymorphic and can be evaluated as an Int or as a<br>
distribution over Int:<br>
<br>
<br>
&gt; t1r = t1 ::Int        -- 6<br>
&gt; t1p = t1 ::Prob Int   -- Prob {getDist = [(6,1.0)]}<br>
<br>
That looks wonderful. In fact, too wonderful. Suppose later on we<br>
modify the code to add a non-trivial choice:<br>
<br>
&gt; t2 = let x = coin 0.5 + 1 in x + x<br>
&gt; -- Prob {getDist = [(4,0.25),(3,0.25),(3,0.25),(2,0.25)]}<br>
<br>
The result isn&#39;t probably what one expected. Here, x is a shared<br>
computation rather than a shared value. Therefore, in (x + x)<br>
the two occurrences of &#39;x&#39; correspond to two _independent_ coin flips.<br>
Errors like that are insidious and very difficult to find. There are<br>
no overt problems, no exceptions are thrown, and the results might<br>
just look right.<br>
<br>
Thus the original code had to be translated into monadic style more<br>
carefully: `let&#39; should not have been translated as it was. We should<br>
have replaced let with bind, using either of the following patterns:<br>
<br>
&gt; t2b1 = do x &lt;- coin 0.5 + 1; return $ x + x<br>
&gt; -- Prob {getDist = [(4,0.5),(2,0.5)]}<br>
<br>
&gt; t2b2 = coin 0.5 + 1 &gt;&gt;= \xv -&gt; let x = return xv in x + x<br>
&gt; -- Prob {getDist = [(4,0.5),(2,0.5)]}<br>
<br>
After all, let is bind (with the different order of arguments): see<br>
Moggi&#39;s original computational lambda-calculus.<br>
<br>
Our example points out that monadifying Int-&gt;Int function as<br>
m Int -&gt; m Int can be quite dangerous. For example, suppose we have<br>
a pure function fi:<br>
<br>
&gt; fi :: Int -&gt; Int<br>
&gt; fi x = x + x<br>
<br>
and we simple-mindedly monadified it:<br>
<br>
&gt; fp :: Monad m =&gt; m Int -&gt; m Int<br>
&gt; fp x = liftM2 (+) x x<br>
<br>
We can use it as follows: after all, the function accepts arguments of<br>
the type m Int:<br>
<br>
&gt; tfp = fp (coin 0.5)<br>
&gt; -- Prob {getDist = [(2,0.25),(1,0.25),(1,0.25),(0,0.25)]}<br>
<br>
The result shows two independent coin flips. Most of the readers of<br>
the program will argue that in an expression (x + x), two occurrences<br>
of x should be _correlated_. After all, that&#39;s why we use the<br>
same name, &#39;x&#39;. But they are not correlated in our translation.<br>
<br>
Furthermore, translating let as bind is suboptimal. Consider<br>
<br>
&gt; t3b2 = coin 0.5 + 1 &gt;&gt;= \xv -&gt; let x = return xv in (5 :: Prob Int)<br>
&gt; -- Prob {getDist = [(5,0.5),(5,0.5)]}<br>
<br>
although we don&#39;t use the result of a coin flip, we performed the coin<br>
flip nevertheless, doubling the search space. We know that such<br>
doubling is disastrous even for toy probabilistic problems.<br>
<br>
These issues are discussed at great length in the paper with Sebastian<br>
Fischer and Chung-chieh Shan, ICFP 2009.<br>
<br>
<a href="http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet" target="_blank">http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet</a><br>
<br>
<br>
</blockquote></div><br></div></div>