1. 7
  1. 4

    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:

    1. 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.

    2. I experimented with really nice error tracing for type errors (judgement refutations).

    3. 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.

    4. I also have a cumulative, predicative hierarchy of universes, as well as an intensional identity type.

    5. 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.

    1. 1

      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!

      1. 1

        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.

        1. 1

          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.

          1. 2

            I would love to see such a post!

            1. 2

              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.

              1. 2

                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.

              2. 2

                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 :)