Re: prelude extension proposal

From: Wolfgang Lux <>
Date: Fri, 14 Oct 2005 11:01:21 +0200

Hi Bernd!

> This is a really good point. Thus convinced, I would like to add some
> definitions to the proposal, as this is how we handle non-determinism
> in
> the prelude of the new Curry implementation, following the proposal of
> the mentioned paper:
> [...]
> data SearchTree a
> = Fail
> | Value a
> | Or [SearchTree a]
> | Suspend

IIUC, the main difference between the paper and your proposal is the
introduction of the Suspend constructor in SearchTree. Looking at the
definitions of allValuesD and allValuesB, Suspend is always handled like
a failure. Furthermore, PAKCS' implementation of getSearchTree cannot
return Suspend at all. On the other hand, MCC could return Suspend when
an encapsulated search suspends, but the underlying implementation can
better: It resumes a suspended search once the uninstantiated non-local
variable, which was causing the suspension, is bound.

Here is a little contrived example that demonstrates why a simple
constructor is not general enough (at least for MCC's implementation of
encapsulated search).

> import AllSolutions
> data Nat = Z | S Nat
> le Z _ = success
> le (S m) (S n) = le m n
> notAbove n | m `le` n = m where m free
> main =
> do
> t <- getSearchTree (notAbove lim)
> let solns = allValuesD t
> doSolve (x =:= head solns)
> print x
> doSolve (y =:= head (tail solns) & lim =:= S (S Z))
> print y
> where x, y, lim free

This will print the two lines
   S Z
However, this wouldn't work if getSearchTree returned Suspend when an
encapsulated search suspends (unless of course the compiler is smart
enough to figure out that is should perform the unification lim =:=
S (S Z) *before* computing the second solution).


curry mailing list
Received on Fr Okt 14 2005 - 12:23:00 CEST

This archive was generated by hypermail 2.3.0 : Mo Okt 26 2020 - 07:15:03 CET