[RFC007] Migrate the typechecker to the new AST - Part I

[yannham]

Migrate the typechecker to the new AST (Part I)

Content

After the parser, this PR undertakes the migration of the typechecker to operate on the new AST.

Actually swapping the typechecker isn't done as part of this PR, because this requires even more changes - in particular migrating the parts of NLS that handle the term visitor pattern, and keeping part of the mainline contract equality checking code because it's still used at runtime for contract deduplication.

In the meantime, this PR duplicates the whole typechecker under bytecode::typecheck temporarily, so that we can iterate there.

How to review

Most of those changes are pretty mechanic: we switched type signatures to use components from bytecode::ast::* instead of term::*, and then fixed the myriad of compiler errors. Because we duplicated the code, it's not easy to see the difference with the original version either; but most of the changes should really be boring.

Some parts that might be worth looking at:

• all the Traverse mechanic has been moved to a new dedicated top-level module traverse (it was previously defined in term). As for combine::Combine, we added a second version of the trait for arena-allocated values: TraverseAlloc, and implemented it for all the new AST subcomponents.
• typechecking records as defined in the new AST is not trivial, because all we have now is a list of path-defined fields, that might overlap in different ways. The machinery to handle record is now implemented in bytecode::typecheck::record. Most of it is a clean implementation of what we did in the parser before RFC007: transform a list of path-defined fields to nested maps. The typechecking part of bytecode::typecheck::record has been mostly taken from typecheck, and hasn't been substantially modified.
• While I tried to keep this PR focused on doing the minimal changes so that the repo compiles again, saving more substantial refactoring/cleaning for later, it was just too tempting for typecheck::eq, which was previously complicated by the fact that it needs to handle both typechecking-time and run-time contract equality check. the new bytecode::typecheck::eq has been re-organized around traits instead of free-standing functions, plus other simplifications coming from the fact that runtime contract equality will have to be done entirely differently in the bytecode VM, so we can afford to be less generic here.

All in all, I believe that we'll have a net reduction of LoC once we scrap the original typechecker, because many edge cases just don't happen with the new, simpler AST.

[github-actions]

Bencher Report

Branch	rfc007/typechecking
Testbed	ubuntu-latest

Click to view all benchmark results

Benchmark	Latency	nanoseconds (ns)
fibonacci 10	📈 view plot 🚷 view threshold	488,230.00
foldl arrays 50	📈 view plot 🚷 view threshold	1,714,100.00
foldl arrays 500	📈 view plot 🚷 view threshold	6,764,600.00
foldr strings 50	📈 view plot 🚷 view threshold	6,987,500.00
foldr strings 500	📈 view plot 🚷 view threshold	60,716,000.00
generate normal 250	📈 view plot 🚷 view threshold	43,753,000.00
generate normal 50	📈 view plot 🚷 view threshold	1,943,700.00
generate normal unchecked 1000	📈 view plot 🚷 view threshold	3,244,200.00
generate normal unchecked 200	📈 view plot 🚷 view threshold	762,190.00
pidigits 100	📈 view plot 🚷 view threshold	3,167,500.00
pipe normal 20	📈 view plot 🚷 view threshold	1,501,600.00
pipe normal 200	📈 view plot 🚷 view threshold	9,967,800.00
product 30	📈 view plot 🚷 view threshold	851,120.00
scalar 10	📈 view plot 🚷 view threshold	1,544,300.00
sum 30	📈 view plot 🚷 view threshold	834,570.00

🐰 View full continuous benchmarking report in Bencher

[jneem]

That's a lot of changes! I left a comment mostly just to show that I read something 😉

Seriously, though, I read the parts you mentioned in the description, and skimmed the rest.

[jneem]

Maybe it's not important in this context, but in principle there are multiple locations for each field, right? It looks like ResolvedRecord::combine is just choosing one. (The LSP certainly wants them all, but I guess it isn't using this resolution anyway...)

[yannham]

Indeed. For now I'm just maintaining the old behavior, which was to use TermPos::None as soon as the parser had to merge multiple definitions either statically or dynamically, precisely because the RichTerm interface requires that you provide at most one position, which isn't possible. If you look at ResolvedField::pos,it uses a XOR so that we return a defined position iff there is only one position defined; if there is none or there are multiple ones, we bail out and return None.

We can certainly do better in the future, I suppose. Although having a multi-pieces definitions in a statically typed block is currently un-ergonomic enough (since we can't type merging correctly, everything has to be of type Dyn) that I don't expect it to happen much. Still, I expect to re-use the record resolution part for compilation, where you might want all the positions. And one day we might type & more precisely as well.