[Haskell-cafe] Non-deterministic function/expression types in Haskell?

[Alexander Solla]

The `random-fu` package has a monad called `Random` to
encapsulate/construct random variables (i.e., for simulation).

Whether monads are a "perfect" solution to your problem depends on what
your random variables represent.  In most "finite" cases of jointly
distributed random variables, you can get away with just applicative
functors.  But this wouldn't do if you were modeling something like a
normal random walk.

The sequencing property isn't something you "need" to care about when
you're not using it (unless it causes performance issues).  After all, even
hand-written math is written down "in order", even mathematical expressions
have parse trees with implicit partial orders, etc.

On Thu, Jan 11, 2018 at 8:27 AM, Benjamin Redelings <
benjamin.redelings at gmail.com> wrote:

> Hi,
>
> 0.  Does anyone know of any simple extensions of the HM type system to
> non-deterministic functions?  The reason that I'm asking is that for
> probabilistic programming in the lambda calculus, there are two ways of
> writing expressions:
>
> (a) stochastic: let x = sample $ normal 0 1 in x*x
>
>     or simply (sample $ normal 0 1)^2
>
> (b) "mochastic": do {x <- normal 0 1; return (x*x)}
>
> The "mo" in the second one refers to the use of monads.  That is the
> approach taken in the paper "Practical Probabilistic Programming with
> monads" (http://mlg.eng.cam.ac.uk/pub/pdf/SciGhaGor15.pdf) which I really
> enjoyed.
>
> However, I am interested in the stochastic form here.  There are a number
> of reasons, such as the fact that the monadic representation forces
> serialization on things that need not be serial.  In fact, though, I'm not
> trying to prove which one is best, I am just interested in exploring the
> non-monadic approach as well.
>
> 1. So, is it possible to do a simple extension to the type system to
> express non-determinism?  I found this paper (Implicit Self-Adjusting
> Computation for Purely Functional Programs) that uses "level" tags on types
> to express either (i) security or (ii) changeability.  The first idea (for
> example) is that each type is tagged with one of two "levels", say Public
> and Secure, so that we actually have Int[Public] or Int[Secure].  Any
> function that consumes a Secure value must (i) must return a Secure type
> and (ii) has the arrow in its type labelled with [Secure].  I won't explain
> the "changeable" idea because its kind of complicated, but I am very
> interested in it.
>
> 2. This is kind of tangential to the point of my question, but to explain
> the examples below, it might be important to distinguish sampling from a
> distribution from the distribution itself.  So, normal 0 1 won't generate a
> random sample.  Instead, normal 0 1 () will generate a random sample.  This
> allows us to pass (normal 0 1) to another function which applies it
> multiple times to generate multiple samples from the same distribution.
>
>    -- sample from a distribution dist
>    sample dist = dist ()
>
>    --- take n samples from a distribution dist
>    iid n dist = take n (map sample $ repeat dist)
>
> Here we see some of the value of using the stochastic approach, versus the
> "mochastic" approach: we can use normal Haskell syntax to handle lists of
> random values!
>
> 3. So, I'm wondering if its possible to extend the HM type system to
> handle non-determinism in a similar fashion by either (i) having some
> function types be non-deterministic and/or (ii) having term types be
> non-deterministic.  Taking the second approach, I suggest tagging each
> type with level [D] (for deterministic) or [N] (for non-deterministic).
> Notation-wise, if a determinism level is unspecified, then this means (I
> think) quantifying over determinism levels.  A function that samples from
> the normal distribution we would get a type like:
>
>    normal:: double -> double -> () -> double[N]
>
> Our goal would be that an expression that consumes a non-deterministic
> expression must itself be non-deterministic, and any function that takes a
> non-deterministic input must have a non-deterministic output.   We could
> implement that using rules something like this, where {a,b} are type
> variables and {l1,l2} are level variables.
>
> x:a[l1] :: a[l1]
> \x:a[l1] -> E:b[l2]  :: a[l1] -> b[max l1 l2]
> E[a[l1]->b[l2]] E[a[l]] :: b[l2]
>
> The idea is that max l1 l2 would yield N (non-deterministic) if either
> l1=N or l2=N, because N > D.
>
> 4. Putting non-determinism into the type system would affect GHC in a few
> ways:
>
> (a) we shouldn't pull non-deterministic expressions out of lambdas:
>
>    We should NOT change
>        \x -> let y=sample $ normal 0 1 in y+x
>    into
>       let y = sample $ normal 0 1 in \x -> y+x
>
> (b) we should merge variables with identical values if the types are
> non-deterministic.
>
>    For example it is OK to change
>       let {x=normal 0 1; y = normal 0 1 in (sample x * sample y)}
>    into
>       let {x=normal 0 1} in sample x
>
>    However it is NOT OK to change
>       let {x=sample $ normal 0 1; y = sample $ normal 0 1} in x*y
>    into
>       let {x=sample $ normal 0 1} in x*x
>
> Perhaps this would be useful in other contexts?
>
> 5. If what I've written makes sense, then the types of the functions
> 'sample' and 'iid' would be:
>
> sample:: (()->a[N]) -> a[N]
>
> iid:: Int -> (() -> a[N]) -> [a[N]]
>
> 6.  This is quite a long e-mail, so to summarize, I am interested in
> whether or not there are any simple systems for putting non-determinism
> into HM.  Is the use of tagged types known NOT to work?  Is there are work
> on this that I should be aware of?
>
> Any help much appreciated! :-)
>
> take care,
>
> -BenRI
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180112/af4056f9/attachment.html>