7 ms·
Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?
by rfw 11y ago
Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?
- pzone 11y agoIt should be able to use a Hindley-Milner algorithm.
- dllthomas 11y agoAs I understand it, type inference breaks down on dependent types.
- dllthomas 11y agoI'm not sure the exact approach, but there's definitely some heavy lifting. My understanding is that most (all?) dependently typed languages are essentially theorem provers at heart.
- chenglou 11y agoSee my answer here: https://news.ycombinator.com/item?id=10856736 https://news.ycombinator.com/item?id=10856736