Jason (jcreed) wrote,

I may have to abandon my distaste for "spineless" canonical-forms LF. The reason: unless I'm mistaken, second projection from a Σ winds up inexorably awful in spine form. You have to keep around the term somehow, to know what to substitute into the second type in the pair. The usual synthesis rules work fine on the other hand, though they still seem to require an atomic-for-atomic substitution.

On the other hand the weird PTS view on things is still holding up, and obviates the need even for a signature, since type family declarations can be shoved into mere Π-types.
Tags: lf, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded