Non-deterministic function/expression types in Haskell?
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
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-... [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.
Hi Oleg, I like monads, really I do. I am just not asking a question about how I can (or should) use monads. I guess we can split my question into two branches: (a) why are monads a perfect solution to my problem? (b) can we extend the HM type system to support non-determinism directly? What I am actually interested in is (b), so I don't want to get sidetracked with (a) if it means ignoring (b). I will think if I can respond to (a) without completely getting side-tracked and ignoring (b). Does that make sense? take care, -BenRI P.S. Thanks for the links!
(a) Non-determism is an effect, e.g. simple list is non-determinism monad, for small discrete distributions! (b) Yes. We can write effectful code "implicitly" - You might look into *Automatically Escaping Monads* - https://www.youtube.com/watch?v=wG8AErq6Bbo, slides: http://benl.ouroborus.net/talks/2016-HIW-Escape.pdf - http://disciple.ouroborus.net/ or https://github.com/DDCSF/ddc Interstingly, while searching for the paper, I stumbled upon Oleg Kiselyov's (not me) paper from *Effects Without Monads: Non-determinism*, which is a different approach. Maybe that's what you are looking after http://okmij.org/ftp/tagless-final/nondet-paper.pdf - Oleg On 11.01.2018 21:41, Benjamin Redelings wrote:
Hi Oleg,
I like monads, really I do. I am just not asking a question about how I can (or should) use monads.
I guess we can split my question into two branches: (a) why are monads a perfect solution to my problem? (b) can we extend the HM type system to support non-determinism directly?
What I am actually interested in is (b), so I don't want to get sidetracked with (a) if it means ignoring (b). I will think if I can respond to (a) without completely getting side-tracked and ignoring (b). Does that make sense?
take care,
-BenRI
P.S. Thanks for the links!
Hi Oleg, Thanks for the links! These are quite interesting. 1. Here is one situation that occurs in evolutionary biology where I would want to have the full range of Haskell syntax available to me. Consider a binary tree, where each tree node has an integer name in [1..num_nodes tree]. The function (parent tree n) gives the parent of node n and (root tree) gives the root node. -- the expected value for a node is the value at its parent mean node tree x | node == root tree = 0 | otherwise = x!!parent tree node -- given a tree, simulate down the tree, simulate_on_tree tree = let x = [sample $ normal (mean node tree x) 1 | node <- [1..num_nodes tree]] My understanding is that you cannot refer to the result of a computation while performing a computation, as in: do {x <- simulate_on_tree tree x} Am I missing something? On 01/11/2018 12:02 PM, Oleg Grenrus wrote:
(a) Non-determism is an effect, e.g. simple list is non-determinism monad, for small discrete distributions!
(b) Yes. We can write effectful code "implicitly" - You might look into *Automatically Escaping Monads* - https://www.youtube.com/watch?v=wG8AErq6Bbo, slides: http://benl.ouroborus.net/talks/2016-HIW-Escape.pdf - http://disciple.ouroborus.net/ or https://github.com/DDCSF/ddc
Interstingly, while searching for the paper, I stumbled upon Oleg Kiselyov's (not me) paper from *Effects Without Monads: Non-determinism*, which is a different approach. Maybe that's what you are looking after http://okmij.org/ftp/tagless-final/nondet-paper.pdf
2. Why would we want to consider non-determinism (in the sense of returning an unpredictable value) as an effect? Certainly running a non-deterministic function does not change global state like modifying an IORef would. I'm also thinking of functions that are (somehow) TRULY random, so they are not keeping a hidden state around somewhere. I'm calling them "non-deterministic" instead of "random" because I want to ignore (for the moment) the probability distribution, and just say that the result is arbitrary. 3. Sampling from a normal distribution gives ONE value, and the list of possible values is .... large :-) [i.e. it would include all Double values.] 4. Interesting - I like his approach to making the box / run instructions implicit. 5. In this paper, it seems that non-determinism means returning ALL possible outcomes. However, what I meant is arbitrarily choosing ONE possible outcome. My terminology is probably being imported from statistics - is there a different word I should use here? -BenRI
Hello, Benjamin. Nature of Haskell is to treat random values under
monad. Because generator returns different values on calls with the same
arguments. So, no way to "declare" such function as "nondeterministic"
function. Haskell is not good language for such job. But there are more
suitable languages for such kind of tasks. If you prefer Haskell-like
syntax, better will be to use ML family language: modern F#, Ocaml or
SML, where IO will not be involved - all is under IO explicitly. But
there is another good choice: *Mercury*. It supports (sure, because it's
declarative language and is based on Prolog) special notations for
computations:
* non-deterministic
* deterministic
* semi-deterministic
* multisolution
(see more about these declarations here:
https://www.mercurylang.org/information/doc-release/mercury_ref/Determinism-categories.html#Determinism-categories)/
/
Also it has type system close to Haskell: with type-families,
existential types, abstract types and so on, also it supports functional
programming totally...
But, I'm sure, no problem to develop some DSL for Haskell which will
hide some details ;)
===
Best regards, Paul
//
12.01.2018 18:26, Benjamin Redelings пишет:
> Hi Oleg,
>
> Thanks for the links! These are quite interesting.
>
> 1. Here is one situation that occurs in evolutionary biology where I
> would want to have the full range of Haskell syntax available to me.
> Consider a binary tree, where each tree node has an integer name in
> [1..num_nodes tree]. The function (parent tree n) gives the parent of
> node n and (root tree) gives the root node.
>
> -- the expected value for a node is the value at its parent
> mean node tree x | node == root tree = 0
> | otherwise = x!!parent tree node
>
> -- given a tree, simulate down the tree,
> simulate_on_tree tree = let x = [sample $ normal (mean node tree
> x) 1 | node <- [1..num_nodes tree]]
>
> My understanding is that you cannot refer to the result of a
> computation while performing a computation, as in:
>
> do {x <- simulate_on_tree tree x}
>
> Am I missing something?
>
>
> On 01/11/2018 12:02 PM, Oleg Grenrus wrote:
>> (a) Non-determism is an effect, e.g. simple list is non-determinism
>> monad, for small discrete distributions!
>
> 2. Why would we want to consider non-determinism (in the sense of
> returning an unpredictable value) as an effect? Certainly running a
> non-deterministic function does not change global state like modifying
> an IORef would. I'm also thinking of functions that are (somehow)
> TRULY random, so they are not keeping a hidden state around
> somewhere. I'm calling them "non-deterministic" instead of "random"
> because I want to ignore (for the moment) the probability
> distribution, and just say that the result is arbitrary.
>
> 3. Sampling from a normal distribution gives ONE value, and the list
> of possible values is .... large :-) [i.e. it would include all
> Double values.]
>
>
>> (b) Yes. We can write effectful code "implicitly"
>> - You might look into *Automatically Escaping Monads*
>> - https://www.youtube.com/watch?v=wG8AErq6Bbo, slides:
>> http://benl.ouroborus.net/talks/2016-HIW-Escape.pdf
>> - http://disciple.ouroborus.net/ or https://github.com/DDCSF/ddc
> 4. Interesting - I like his approach to making the box / run
> instructions implicit.
>
>> Interstingly, while searching for the paper, I stumbled upon Oleg
>> Kiselyov's (not me) paper from
>> *Effects Without Monads: Non-determinism*, which is a different
>> approach.
>> Maybe that's what you are looking after
>> http://okmij.org/ftp/tagless-final/nondet-paper.pdf
> 5. In this paper, it seems that non-determinism means returning ALL
> possible outcomes. However, what I meant is arbitrarily choosing ONE
> possible outcome. My terminology is probably being imported from
> statistics - is there a different word I should use here?
>
> -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.
Hello, Thus quoth PY on Mon Jan 15 2018 at 09:08 (+0100):
But there is another good choice: *Mercury*. It supports (sure, because it's declarative language and is based on Prolog) special notations for computations:
If you prefer a more Haskellish syntax, you may also want to look at Curry : http://www-ps.informatik.uni-kiel.de/currywiki/ Curry has a built-in function called "choice" which allows "non-deterministic, set-valued" functions. Now, whichever tool you use, you are probably going to wind up with monads or with monads in disguise, as Olaf points out. (And sometimes disguise may be quite important.) -- Sergiu
Hi Ben,
Not sure I understand exactly if this what you want, but if the problem is
recursion within monads you might want to take a look at MonadFix or
recursive do notation. If I understood more about how they worked I'd give
an example, but I don't; I just know they're related to recursion in monads.
https://ocharles.org.uk/blog/posts/2014-12-09-recursive-do.html
https://downloads.haskell.org/~ghc/7.8.1/docs/html/users_guide/syntax-extns....
בתאריך יום ב׳, 15 בינו׳ 2018, 5:53, מאת Sergiu Ivanov : Hello, Thus quoth PY on Mon Jan 15 2018 at 09:08 (+0100): But there is another good choice: *Mercury*. It supports (sure,
because it's declarative language and is based on Prolog) special
notations for computations: If you prefer a more Haskellish syntax, you may also want to look at
Curry : http://www-ps.informatik.uni-kiel.de/currywiki/ Curry has a built-in function called "choice" which allows
"non-deterministic, set-valued" functions. Now, whichever tool you use, you are probably going to wind up with
monads or with monads in disguise, as Olaf points out. (And sometimes
disguise may be quite important.) --
Sergiu
_______________________________________________
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.
On Thu, Jan 11, 2018 at 1:41 PM, Benjamin Redelings
(a) why are monads a perfect solution to my problem? (b) can we extend the HM type system to support non-determinism directly?
Yes, there are type systems that express effects differently. No, they don't really do anything different than monads would do. The classic paper on the subject is probably Wadler's "The Marriage of Effects and Monads". http://homepages.inf.ed.ac.uk/wadler/papers/effectstocl/effectstocl.pdf That said, there are a variety of other language features building on the idea of effects. Look for any of the literature on algebraic effects or effect handlers. Many of them use non-determinism as an example. /g -- Prosperum ac felix scelus virtus vocatur -- Seneca
Hi Oleg, On 01/11/2018 09:17 AM, Oleg Grenrus wrote:
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! Just to be clear, I'm not using [N] as an operator on types, but as part of the type. So a type could be something like the pair (Int,D) or (Int,N). In that context a[N][N] is not part of the system.
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. In my other message I posted an example that doesn't fit this very well:
do { x <- f x } does not work, where as let x = f x does work. Basically I'm trying to avoid monads because I want to use the full features of the Haskell language, instead of programming in an embedded language. In that context "more natural" term-level syntax is not sufficient. Also, it seems possible that everything in Haskell COULD be written in a monad. We could eliminate recursive let bindings, and tell people to create a giant state machine which they use by reading and writing IORefs. But then you also eliminate some of the point of using Haskell and may as well go write in C or something. So it seems to me that just because you CAN use a monad doesn't mean you SHOULD use a monad, and the question is "when is a monad better than something else?" Does that make sense? Am I missing something? -BenRI
You seem rather confused as to what a monad is. It is not about "everything is in an IORef", for one. (IO is not the only Monad, nor are the others pretending to be IO.) On Fri, Jan 12, 2018 at 11:38 AM, Benjamin Redelings < benjamin.redelings@gmail.com> wrote:
Hi Oleg,
On 01/11/2018 09:17 AM, Oleg Grenrus wrote:
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!
Just to be clear, I'm not using [N] as an operator on types, but as part of the type. So a type could be something like the pair (Int,D) or (Int,N). In that context a[N][N] is not part of the system.
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.
In my other message I posted an example that doesn't fit this very well:
do { x <- f x } does not work, where as let x = f x does work. Basically I'm trying to avoid monads because I want to use the full features of the Haskell language, instead of programming in an embedded language. In that context "more natural" term-level syntax is not sufficient.
Also, it seems possible that everything in Haskell COULD be written in a monad. We could eliminate recursive let bindings, and tell people to create a giant state machine which they use by reading and writing IORefs. But then you also eliminate some of the point of using Haskell and may as well go write in C or something. So it seems to me that just because you CAN use a monad doesn't mean you SHOULD use a monad, and the question is "when is a monad better than something else?"
Does that make sense? Am I missing something?
-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.
-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
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]
Keep in mind that I don't know the first thing about type systems. I just babble about what feels right. With this said, this sounds like a completely new kind of term to me. Any by "kind", I mean as in "k" or "*". So some of the original examples could look like {-# LANGUAGE KindSignatures, NonDeterminism #-} normal :: Double -> Double -> () -> Double :: n sample :: (() -> a :: n) -> a :: n iid :: Int -> (() -> a :: n) -> [a :: n] constN :: (a :: *) -> (b :: n) -> (a :: *) -- also this: non-deterministic argument, but deterministic result where "n" is a new kind annotation replacing the [N] and the implicit "*" replaces the [D]. So the rules would have to be on the kind-level I suppose? Cheers.
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@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.
participants (9)
-
Alexander Solla -
Benjamin Redelings -
Brandon Allbery -
J. Garrett Morris -
Jake -
MarLinn -
Oleg Grenrus -
PY -
Sergiu Ivanov