<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Sandra,</p>
<p>Thank you for the references!</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 10/15/19 11:10 AM, Sandra Dylus
wrote:</div>
<blockquote type="cite"
cite="mid:19EB8AB6-D6DB-4A6E-9C19-0C453F81B0B9@web.de">
<pre class="moz-quote-pre" wrap="">if you’re explicitly interested in sharing computations (rather than only modelling non-strictness) then the following approach by Fisher, Kiselyov and Shan might be of interest.
<a class="moz-txt-link-freetext" href="http://homes.sice.indiana.edu/ccshan/rational/S0956796811000189a.pdf">http://homes.sice.indiana.edu/ccshan/rational/S0956796811000189a.pdf</a> (Purely functional lazy nondeterministic programming)
The are modelling the functional logic language Curry, but have also some remarks about modelling a lazy probabilistic language with their approach.
If you’re not interested in the sharing part of laziness, the paper might be a good first starting point nonetheless. They use a deep monadic embedding that you can use to model non-strictness. Other papers that use such an encoding are the following.
</pre>
</blockquote>
<p>Their function 'share :: m a -> m (m a)' is interesting: I
think the double wrapping m (m a) suggests how one could handle
lazy effects in a monad.</p>
<p>A function (a->b) would get lifted to (m a -> m (m b)). <br>
</p>
<p>(i) the input changes from a to (m a) so that the function itself
can decide whether to include the effect of the input into the
output</p>
<p>(ii) the output changes from b to m (m b) so that it still has
type (m b) after being unwrapped by the monad.</p>
<p>For example, if g takes type (m b) as input, then:<br>
</p>
<pre>do
x <- f args -- if f has return type (m b) then x has type b
y <- g x -- but x needs to have type (m b) here
return y
-BenRI
</pre>
<blockquote type="cite"
cite="mid:19EB8AB6-D6DB-4A6E-9C19-0C453F81B0B9@web.de">
<pre class="moz-quote-pre" wrap=""><a class="moz-txt-link-freetext" href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.192.7153&rep=rep1&type=pdf#page=8">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.192.7153&rep=rep1&type=pdf#page=8</a> (Transforming Functional Logic Programs into Monadic Functional Programs)
<a class="moz-txt-link-freetext" href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.9706&rep=rep1&type=pdf">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.9706&rep=rep1&type=pdf</a> (Verifying Haskell Programs Using Constructive Type Theory)
Best regards
Sandra</pre>
</blockquote>
</body>
</html>