5 ms·

> doesn't matter which language you use Idris.

by Manishearth 10y ago

lossolo 10y ago
Care to elaborate? I don't see how this can be done without trading space/time over solution without bound checking.
- Manishearth 10y ago
  It won't work in all cases :) IIRC Idris will move type info to runtime if it can't prove it at compile time. Basically, in Idris I can have a function concat which takes a Vector<N, T>, a Vector<M,T>, and produces a Vector<N+M, T>. You can have arbitrary expressions there, and even things like a function which returns a different type based on its boolean argument. So most signatures will just carry dependencies through, but some things are dependent on runtime input and that's when the "N" part of the type will be tracked at runtime. At least, that's how I think it works. Dependent types help eliminate large swaths of bounds checks. Not all of them, and I'm not sure how much better it does than a good optimizing compiler.
  - lossolo 10y ago
    > I'm not sure how much better it does than a good optimizing compiler. It can be done by static analysis by compilers in other languages also. Knowing size at compile time is easy most of the time and we are not talking at all about this case. Your answer that Idris solves that is wrong in the context that this discussion started (dynamically allocated memory/not knowing the size compile time). You still need to trade time/space comparing to solution without bound checking, doesn't matter which language you use. I am getting info that I am submitting too fast? so answer to your other comment will need to wait.
    - Manishearth 10y ago
      Yes, it can be done by static analysis, but by making size dependencies part of the API it makes the static analysis much easier and able to cross API boundaries without needing to inline, on the contrary most optimizers will not handle such invariants across a few layers of function calls. Like I said, Idris doesn't solve this problem completely, but it is able to eliminate bounds checks in way more situations because the default is effectively no bounds checking. The nice thing about dependent types is that in all the cases where you don't need a bounds check -- where a program invariant enforces that you are within bounds -- your code will not contain a bounds check regardless of optimization. Only in the cases where there are runtime dependencies that can't be resolved will there be issues, and in thee cases you need a bounds check anyway. It's not perfect/complete, and like I said optimizers can get most of the way there anyway. I just wanted to note that there are better solutions for bounds checking.

> doesn't matter which language you use Idris.

lossolo 10y ago

Care to elaborate? I don't see how this can be done without trading space/time over solution without bound checking.

Manishearth 10y ago
It won't work in all cases :) IIRC Idris will move type info to runtime if it can't prove it at compile time. Basically, in Idris I can have a function concat which takes a Vector<N, T>, a Vector<M,T>, and produces a Vector<N+M, T>. You can have arbitrary expressions there, and even things like a function which returns a different type based on its boolean argument. So most signatures will just carry dependencies through, but some things are dependent on runtime input and that's when the "N" part of the type will be tracked at runtime. At least, that's how I think it works. Dependent types help eliminate large swaths of bounds checks. Not all of them, and I'm not sure how much better it does than a good optimizing compiler.
- lossolo 10y ago
  > I'm not sure how much better it does than a good optimizing compiler. It can be done by static analysis by compilers in other languages also. Knowing size at compile time is easy most of the time and we are not talking at all about this case. Your answer that Idris solves that is wrong in the context that this discussion started (dynamically allocated memory/not knowing the size compile time). You still need to trade time/space comparing to solution without bound checking, doesn't matter which language you use. I am getting info that I am submitting too fast? so answer to your other comment will need to wait.
  - Manishearth 10y ago
    Yes, it can be done by static analysis, but by making size dependencies part of the API it makes the static analysis much easier and able to cross API boundaries without needing to inline, on the contrary most optimizers will not handle such invariants across a few layers of function calls. Like I said, Idris doesn't solve this problem completely, but it is able to eliminate bounds checks in way more situations because the default is effectively no bounds checking. The nice thing about dependent types is that in all the cases where you don't need a bounds check -- where a program invariant enforces that you are within bounds -- your code will not contain a bounds check regardless of optimization. Only in the cases where there are runtime dependencies that can't be resolved will there be issues, and in thee cases you need a bounds check anyway. It's not perfect/complete, and like I said optimizers can get most of the way there anyway. I just wanted to note that there are better solutions for bounds checking.