3 ms·
What would be the dependent type you could use to prevent the bug in the given example though? There is nothing wrong with the function itself, there is just a
by WJW 6y ago
What would be the dependent type you could use to prevent the bug in the given example though? There is nothing wrong with the function itself, there is just a discrepancy between what it does and how it is named. I don't know of any constraint that would fix that.
In any case, the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
- AnthonBerg 6y agoIn dependent types, types depend on values. Here, the type depends on the value that is the function name :) As far as I know, this is literally actually possible in Idris, right now. Wrote a bit more earlier: https://news.ycombinator.com/item?id=24716477 https://news.ycombinator.com/item?id=24716477 > the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it. Unbounded infinity has infinite, uncountable bugs. A defined, bounded, well-constructed, proven type system has fewer bugs. Dependent types are not an axis of explosion, but rather a way to express useful bounds on multiple axes.
- WJW 6y agoReading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (at least until AGI is a thing). There are plenty of function names that represent highly specific business processes (and jargon) and I don't see how any type system will have enough context for that. Less bugs does sound good, but after a minute thought there still seem to be uncountably infinite bugs even in the presence of dependent types. Just a few less than without. :)
- AnthonBerg 6y agoWe have a lllooootttt of work ahead of us! heh! (But yes: It's a good place to hook the AGI up!)