hazelgrove / hazelnut-popl17

Submission to POPL 2017
2 stars 1 forks source link

sensibility and delete #35

Closed ivoysey closed 8 years ago

ivoysey commented 8 years ago
“The deletion rule for Z-expressions in analysis changes not just the
expression being deleted but also the inferred type.  Does this “action
outside the hole” cause any difficulties?”
ivoysey commented 8 years ago

we said

The deletion rule in analytic position does change the type itself, but the
new type -- being the hole type -- is consistent with every type, so there
is no difficulty (indeed, if there were, the corresponding case of
Sensibility would fail to go through.)

which we should note in the text possibly