Re: Pull tabbing with variables

From: Michael Hanus <>
Date: Mon, 21 Dec 2015 17:46:58 +0100

Hi Andy,

the behavior you see is due to the distinction between
free variables and generators. Although this distinction
is somehow irrelevant from a semantical point of view,
it is essential to implement unification of free variables.
For instance, the result of solving the equational constraint

> x =:= (y :: [Bool]) where x,y free

should be just one answer (binding x and y to the same variable)
instead of infinitely many results if x and y are handled
as generators. Therefore, KiCS2 has a tag for generators
which shows whether this generator is a variable or a choice.
Initially, each free variable in the program is tagged as
a "variable", but when it is narrowed, the variable tag is replaced
by a "choice" tag.

Now, consider your example: Operation g does nothing with its
argument, so the tag is not changed. However, operation f
narrows its argument, therefore the tag is changed before
the actual narrowing takes place. Note that the tag change
is not done in place since we compile to Haskell, i.e., other
occurrences of y have still the "variable" tag.

Altogether, we obtain two results:

- from g: S y (where the tag on y is not changed)

- from f: Z

Since the REPL checks the tags before printing a choice
value, it prints in the first case (S _x2), although
the value behind _x2 is a choice.

The actual implementation is a bit more advanced
(due to the implementation of encapsulated search), but the basic
ideas of this scheme are described in our PADL'13 paper, see

I hope this explanation was helpful.

Best regards,


On 12/17/2015 04:00 PM, Andy Jost wrote:
> Consider the following program:
> data Peano = S Peano | Z
> f (S Z) = Z
> g a = a
> main = f x ? g x where x=S y; y free
> KiCS2 produces the correct answers, (S _x2) and Z; my question is about=

> how it does so.
> We know KiCS2 will replace y with the generator (S _x) ? Z, and we migh=
> naively expect f to execute a pull tab step so that f x and g x share
> the expression x = (S (S _x)) ? (S Z). Note that the choice arising
> from the generator is now above S in (the original) x. (I ignore the
> unlikely possibility that we simply got lucky by evaluating g x before =
f x.)
> If the above is accurate, then the program would output (S (S _x)), (S
> Z), and Z. So something else must be going on. I don’t recall seein=
> any mention of this issue in the published work about KiCS2.
> Can anyone explain what accounts for this behavior? One theory I have
> is that the shared subexpression is not shared after the pull-tab step.=
> That would seem to imply some inefficiency, but Brassel’s dissertatio=
> contains a section on the benefits of sharing subexpressions in KiCS2,
> so I’m not sure.
> Any help is appreciated!
> -Andy
> _______________________________________________
> curry mailing list
> curry_at_lists.RWTH-Aachen.DE
> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

curry mailing list

Received on Mo Dez 21 2015 - 17:47:58 CET

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:04 CEST