search

hazelgrove / hazelnut-popl17

Submission to POPL 2017
2 stars 1 forks source link

independence of movement from typesystem #37

Closed ivoysey closed 8 years ago

ivoysey commented 8 years ago 
I may be mistaken, but the system for navigating with the cursor seems
completely orthogonal to the type system. It also seems like it is a
special case of something much more general that would apply to any term
signature. I am wondering whether this part of the system could be factored
out and handled completely separately, independently of the type system. As
it is currently, it is like the lambda calculus with a cursor movement
system for allowing a user to navigate around to select a redex to
reduce. Perhaps it would be possible to present a cursor-free version of
the type system in which any subterm matching a rule premise can be a
redex, as in the lambda calculus. If there is some reason this is not
possible, this should be explained.
ivoysey commented 8 years ago

we should bring up the editorializer here; the movements are likely derivable from any type system of a certain form.