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

[Benjamin Redelings]

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