[Haskell-cafe] Help on syntactic sugar for combining lazy & strict monads?
Olaf Klinke
olf at aatal-apotheke.de
Fri Jul 30 21:33:29 UTC 2021
On Thu, 29 Jul 2021, Benjamin Redelings wrote:
> Hi Olaf,
>
> I think you need to look at two things:
>
> 1. The Giry monad, and how it deals with continuous spaces.
I believe I understand the Giry monad well, and it is my measuring stick
for functional probabilistic programming. Even more well-suited for
programming ought to be the valuation monad, because that is a monad on
domains, the [*] semantic spaces of the lambda calculus. Unfortunately, to
my knowledge until now attempts were unsuccessful to find a cartesian
closed category of domains which is also closed under this probabilistic
powerdomain construction.
[*] There are of course other semantics, domains being one option.
>
> 2. The paper "Practical Probabilistic Programming with Monads" -
> https://doi.org/10.1145/2804302.2804317
Wasn't that what you linked to in your original post? As said above,
measure spaces is the wrong target category, in my opinion. There is too
much non constructive stuff in there. See the work of Culbertson and
Sturtz, which is categorically nice but not very constructive.
>
> Also, observing 2.0 from a continuous distribution is not nonsensical.
>
> -BenRI
Perhaps I am being too much of a point-free topologist here. Call me
pedantic. Or I don't understand sampling at all. To me, a point is an
idealised object, only open sets really exist and are observable. If the
space is discrete, points are open sets. But on the real line you can not
measure with infinite precision, so any observation must contain an
interval. That aligns very nicely with functional programming, where only
finite parts of infinite lazy structures are ever observable, and these
finite parts are the open sets in the domain semantics.
So please explain how observing 2.0 from a continuous distribution is not
nonsensical.
Olaf
>
> On 7/21/21 11:15 PM, Olaf Klinke wrote:
>>> However, a lazy interpreter causes problems when trying to introduce
>>> *observation* statements (aka conditioning statements) into the monad
>>> [3]. For example,
>>>
>>> run_lazy $ do
>>> x <- normal 0 1
>>> y <- normal x 1
>>> z <- normal y 1
>>> 2.0 `observe_from` normal z 1
>>> return y
>>>
>>> In the above code fragment, y will be forced because it is returned, and
>>> y will force x. However, the "observe_from" statement will never be
>>> forced, because it does not produce a result that is demanded.
>>
>> I'm very confused. If the observe_from statement is never demanded, then
>> what semantics should it have? What is the type of observe_from? It seems
>> it is
>> a -> m a -> m ()
>> for whatever monad m you are using. But conditioning usually is a function
>> Observation a -> Dist a -> Dist a
>> so you must use the result of the conditioning somehow. And isn't the
>> principle of Monte Carlo to approximate the posterior by sampling from it?
>> I tend to agree with your suggestion that observations and sampling can not
>> be mixed (in the same do-notation) but the latter have to be collected in a
>> prior, then conditioned by an observation.
>>
>> What is the semantic connection between your sample and obsersvation monad?
>> What is the connection between both and the semantic probability
>> distributions? I claim that once you have typed everything, it becomes
>> clear where the problem is.
>>
>> Olaf
>>
>> P.S. It has always bugged me that probabilists use elements and events
>> interchangingly, while this can only be done on discrete spaces. So above I
>> would rather like to write
>> (2.0==) `observe_from` (normal 0 1)
>> which still is a non-sensical statement if (normal 0 1) is a continuous
>> distribution where each point set has probability zero.
>
More information about the Haskell-Cafe
mailing list