Thanks, Sergio, this is a very clear description and I finally fully
understand the problem you wanted to address.
> t has 3 narrexes (4 steps). I think you disagreed with this
> statement in the past, but I insist.
>
> 1. t -> let x free in f x
> 2. t -> let x free in g x
> 3. t -> success ? g (True ? False)
> 4. t -> f (True ? False) ? success
>
> In the narrowing step, I bound the free variable x to (True ?
> False) rather than only True or only False, because variables may
> be shared (indeed x is shared in this case).
Just out of curiosity: Why do you call such a step a "narrowing step"?
What is becoming more narrow by it? My guess is that this might be the
root of all the misunderstandings in the mailing list that people would
normally assume that it is at least possible that the search space
becomes smaller because of a narrowing step.
One point to remark is that it is not feasible to execute
steps 3 and 4 if your integers are solely given in a primitive way. You
would have to "narrow" to (0?1?-1?2?-2?...) Do you want to do this for
functions "f 1 = success" and "g 0 = success"? I am asking this because
it directly relates to your problem as one of the very main reasons to
have residuation as a language construct is the existence of types
like integers.
Therefore I see two solutions to this:
a) allow residuation only on such built-in types, e.g., have functions
"ensureInt :: Int -> Int " and
"ensureFloat :: Float -> Float"
"ensureIOHandle :: IOHandle -> IOHandle"
and then live with the incompleteness for such types.
b) suspend also on non-deterministic choices, e.g.
> 3. ... g (True ? False)
does not evaluate any further as g is rigid.
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Nov 09 2007 - 14:37:37 CET