On 20.01.2011, at 22:18, Daryoush Mehrtash wrote:
I am having hard time understanding the following paragraph in "Purely functional Lazy non-deterministic programing" paper http://www.cs.rutgers.edu/~ccshan/rational/lazy-nondet.pdf
The problem with the naive monadic encoding of non-determinism is that the arguments to a constructor must be deterministic. If these arguments are themselves results of non-deterministic computations, these computations must be performed completely before we can apply the constructor to build a non-deterministic result.
Why does the argument to constructors must be deterministic? WHy is it that thunks are not used in this case?
If you use a monadic model for non-determinism in Haskell you use the standard constructors provided by Haskell and the bind operator to apply it to a non-deterministic (monadic) value. For example, consider the non-deterministic value coin defined as follows. coin :: MonadPlus m => m Bool coin = False `mplus` True To apply the constructor Just to this value you use the bind operator as follows. test :: MonadPlus m => m (Maybe Bool) test = coin >>= return . Just If you now consider the following definition. loop = MonadPlus m => m Bool loop = loop If we apply Just to loop as follows test2 :: MonadPlus m => m (Maybe Bool) test2 = loop >>= return . Just the evaluation of test2 does not terminate because >>= has to evaluate loop. But this does not correctly reflect the behaviour in a functional logic language like Curry. For example, if you have a function that checks whether the outermost constructor of test2 is Just, the test is supposed to be successful. In the naive model for non-determinism this is not the case. Cheers, Jan