hazelgrove / hazelnut-popl17

Submission to POPL 2017
2 stars 1 forks source link

partial evaluation with holes #38

Closed ivoysey closed 8 years ago

ivoysey commented 8 years ago
To what extent can one precompile or partially evaluate in the presence of
holes?
ivoysey commented 8 years ago

it seems like this reviewer, C, didn't understand what we meant when we talked about the dynamics

ivoysey commented 8 years ago

we said

Section 6.6 discussed the possibility of defining a dynamic (operational)
semantics for incomplete H-expressions based on CMTT. Evaluation could
proceed until a hole appeared in an elimination position. Compilation
relies on a theory of evaluation, so it could be considered after
developing this theory. It would also be interesting to explore the
intersection of incremental computation and our action semantics -- many of
the computations necessary for compiling a term could be reused when
compiling the term that arises from performing an action on it.
ivoysey commented 8 years ago

reviewer D brought this up too:

Section 3: "We are not concerned here with defining a dynamic semantics for
Hazelnut" I can imagine defining semantics for the hole-less subset, but
what would be the purpose of a dynamic semantics for the entire language?