I figured out how to type check/synth all of the middle bits of Hurken's paradox. turns out the sole cause of issues is the one bug I have with my bidi algo

This is pretty cool because it seems like with a few strategically-placed displacements, crude-but-effective is just as effective as universe polymorphism

Someone has got to come up with a better name for crude-but-effective it's way too long. Favonia et al. had the opportunity and then didn't and continued calling it crude-but-universal which is longer and more boring


Anyway this is a rather exciting development bc this shows the type theory is actually useful (thank goodness!) and all I need to do is fix the type checker bug and I want to do it now but I need to be asleep right NOW

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.