3 ms·
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
by Georgelemental 3y ago
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)
- dzaima 3y agoThere'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.
- TylerE 3y agoYes, exactly. Saying "just do the thing correctly, duh!" is easy. Ya know the saying about the difference between theory and practice?
- Georgelemental 3y agoI guess you have to add an implied "and preserves backward compatibility for (>99.9% of) sound code that compiles today" condition
- wbl 3y agoA 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.