>> a = allSolutions coin ++ [coin] ++ allSolutions coin
>>
>> b = let x = coin
>> in allSolutions x ++ [x] ++ allSolutions x
>
>The (first) result for a and b is [0,0,0] with weak encapsulation. However
>this does not mean that a and b are equivalent under weak encapsulation as
>you will notice when asking for more solutions. In particular, a has 8
>solutions with weak encapsulation whereas b has only 2.
yes, because Curry's nullary function (global '=') vs value (local '=')
binding distinction interprets 'coin' differently from 'x'. and 'allSolutions'
passes 'coin' or 'x' to 'findall', via a parameter binding, thus sharing
any choices instead of passing them into the capsule.
>> coinW = wrap (0?1)
>>
>> c = let x = coinW
>> in allSolutions (unwrap x) ++ [unwrap x] ++ allSolutions (unwrap
>> x)
>
>No. With weak encapsulation c is equivalent to either a or b (depending on
>whether function declarations are eta-expanded or not), i.e., it has either
>eight or two solutions and the first of them is [0,0,0].
i don't think eta conversion is valid in a language with implicit
non-determinism and reduction to weak head normal form:
'a -> {ND} b' is observably different from '{ND} (a->b)'.
still, the other result was surprising (to me). it implies that
not only the named 'x', but also the anonymous choice '(0?1)'
within it is shared. short of some full lazyness transformation at
work, i couldn't see at first where that sharing was coming from
(see below for the step i missed).
>> am i missing something?
>
>Probably call-time choice. The non-deterministic choice between 0 and 1 is
>tied to the call (0?1) and not the evaluation of (0?1) (wherever this
>happens).
i am aware of that, i think (see the other thread;-). it means that
let x=(0?1) in x+x --> 0+0 ? 1+1 -- two, not four results
nevertheless, we also have
let x=(0?1) in 2+2 --> 2+2 -- one, not two results
which means that the choice is tied to the named binding 'x' for
'(0?1)', but triggered by the evaluation of 'x', after entering the
'let'-body (call-time). which is why i think that call-time-choice
is a misnomer (perhaps call-site-choice?).
my problem turns out to be slightly more subtle, so it might be
worth elaborating on the point i missed: i expected
(a) let x=\f->(f (0?1)) in x id + x id
--> 0+0?1+0?1+1?0+1
and similarly, with 'wrap g f = f g' and 'unwrap w = w id'
(b) let x= wrap (0?1) in unwrap x + unwrap x
--> 0+0?1+0?1+1?0+1
the problem is 'similarly'. (a) is correct, but (b), which i used as
'equivalent', is not. is that obvious to Curry programmers?-)
in deterministic call-by-need, we have 'wrap g == \f-> f g', but
in non-deterministic call-by-need, these two differ observably,
because they differ in sharing. in essence, i expected partial
applications, which are values, to be substituted without
additional sharing, whereas call-by-need first lifts out (and
hence shares) the partial bindings, then substitutes what is left:
let wrap = \g->\f->f g in let x= wrap (0?1) in ..x..x..
--> {let-V}
let wrap = \g->\f->f g in let x= (\g->\f->f g) (0?1) in ..x..x..
--> {gc}
let x= (\g->\f->f g) (0?1) in ..x..x..
--> {let-I}
let x= (let g= (0?1) in \f->f g) in ..x..x..
--> {let-A}
let g= (0?1) in let x= (\f->f g) in ..x..x..
it is that last step that lifts out the binding for the choice, before
substituting the remaining abstraction for 'x', which means that
all the partial applications in the body share the binding for 'g',
which leads to the observable difference.
so, we'd need to wrap directly in lambda, without 'wrap'/'unwrap':
coinA f = f (0?1)
g = let x = coinA
in allSolutions (x id) ++ [x id] ++ allSolutions (x id)
allSolutions g = findall (\x->x=:=g)
-- Goal: g :: [Int]
-- Result: [0,1,0,0,1] ?
thanks,
claus
>PS: Rather than guessing the weak encapsulation semantics, you might try to
>run your examples with the Münster Curry compiler, whose try primitive uses
>weak encapsulation.
i'd love to, but Curry developers do not seem to like windows
users!-) in fact, i downloaded both PAKCS and Muenster Curry
before i read the requirements:
PAKCS doesn't even consider windows:
"The current version of PAKCS runs on Unix-based platforms"
Muenster Curry is more helpful, and suggests that the Cygwin build
tools plus a gcc and a Haskell compiler should be all that is needed.
unfortunately, that doesn't seem to be quite accurate, as it seems
to rely on the *cygwin gcc*, not any gcc. my current setup is typical
for ghc builds: cygwin build tools, but *mingw gcc*, to produce
proper, cygwin-lib-free windows executables. works fine for ghc.
i understand that relying on cygwin's runtime on windows saves
developer effort, ghc used to do that, too, years ago. but nowadays,
mingw gcc is prefered for ghc builds and installing both cygwin and
mingw gcc tends to lead to a mess. since the main additions of
Curry over Haskell are logic variables and non-determinism, neither
of which should be platform-dependent, couldn't a ghc-based Curry
implementation rely on ghc's networking et al support, instead of
cygwin's?
for the moment, it seems i'm stuck with PAKCS' www interface
and pencil/paper interpretation of the Curry report. that is still not
'guessing' - weak encapsulation should correspond to call-by-need
plus non-determinism, for which i have my own core calculus
implementation. but it is easy to misinterpret informal reports or
to mis-model high-level features at the core calculus level, my own
implementation is still evolving, and the only easiliy accessible
Curry implementation doesn't implement weak encapsulation, so
i can't test ideas directly.
under these circumstances, do people mind if i try to (in-)validate
my observations by asking here? after all, it should be possible to
understand Curry basics without an implementation.
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Mai 07 2007 - 16:11:07 CEST