8

We know that in Prolog - non-deterministic predicates are a feature used to whittle down combinatorial problems.

In Haskell we see some similar non-deterministic behaviour to Prolog in the List Monad.

In Haskell we also see non-determinism in choosing thunk evaluation order:

But there is nothing telling GHC which of those thunks should be evaluated first, and therefore GHC is at full liberty to choose whichever thunk to evaluate first.

This is fascinating - and somewhat liberating. I'm wondering (apart from noodling with logic problems like eight-queens) what principle this serves. Was there some big idea or big problem they were trying to solve with non-determinism?

My question is: What is the reasoning behind making non-determinism a feature of Haskell?

  • Because Haskell thunk evaluation is referentially transparent (pure), so the order has no effect on the result. It's not non-deterministic programming in the sense of Prolog where one of many possible results is chosen. – Jack Dec 30 '17 at 1:29
  • Sure, but when you’re designing a Compiler surely it is more work to add the non-determinism? What motivates you to put the extra work in? – hawkeye Dec 30 '17 at 1:33
  • 2
    The standard doesn't define the order of evaluation. The standard doesn't force the compiler to choose a specific order. It doesn't mean that the compiler is somehow choosing randomly or something like that. The compiler does choose the order deterministically, according to its own rules. It's just that the rules aren't defined by the standard, and are left as a compiler implementation detail. – Fyodor Soikin Dec 30 '17 at 2:30
  • Thanks @FyodorSoikin - that's helpful. I'm not concerned with whether it is the compiler or the standard - merely the intention behind the design choice. Why do it? What do you get out of this? – hawkeye Dec 30 '17 at 2:52
  • 1
    By not including a specific order of evaluation in the standard you get the freedom for the compiler to change it however it sees fit, thus enabling optimizations. This is pretty standard stuff. Even microprocessors mess with instruction order if they can prove that it doesn't affect the result. – Fyodor Soikin Dec 30 '17 at 3:40
19

While it is true that both aspects cited in the questions appear as forms of non-determinism, they are indeed quite different both in how they work and in their goals. Hence any answer has to be necessarily split in two parts.

Evaluation order

Haskell mandates no particular execution order in the evaluation of thunks essentially because of two reasons.

  1. First of all, Haskell is a purely functional language, so you are guaranteed to have referential transparency (if you don't mess around with unsafePerformIO & co.). This means that the evaluation of any expression, e.g. f x will result in the same outcome no matter how many times it is evaluated and no matter in which part of the program it is evaluated (assuming f and x bind to the same values in the considered scopes, of course). Hence mandating any particular order of execution would have no purpose, because changing it would not produce any observable effects in the outcome of the program. In this regard, this is not really a form of nondeterminism, at least not any form of observable one, since the different possible executions of the program are all semantically equivalent.

Changing order of execution can, however, have an effect on the performance of the program, and leaving the compiler the freedom of manipulating the order at its will is fundamental to achieve the amazing performance that a compiler like GHC can obtain compiling such an high-level language. As an example, think about a classic stream-fusion transformation:

map f . map g = map (f.g)

This equality simply means that applying two functions to a list with map has the same outcome than applying once the composition of the two functions instead. This is only true because of referential transparency, and is a kind of transformation that the compiler can always apply, no matter what. If changing the order of execution of the three functions had effects on the result of the expression, this would not be possible. On the other hand, compiling it in the second form instead of the first may have a huge performance impact, because it avoids the construction of one temporary list and only traverses the list once. The fact that GHC can automatically apply such transformation is a direct consequence of referential transparency and the non-fixed order of execution and it is one of the key aspects of the great performance that Haskell can achieve.

  1. Haskell is a lazy language. This means that any particular expression is not required to be evaluated unless its result is actually needed, and this could as well be never. Laziness is a sometimes debated feature and some other functional languages avoid it or limit it to be opt-in, but in the context of Haskell it is a key feature in the way the language is used and designed. Laziness is another powerful tool in the hands of the compiler's optimizer, and most importantly allows code to be composed easily.

To see what I mean by ease of composition, consider an example when you have a function producer :: Int -> [Int] that performs some complex task to compute a list of some sort of data from an input argument, and consumer :: [Int] -> Int which is another complex function computing a result from a list of input data. You have separately written them, tested them, optimized them very carefully, and used them in isolation in different projects. Now in the next project it happens that you have to call consumer on the result of producer. In a non-lazy language this may be non-optimal, since it may be the case that the combined task may be most efficiently implemented without building a temporary list structure. To obtain an optimized implementation you would have to reimplement the combined task from scratch, re-test it, and re-optimize it.

In haskell this is not needed, and calling the composition of the two functions consumer . producer is perfectly fine. The reason is that the program is not required to actually produce the whole result of producer before giving it to consumer. In fact, as soon as consumer will need the first element of its input list, then the corresponding code from producer will run as far as needed to produce it, and no more. When the second element is needed, it will be computed. If some element will not be needed by consumer, it will not be computed at all, effectively saving useless computations. The execution of consumer and producer will effectively be interleaved, not only avoiding the memory usage of the intermediate list structure, but also possibly avoiding useless computations, and the execution would probably be similar to the hand-written combined version that you had to write yourself otherwise. This is what I meant by composition. You had two well-tested and performant pieces of code and you could compose them obtaining for free a well-tested and performant piece of code.

Nondeterministic monads

The use of nondeterministic behavior provided by the List monads and similar ones is instead totally different. Here the point is not that of providing the compiler with means of optimizing your program, but clearly and concisely express computations that are inherently nondeterministic.

An example of what I mean is provided by the interface of the Data.Boolean.SatSolver library. It provides a very simple DPLL SAT solver implemented in Haskell. As you may know, solving the SAT problem involves finding an assignment of boolean variables that satisfies a boolean formula. There may be more than one such assignments, however, and one may need to find any of them, or iterate over all of them, depending on the application. Hence, many libraries will have two different functions like getSolution and getAllSolutions. This library instead has only one function, solve, with the following type:

solve :: MonadPlus m => SatSolver -> m SatSolver

Here, the result is a SatSolver value wrapped inside a monad of unspecified type, which however is constrained to implement the MonadPlus type class. This type class is the one that represent the kind of nondeterminism provided by the list monad, and in fact lists are instances. All the functions that operate on SatSolver values returns their results wrapped into a MonadPlus instance. So suppose you have the formula p || !q and you want to solve it by restricting on the results that set q true, then the usage is the following (variables are numbered instead of being identified by name):

expr = Var 1 :||: Not (Var 2)

task :: MonadPlus m => m SatSolver
task = do
  pure newSatSolver
  assertTrue expr
  assertTrue (Var 2)

Note how the monad instance and the do notation mask all the low-level details of how the functions manages the SatSolver data structure, and lets us express clearly our intent.

Now, if you want to obtain all the results, you simply use solve in a context where its result has to be a list. The following will print all the results on screen (assuming a Show instance for SatSolver, which does not exist, but forgive me this point).

main = sequence . map print . solve task

However, lists are not the only instances of MonadPlus. Maybe is another instance. So if you just need one solution, no matter which one, you can just use solve as if it returned a Maybe SatSolver value:

main = case solve task of 
  Nothing -> putStrLn "No solution"
  Just result -> print result

Now suppose that you have two tasks so built, task and task2, and you want to obtain a solution to either one. Once again everything comes together to let us compose our pre-existing building blocks:

combinedTask = task <|> task2

where <|> is a binary operation provided by the Alternative typeclass, which is a super class of MonadPlus. This again let us clearly express our intent, reusing code without changes. The nondeterminism is clearly expressed in code, not buried under the details of how the nondeterminism is actually implemented. I suggest you to take a look at the combinators built on top of the Alternative type class to get further examples.

The nondeterministic monads like lists are not just a way to express nice exercises but offers a way to design elegant and reusable code that clearly expresses intent in the implementation of tasks which are inherently nondeterministic.

  • I don't think your task implementation is quite right. assertTrue takes two parameters, and you're only giving one. You still need a little bit more explicit piping of the SatSolver value between the functions if you're going to use do notation. – 4castle Jan 2 '18 at 0:39
  • Ah! The first version I was writing used a chain of >>=, so you could (and had to) avoid naming the argument. This seems a case where do notation is more verbose. Feel free to edit, or I’ll do it as soon as I get back to office. – gigabytes Jan 2 '18 at 2:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.