4 ms·
Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically th
by dllthomas 11y ago
Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!
- rfw 11y agoReally? 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