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

[Oleg Grenrus]

Hi Benjamin

Let's see what you ask for, you have *new* syntax for types:

    a[N] and a[D]

what are a[N][N] or a[N][D] or a[N][D] or a[D][D]?

Aren't they a[N], a[N], a[N] and a[D] respectively?
That's what monads are about!

So

   a[N] ~ Distr a
   a[D] ~ Identity a ~ a

No need to complicate type-system! You just to not be afraid of monads!

Monads aren't sequencing, they are computational context.

I guess, you just want more natural term-level syntax.

You can use ApplicativeDo [1] (in GHC-8.0+), so e.g.

    do x <- normal 0 1
       y <- normal 0 1
       return (f x y)

will be transformed into

    liftA2 f (normal 0 1) (normal 0 1)

That's almost like

    f (normal 0 1) (normal 0 1)

if you have proper syntax highlighting ;)

Note: various term syntax extensions been proposed.
E.g. idiom brackets in the "Applicative programming with effects" [2]:

   (| f (normal 0 1) (normal 0 1) |)

to mean

   pure f <*> normal 0 1 <*> normal 0 1

which is equivalent to above liftA2 expression. If you like that, you
can check
"the Strathclyde Haskell Enhancement", it supports idiom brackets.

[1]
https://www.microsoft.com/en-us/research/publication/desugaring-haskells-do-notation-into-applicative-operations/
[2] http://strictlypositive.org/IdiomLite.pdf
[3] https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/

On 11.01.2018 18:27, Benjamin Redelings 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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180111/3630ca68/attachment.sig>