Explicit approach to lazy effects For probability monad?

Hi, I'm wondering if people could point me to some background on explicitly representing lazy effects in Haskell? The only effect I am concerned about at this point is `seq`. If there is a way to do this with monads, that would be great. (I know that a lot of people hate lazy effects. However, I think this is an orthogonal issue to the question of how to *represent* lazy effects explicitly.) As background, I'm using a lazy probability monad where random sampling is done with unsafeInterleaveST/IO (or something similar), so that random variables are only sampled if they are actually used: model = do x <- sample $ normal 0 1 -- the interpreter does `unsafeInterleaveIO` to implement 'sample' cond <- sample $ bernoulli 0.5 let y = if cond == 1 then x else 0 return y Here, x is only sampled if cond==1. This has a lot of benefits in procedures like Markov chain Monte Carlo. I initially thought that I could model lazy effects by mapping a -> (a,state) as in the ST monad. However, it seems like lazy effects basically require allowing forked state threads to join CONDITIONALLY on if a value is used/forced, and I don't see how to do that without a source-to-source transformation of functions. It seems like lazy effects require tracking state within each closure, and not globally within the monad interpreter. It kind of seems like this can't work if >>= has type 'm a -> (a -> m b) -> mb', assuming m a = (a,state). The second argument needs to have type (m a -> m b) instead of (a -> m b), since the computation needs to have access to the state produced by the first "m a" computation, in order to (optionally) depend on the state thread for first computation. Does this make any sense? I don't know the literature in this area. Q1. Is there a nice way of representing lazy effects that someone could point me to? Q2. Alternatively, is there a proof that either (i) there is not a monadic way to represent lazy effects, or (ii) fmap f requires a source-to-source transformation (for example to explicitly join state threads on strict operations like ($) and case). -BenRI P.S. As even more background, I'm using a probability monad that allows you to e.g. generate an infinite list of random variables, and only instantiate the ones that are looked at: model = do n <- sample $ geometric 0.5 ys <- sample $ list (repeat $ normal 0.0 1.0) zs <- take n ys return (sum zs) Here the number of random variables (n) can change over time, and I ultimately want effects to happen when they are instantiated. There is a brief overview at http://www.bali-phy.org/models.php

Hi,
On 15. Oct 2019, at 16:59, Benjamin Redelings
I'm wondering if people could point me to some background on explicitly representing lazy effects in Haskell? The only effect I am concerned about at this point is `seq`. If there is a way to do this with monads, that would be great. (I know that a lot of people hate lazy effects. However, I think this is an orthogonal issue to the question of how to *represent* lazy effects explicitly.)
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. http://homes.sice.indiana.edu/ccshan/rational/S0956796811000189a.pdf (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. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.192.7153&rep=rep1&type=pdf#page=8 (Transforming Functional Logic Programs into Monadic Functional Programs) http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.9706&rep=rep1&type=pdf (Verifying Haskell Programs Using Constructive Type Theory) Best regards Sandra

Hi Sandra, Thank you for the references! On 10/15/19 11:10 AM, Sandra Dylus wrote:
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.
http://homes.sice.indiana.edu/ccshan/rational/S0956796811000189a.pdf (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.
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. A function (a->b) would get lifted to (m a -> m (m b)). (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 (ii) the output changes from b to m (m b) so that it still has type (m b) after being unwrapped by the monad. For example, if g takes type (m b) as input, then: 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
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.192.7153&rep=rep1&type=pdf#page=8 (Transforming Functional Logic Programs into Monadic Functional Programs) http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.9706&rep=rep1&type=pdf (Verifying Haskell Programs Using Constructive Type Theory)
Best regards Sandra
participants (2)
-
Benjamin Redelings
-
Sandra Dylus