Jason (jcreed) wrote,

Some minor but pleasant breakthroughs trying again to chip away at how unification is supposed to work in HLF. I think I see more what I need to do with the CMTT-ish substitutions.

That line of thought also lead me off on a tangent with an old idea that I keep returning to occasionally, namely how to push thinking of LF in spine form just a little further to appropriately coalesce not just sequences of arguments, but sequences of λs as well. It turns out, I think, that putting the whole calculus 'in substitution form' instead of 'in spine form', is the way to do it. Basically it looks a lot like CMTT, except without the 'M', and every variable is contextual: function types themselves are realized in "lowered" fashion. I write them as Π-types, but basically they are much more like the types (Ψ |- A) from CMTT. The consequence is that many of the syntactic productions collapse in a lovely way, even more so if I also lump in the ideas I had a while ago about polymorphism restricted to base types. In deBruijn form all that remains of the entire syntax of the language is:

Natural Numbers n ::= 0, 1, 2, ...
Atomic Classifiers a ::= type | R
Atomic Terms R ::= n[σ]
Classifiers V ::= ΠΨ.a
Normal Terms N ::= λnR
Substitutions σ ::= id | N.σ
Contexts Γ,Ψ ::= . | Γ,A

That's it! No signature necessary because you can do it all in the context, (although I reckon an implementation would still want a signature for pragmatic reasons, to avoid deBruijn-shift renumberings of frequently-used constants) no unnecessary syntactic distinction between terms and types, and types and kinds, you get some of the laziness benefits of explicit substitutions, and you get a limited form of type operators and polymorphism almost for free.

In the afternoon I went over to the Embassy party, saw some awesome folks, some of which don't usually appear in pittsburgh any more such as damion and theadana and fizzbang.

After that jra1279 appeared with her boyfriend Andy, after some crazy pittsburgh highway hassle, here being en route for them on their way eventually to Milwaukee. It was awesome to finally meet the two of them! We had dinner at JM's and chatted for a while before they headed back to the road.
Tags: math, social, work

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded