[PRL] review of proposal

Mon May 23 11:40:40 EDT 2005

I left my feedback at:

http://www.ccs.neu.edu/home/lieber/s/review/

It is not in NSF format but describes my reactions to the proposals that
might help to improve them and also to further local interactions. 

-- Karl

> -----Original Message-----
> From: prl-bounces at lists.ccs.neu.edu
[mailto:prl-bounces at lists.ccs.neu.edu]
> On Behalf Of Matthias Felleisen
> Sent: Monday, May 23, 2005 11:30 AM
> To: PRL Mailing List
> Subject: [PRL] review of proposal
> 
> For the benefit of our junior members, I wrote a review that I would
> almost deliver to NSF for Mitch's proposal. You can hopefully tell
> where I use phrases that are inappropriate and where I left out
> explanations of detailed problems with the proposal. The format is
> almost completely what NSF demands. I left out a few ever-changing
> things. -- Matthias
> 
> MW, Foundational Studies in Programming
> 
> Summary: This proposal is really a combination of two separate,
disjoint
>   mini-proposals.
> 
> The first mini-proposal concerns proofs of observational equivalences.
> The
>   problem is to prove that two phrases in a language are
> indistinguishable
>   in all programs (context) in which they could occur. In the late
60s,
> 70s,
>   and 80s, people studied the theory of observational equivalence in a
>   purely functional context. In the 80s, they turned their attention
to
>   imperative languages. Meyer (later with Sieber) showed in several
> papers
>   how difficult it was to reason about observational equivalence in
the
>   presence of memory allocation and mutation (both in an Algol-like
> setting
>   and in a higher-order setting).
> 
> The PI proposes to study a modification of the bisimulation approach
to
>   this problem. A bisimulation is a maximal-fixpoint approach to
proving
>   observational equivalences (adapted from concurrency to the
sequential
>   world). Through a rather technical looking change to the
conventional
>   definition, the relation can apparently deal with allocation and
> mutation
>   in a surprisingly straightforward manner. The proposal claims (w/o
> proof)
>   that the technique can cope with all of Meyer's puzzles.
> 
> The second mini-proposal concerns the study of syntactic abstraction
> (aka
>   macros), specifically two different aspects: the notion of hygienic
> macros
>   (now standard in Scheme) and macros for languages with
old-fashioned,
>   stupid syntax :-). With respect to hygiene, the proposal first
explains
>   the problem (but see below) and then indicates that the PI and his
>   students have a new way of specifying hygiene as a variation of
>   alpha-equivalence. With respect to macros for conventional syntax,
the
>   proposal is based on Cardelli et al.'s work on extensible languages.
It
>   explains why this is not syntactic abstraction, how to use it for
macro
>   abstraction, and why the resulting system should expand macros in a
> "lazy"
>   rather than an "eager" fashion.
> 
> Evaluation:
> 
> A proposal should explain a problem, describe a solution approach in
>   sufficient detail (or several approaches), and sketch a realistic
> path. It
>   should also compare and contrast its approach with related attempts.
> 
> This proposal succeeds with this for the first mini-proposal but it
> fails
>   almost completely in the second half.
> 
> Observational equivalence: The PI should have explained the topic and
> its
>   relevance so that non-experts on this panel can understand it.
Having
> said
>   this, the proposal clearly forwards an idea on how to tackle this
>   extremely difficult problem from a new angle. I am impressed by the
> kind
>   of puzzles they can solve now. Earlier approaches based on
operational
>   semantics have succeeded in doing some of this, but the PI's
approach
>   appears to be powerful. -- The major problem I have with this part
are
> the
>   exaggerated claims that any of this may apply to OOP (possibly) or
AOP
>   (fantasy land).
> 
> I wish I understood how this compares to approaches based on
> denotational
>   semantics (especially:
> 
> @article{ abramsky99full,
>      author = "Samson Abramsky and Guy McCusker",
>      title = "Full abstraction for {Idealized Algol} with passive
> expressions",
>      journal = "Theoretical Computer Science",
>      volume = "227",
>      number = "1--2",
>      pages = "3--42",
>      year = "1999",
>      url = "citeseer.ist.psu.edu/abramsky98full.html" }
> 
> and other new approaches based on games.)
> 
> Macros: The hygiene problem is explained reasonably well -- for people
> who
>   like parentheses _and_ indentation, though I believe that "hygiene"
is
>   misrepresented in this proposal. (I personally transported the
phrase
> from
>   a Brandregt paper to the first hygiene paper. -- MF) The idea of
using
>   alpha equivalence to model this notion is obvious; almost everyone
who
>   studied the problem starting in 1986 had it. The plan sounds
>   reasonable. What is missing is a new idea. If it is in there, I
missed
>   it. Completely.
> 
>   For the concrete syntax part, the PI and his students are taking a
> novel
>   approach, using Cardelli et al.'s extensible language as a macro
> system. I
>   wish they had included some examples so that I can understand how
they
> did
>   this. I don't even know whether they did it for BASIC or SML/NJ with
>   higher-order functors. Given the writing, it is not obvious what
they
> have
>   accomplished, whether it's research or a cute hack. The discussion
of
> lazy
>   vs eager is entirely appropriate, though extremely abstract. Again,
I
> wish
>   they had explained this with examples. Worse, this part too entirely
>   misses an explanation of how they intend to do better than the
numerous
>   failed approaches from the past, starting with Daniel Weise all the
> way to
>   Maya.
> 
> Details:
> 
> The proposal feels "airy" that is, it wastes a lot of space. It
repeats
> the
>   summary inside the proposal, it doesn't use the full allotment of
> space. I
>   would have liked to see the PI use the extra space to explain things
in
>   sufficient detail.
> 
> -- marked in the proposal --
> 
> Example: You mention macro systems as part of the module system but
you
> completely fail to discuss
> 
> How would your concrete syntax system deal with something like this:
> 
> (module foo mzscheme
> 
>    (m 10)
> 
>    (define-syntax m
>      (syntax-rules ()
>        [(_ x) (printf ">>> ~s~n" x)]))
> 
>    )
> 
> in your system?
> 
> --- more details ---
> 
> PI: The PI is well-known for delivering theoretical results for many
> years,
>   and we can expect that he will do so in the future. According to the
> prior
>   results section, he has also graduated three PhD students over the
past
>   five years.
> 
> Broad Impact: The proposal attempts to explain its impact on the
> context of
>   PL research and CS but the prose is entirely boiler plate. So let's
> hope
>   it will have some.
> 
> 
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl