4 ms·
Aren't dependent types undecidable?
by throwaway613834 9y ago
Aren't dependent types undecidable?
- yeahbutbut 9y agoMaybe.
- throwaway613834 9y agoWhat do you mean by "maybe"? [1] https://cs.stackexchange.com/questions/12691 https://cs.stackexchange.com/questions/12691
- yeahbutbut 9y agoI was trying to be punny by implying indecision... edit: also thanks for the link :)
- throwaway613834 9y agoOhh wow that went over my head haha.
- tomp 9y agointegers with additions are decidable - that's pretty much what you need to verify array bounds (multiplication with a constant is included as well, so matrices should work too).
- throwaway613834 9y agoDo you mean "in practice" that's what you need? I could buy that, but I'm thinking about it in terms of the language spec. What would it say? Are we moving toward a language spec that says the meaning is "whatever the reference compiler can handle"? Or do you mean one that says "array indices may only be (constant) linear combinations of variables in order for the code to be compilable" or something like that?
- tomp 9y agoGood point. The way I imagined is, the language is defined as "safe", and has both "static" and "dynamic" guarantees. Whatever the compiler is able to prove statically, amazing, or else it adds dynamic checks. The programmer can optionally tag the function/expression so that the compiler will warn if it can't prove it. Long-term, I think it's very reasonable to assume the solvers will improve, so best to design a language with this in mind.
- bjz_ 9y agoNo, not if your language has totality checking like Idris, Agda, Lean, etc. Granted, it can sometimes be finicky to prove totality - the type checker naturally has to be a little conservative due to the impossibility of solving the halting problem, but for most things with array bounds checking it shouldn't be an issue.