Dear Curry fans,
> Your issues relate to the Curry topics of using trees to collect output
> and to 'encapsulated search'. But I am the wrong person to say something
> about this. Seems to have largely to do with concealing non-determinism
> with IO.
i thought this last statement reflected a rather strange point of view (strange
to me, i mean;-), so i tried to find out more. from a search of the mailing list
archive, i was led to this paper as the likely origin:
http://www.informatik.uni-kiel.de/~mh/publications/papers/JFLP04_findall.html
Encapsulating Non-Determinism in Functional Logic Computations [1]
Bernd Braßel, Michael Hanus, Frank Huch
Journal of Functional and Logic Programming, No. 6, 2004
which i found rather exciting. first, the tree representation of search
spaces, followed by suitable traversals, as suggested in [1], is very close to
one of the main suggestions in my 1991 MSc thesis, which i abstracted here
in the earlier thread, and even if the authors weren't aware of my suggestions,
it is nice to see them validated after so long (i must be getting old;-). second,
in focussing on the interactions of encapsulation and sharing, and in giving an
operational semantics, the paper clearly went beyond my own work, and
identified some serious and unexpected issues afflicting the call-by-need
variation of these ideas, so this seemed like the ideal opportunity to link
myself back in to the current FLP research stream.
[about myself: i have focussed on functional programming in Haskell in
recent years, but have this year restarted my language design experiments
at the level of core calculi, and to get a basis for executable specifications
of such calculi, i am also developing an embedding of small-step,
language-level operational semantics in Haskell; given my background,
it is not surprising that the first things i added after the basic call-by-need
calculus were non-determinism and logic variables. there are several
avenues i want to explore from here, encapsulated search based on a
tree representation of the search spaces being one of the aspects i had
considered solved, before seing the sharing issues raised in [1] ]
unfortunately, my enthusiasm did not last long, as the compelling analysis
of the issues was followed by design decisions that i find hard to agree
with (limitation of encapsulated search to IO), and the operational
semantics was given at the level of an abstract machine instead of the
level of the language itself. i will try to express my concerns here, in the
hope of restarting the interesting discussions that followed the paper back
in 2004. ideally, this might lead to a redesign of Curry's encapsulated
search, but if you could convince me that this ideal is not practical, that
too would be a useful outcome, for my own experiments.
since the analysis in [1] is so compelling, it would be hard to challenge,
so if i am unhappy with the conclusions, and if the analysis seems to lead
more or less directly to these conclusions, i must try to shake the
assumptions on which the analysis of the issues is based. if i can suggest
a suitably different perspective on the symptoms, then a different analysis
might lead to different conclusions, without invalidating the chain of logic
presented in that paper.
let me start with the statements i can agree with:
- in an FLPL combining sharing with non-determinism, sharing
becomes observable
- if we want to provide encapsulated search within a pure FPL, it
is desirable to contain all non-functional effects to the capsules
- it is possible to extend an FLP with observable sharing
http://citeseer.ist.psu.edu/claessen99observable.html
Observable Sharing for Functional Circuit Description [2]
Claessen and Sands, 1999
nevertheless, we do not want such an extension to happen
accidentally, in the form indicated in the problematic examples
provided in [1]
- it is possible to "contain" non-determism in the IO monad
http://research.microsoft.com/~simonpj/Papers/imprecise-exn.htm
A semantics for imprecise exceptions [3]
Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow,
Fergus Henderson. PLDI'99, Atlanta.
as i mentioned before, exceptions can be seen as parameterised
failure, and imprecise exceptions add non-determistic generation
of such exceptions. the solution proposed in [3] is to contain the
_observation_ of such non-determism to the IO monad, very much
like the encapsulation of search in [1], which adds logic variables.
nevertheless, we would prefer the encapsulation of search to be
pure, not IO-bound, if at all possible.
- even if we just want to provide encapsulated search within an FLPL,
violations of referential transparency, as demonstrated in [1], are
highly undesirable
so far, so good, i hope? now for my first objections:
- the examples in [1] assume extensions of an FLPL, not an FPL.
in particular, the main issue does not seem to be the interaction
of sharing and encapsulation, but the interaction of non-local and
local (encapsulated) non-determinism, mediated via sharing.
the early examples assume a "function" coin, which is not a function
at all - it is a non-deterministic expression bound to an identifier, and
the non-determinism is not encapsulated. thus, these examples do not
apply to an FPL with encapsulated search, and in an FLPL, the
effects observed are due to the non-encapsulated non-determinism
in coin.
these distinctions might be hard to observe in Curry, where
deterministic evaluation and generation of non-determistic alternatives
are just two views of the same function definition. it would be helpful
to make potential sources of non-determinism more explicit, and to
distinguish them from deterministic code.
- strong encapsulation proposes to "cut" any sharing that might affect
the results of encapsulated search, but [1] immediately provides
examples that show how the sharing in effect when an encapsulated
search is evaluated can depend on the order of evaluation outside.
if there was no non-determinism outside the capsule, sharing would
not seem to have any effects other than the known observability of
sharing _of non-determinism_ _inside_ the capsule. to observe
sharing _outside_ the capsule, we would have to probe it with
non-determinism, which we can only obtain _inside_ the capsule,
and can only pass to expressions from outside the capsule as
parameters, which are _always shared_.
what would happen if, instead of closing out sharing, we were to
close out sources of non-determinism not originating within the
same capsule? as a first approximation, we might chose to embed
non-nested encapsulated search within a deterministic FPL, as a
refinement, we might try to use different sets of operators for
non-local and local non-determinism, and to tag non-determinism
arising within different capsules (similar to the tagging of state
references in local state transformer monads in Haskell).
it seems that we could then choose whether (a) to import an
external source of non-determinism into a capsule, or (b) to
prevent such import, forcing propagation of such external
non-determinism outside the capsule (depicted here as <..>):
let x = 0 ? 1 in <.. x ..> --a--> <.. (0?1) ..>
let x = 0 ? 1 in <.. x ..> --b--> <.. 0 ..> ? <.. 1 ..>
variation (a) seems to suffer from evaluation order dependency,
and is, in effect, the starting point of the discussion in [1], but
variation (b), not mentioned in [1], does seem to be free of such
issues. it does not matter whether or not the external non-determinism
is propagated before the capsule is evaluated or not, because it will
definitely be propagated outwards before any of its branches can
enter the capsule. note the difference in approach, compared to
strong encapsulation, eg in example 1.3 in [1]. also note that, if
variation (b) is indeed order-independent, the main reasons for
which [1] suggests to impose sequencing of encapsulated search
are no longer present.
- i find it intriguing that, while [1] argues for strong and against weak
encapsulation, it seems to provide only a single example against
the latter (compared to several against the former). following
variation (b) above, both expressions in that example (1.4) would
be equivalent. to obtain a non-singleton encapsulated result, one
would have to associate the non-determinism in coin with that of
the capsule.
as this discussion starter has already grown rather long, i'll leave it
here, for now, to see whether it rings any bells among the list members.
claus
> if you feel like trying out your ideas in Curry, there's a quite usable
> web-interface:
>
> http://www-ps.informatik.uni-kiel.de/~mh/pakcs/curryinput_c2p.cgi
actually, the web-interface (nice, but for somewhat terse error messages)
has to rule out IO, and thus encapsulated search in the IO-based form, right?
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Apr 27 2007 - 08:25:36 CEST