Is there a correspondence between the syntaxes and the type systems of programming languages?

Question

I was reading the first chapter of Robert Harper's Practical Foundations for Programming Languages in which it introduced abstract binding trees, aka abt. It seems pretty like typed lambda calculus.

1. There are ground sorts, which are similar to ground types in typed lambda calculus.
2. There are abstractions; they accept multiple arguments. They remind me of uncurried version of lambdas. It's a bit odd that abstractions at the syntax level aren't first-class, though.
3. Later at the end of the chapter in the book, symbols are introduced. They seem to correspond to data types. (Or do they?)
4. Indexed operators are $\Lambda$ bounded terms in the sense of system F.

The author of the book seemed to be aware of the similarities. The set of symbols is even written $\mathcal{U}$ in the book!

What I'm asking is, is there known to be a correspondence of abt's and type systems, or is it too good to be true? Are there more advanced systems of abt's that correspond to system Fω or dependent types?

The question is kind of too broad. Hopefully it can be accepted on this website.

Answer 1

You seem to have a misunderstanding of the purpose of abstract binding trees (ABTs). They are a tool for describing syntax, much like abstract syntax trees (ASTs). They simply allow you to describe syntax that includes binders in a way that generic tooling can be applied. Capture-avoiding substitution, for example, works basically the same way for first-order logic as it does for the untyped lambda calculus, so it would be nice to implement it once and then "instantiate" it to these particular languages. This is what ABTs accomplish.

Just like ASTs, ABTs have little to no semantics on their own, even when instantiated to a particular syntax. An ABT describing the syntax for the untyped lambda calculus is doing just that, describing syntax. Until you add the beta rule, it's not the lambda calculus. Similarly, if I make an ABT for the the syntax of the simply typed lambda calculus, the ABT won't stop me from making ill-typed nonsense. A type checker still needs to be implemented. Indeed, the exact same ABT could be used for very different type systems or semantics. For example, the difference between the linear lambda calculus and the typed lambda calculus is not a matter of syntax. Similarly, the difference between the call-by-value untyped lambda calculus and the call-by-name lambda calculus is entirely in when the beta rule can be applied, syntactically they are identical.