4 ms·
You do not even need to use dependent types. You could just restrict yourself to polymorphic types if you wanted to. And you could use dependent types just for
by LightMachine 9y ago
You do not even need to use dependent types. You could just restrict yourself to polymorphic types if you wanted to. And you could use dependent types just for the things that don't require any "proving" work. Returning multiple types from a function, implementing type-safe `printf`, checking out-of-bound errors at compile time, things like that.
Dependent types allow you to express things such as `a == b` as a type, and proving that requires some work, but you don't need any of that at all. Idris is a superset of Haskell, you may say.
- seanwilson 9y ago> checking out-of-bound errors at compile time Even that quickly becomes undecidable as non-linear arithmetic is undecidable.
- munin 9y agoProponents of this approach would probably argue that non-linear arithmetic doesn't show up frequently in index computation. I don't know whether this is true or not, would be curious to see data. Based on my own experience I'd agree with it, with caveats for things like a[i%a.length] but you could probably do something there like replace % with an approximation that is linear and sound.
- seanwilson 9y agoEven if it was infrequent (I'd be interested in data too!), what do you do when it does come up? It's very difficult to constrain yourself to decidable domains when you want to write arbitrary programs and capture arbitrary program properties. You could let the proof goal go through without a proof but you'd have to replace it with a runtime check otherwise if the goal happened to be false all your static guarantees are out of the window (like doing a bad type cast in C++ for instance).