Hacker News Reader

Comment by TylerE | Hacker News Reader

a sufficiently advanced new solver. Just like how the lisp guys insisted for decades that a sufficiently advanced compiler would solve all their performance woes. Right up until it became obvious that it couldn't.

Feels a bit like early chess engines. They tried to create super sophisticated heuristics to determine move quality, but then one person (or more probably multiple people independently more or less simultaneously) realized it's both easier and better to just do more or less the simplest thing that can possibly work, but do it as much as possible in the allotted time.

In other words - don't try to logically decide on the best move with some super advanced set of rules. Just assign a fairly basic and straightforward score based on calculating every reasonble move out 15, 20, 30 moves deep.

View on HN

This is beside the point, but the only way an engine can possibly search to depth 20 is by being extremely selective, using heuristics to guess move quality (such as static exchange analysis, the killer move heuristic, history tables, countermove tables, follow-up tables, late move reductions, &c). The discovery was that it's often better to guess move quality dynamically, based on the observed utility of similar moves in similar contexts, rather than statically. But this is not especially "simple", and it still (necessarily!) involves judging up front a few moves as likely-good and the vast majority of moves as unworthy of further examination.

Both type A engines (to use Shannon's terminology) and type B engines are relatively weak. The strong engines are all hybrids.

In the case of the trait solver, there is a clear end goal to reach: "the type system should be sound." This is a yes/no question, which you can prove/disprove mathematically.

(I suppose chess engines also have an end goal of perfect play, but that is a much harder problem)

There's a very simple solver that completes that goal: one that reports that it cannot prove any code as correct. So there must be a secondary goal of "maximize the amount of accepted code", which is a significantly less trivial question.

Yes, exactly.

Saying "just do the thing correctly, duh!" is easy. Ya know the saying about the difference between theory and practice?

I guess you have to add an implied "and preserves backward compatibility for (>99.9% of) sound code that compiles today" condition

A sound type system has strong limits on expressiveness, and even stronger if you want type inference to work. It's very easy to start tripping over those limits as you add features, as users of some Haskell extensions can attest.

Reply on news.ycombinator.com