Jason (jcreed) wrote,

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

  • (no subject)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded