Baby's First Type Checker

Foundational tooling not being written in a compiled language (fast is good, it could be jitted, but ideally it's a single binary) is actually a huge tax that I'm quite glad we're getting over as an industry.

Python is probably the apex of the "slow + doesn't work without a magic environment" problem

I suppose it is how this kind of tool generally works. I think it's just some subset of the feeling I get when someone writes(implements?) $LANGUAGE in $LANGUAGE(e.g. brainf*ck in brainf*ck)

EDIT: escaped censorship

Everyone always says that, but I don't think it's a good intro :-) (e.g. I think the top comment in the lobste.rs thread is suffering from the type inference / functional bias, which is not necessarily due to TAPL, but it's a common thing I've noticed)

Right now I think Siek's book is better for what I want to do, though admittedly I didn't get that far into it, because my type checking project is way on the back burner

I would like to see any type checkers that people wrote after reading TAPL!

TaPL really falls down when trying to bootstrap your way to understanding the notation. A lot of the notation and theory revolves around, essentially, implementing a concurrent virtual machine. I like the original algorithm W paper because it doesn't gloss this conceptual step: it is very much a virtual machine & you can see the authors handling the edge cases. The operational semantics in TaPL are (frankly) obtuse. Also, TaPL makes it seem like new features can be desugared to old features — and they can — but a little more prose explaining the feature's behavior directly without just tossing you into the semantic deep end would've made a much nicer text.

No it's not pleasant at all. It's boilerplate heavy, non-local and indirect. It's presumably a large part of why pattern matching is arriving in Python.

Doing it this way maxes coupling and minimises cohesion.

Your language will have a number of phases/passes to carry out. Let's say LambdaLifting, TypeChecking and Inlining.

All the code for lambda lifting belongs in one module, all the code for type-checking in another module, etc.

If you instead use visitor pattern, you will be looking at all the code related to Variable, Function, Literal in those files respectively.

So when you're working on Function.typecheck(), it will sit in source code just under Function.lambdalift() and just above Function.inline() - things which you don't want to consider together. Meanwhile, you'll need to switch between source files to work on Variable.typecheck() and Literal.typecheck().

  TypeChecker
    visitFunction
    visitVariable
    visitLiteral
  PrettyPrinter
    visitFunction
    visitVariable
    visitLiteral

That's not the only difference - the other issue is that you lose the stack, and must rely on member variables instead.

If you search for pop(), you can see that

    self.expected_ret.append(ret)
    self.generic_visit(n)
    self.expected_ret.pop()

and

    self.push(narrows_true);  [self.visit(s) for s in n.body];  self.pop()
    self.push(narrows_false); [self.visit(s) for s in n.orelse]; self.pop()

In the functional style, you just pass a param using the stack, rather than using an explicit stack.

It's not so bad here, but with a big enough language, and more complicated algorithms, the mutable member variables basically become "mutable globals".

And if you re-call visit() at arbitrary depths, IMO the algorithm gets obscured.

---

That said, I agreed here that visitors are useful when you need to say traverse all string literals in an AST, at arbitrary depths: https://lobste.rs/s/jdgjjt/visitor_pattern_considered_pointl...

---

A sign that this issue isn't settled is that two of the more complex type checkers make opposite decisions

- MyPy uses visitors extensively - https://github.com/python/mypy/tree/master/mypy

- TypeScript mostly uses switch/case functions - https://github.com/microsoft/TypeScript/blob/main/src/compil...

I'd be interested in analysis of why that is, but I suspect it's mainly style