Nice job, thanks for posting this!
Inspired by you, I tried my hand at a different presentation of a bidirectional type checker for a dependently typed lambda calculus. My emphasis was different:
I focussed on providing a presentation that directly represented the judgements of the theory in the program, complete with a notion of analytic and synthetic judgement.
I experimented with really nice error tracing for type errors (judgement refutations).
I used Unbound to avoid having to deal with fiddly integer parameters and substitutions. I like the convenience of Unbound, but it comes at a price: severe anti-modularity.
I also have a cumulative, predicative hierarchy of universes, as well as an intensional identity type.
I do not have inferable and checkable terms in separate syntactic categories, nor do I have a type of “values”. It would be interesting to improve my representation in this way, and then implement NBE.
The main bit of my type checker is here: https://github.com/jonsterling/itt-bidirectional/blob/master/src/TT/Judgement/Bidirectional.hs, but do browse the other files.
I read the “Simple Easy!” paper long ago, but this presentation is quite a bit easier to digest w.r.t. the plain nuts and bolts of your bidirectional type checker. Thanks for writing it up, Danny!
Yeah, I didn’t mean to but I guess I ended up with a nice presentation of Simple Easy!
I’m still entirely dissatisfied with how bindings are handled :/ Since it’s like all the warts of DeBruijn with some of the quirks of explicit names with just a dash of odd HOAS tossed in. Variables are hard, we should just use SKI.
Ha, yes. I found that weird in SE! too, otoh it also serves as an example for how to do non-trivial work under each binder style. Write a final section using Bound and you could write a new post comparing the whole farm of variable binding techniques.
I would love to see such a post!
Fwiw, it is non-trivial in Bound to do type-checking with contexts and working under binders. Larry Diehl has learnt some techniques for doing so in the course of using it in Spire, but it is extremely difficult.
Ah, I forgot about that. Ed once pointed me at Initial Algebra Semantics is Enough! as having tricks to get around that, but I never get my head around how that might work.
I should do this.. Mostly because I don’t think I’m smart enough to scale the current scheme to what I want to do :)