# Re: Intended meaning

From: Sergio Antoy <antoy_at_redstar.cs.pdx.edu>
Date: Fri, 09 Nov 2007 05:29:56 -0800 (PST)

Wolfgang and Bernd,

Thanks for your comments. I am leaving for New York, so only a

The program was:

> t = let x free in (f x ? g x)
> f True = success
> g False = success

Wolfganag writes:

> > 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).
>
> And this is the point I do not understand. In 3. you have chosen
> to narrow the narrex (f x), which means that x is instantiated to
> True. So if x is shared (as you admit), then the only possible
> reduction is
> 3. t -> success ? g True
> and likewise for 4. By using an independent and unconstrained
> generator (True ? False) for the variable x in (g x) you break
> the sharing.

f False = failed

The meaning of the program should remain the same, but the step
in question becomes much more plausible.

Bernd writes:

> 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.

I call it narrowing for lack of better term.

> 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"?

This is a good point. I do not know. 0 and 1 should be generated
because they make a difference. Any other value should not
matter.

> 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.