Jason (jcreed) wrote,
Jason
jcreed

Some success imposing at least the constraint that the typechecking algorithm should maintain the invariant that all types and contexts are well-formed, but it's still frustratingly unclear where such an assumption comes from, and especially frustrating realizing that I've assumed it for so many years now without understanding why. I think this also explains why I was confused at wjl's refinements system doing subtly different things at the type/kind level from what I would have naïvely guessed. On the one hand, letting more types into the system is often a conservative extension from the point of view of type inhabitation, but when hacking up twelf code in practice, we absolutely want twelf to tell us when our types aren't valid types according to our already-specified intentions.

Happy primeth birthday to iole200! A whole bunch of people celebrated over at the bar in the poncy mansion-turned-hotel across the street from my house. good times.
Tags: social, work
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 6 comments