3 ms·

I think the Julia people were right to remove "dependent" from the docs. Nowadays I say that Julia has a limited form of static dependent typing, which is to sa

by wbhart 11y ago

I think the Julia people were right to remove "dependent" from the docs. Nowadays I say that Julia has a limited form of static dependent typing, which is to say it doesn't have dependent typing. When we first wrote Nemo in Julia, we used a form of emulated dependent typing. But the way we did this led to performance problems that we just hadn't thought about. For example, if we did lots of operations over Z/pZ for many primes p, e.g. in multimodular algorithms, it meant that the Jit compiler had to recompile everything for every prime p, which was awfully slow. Julia is absolutely not meant to be used that way, and it took us a long time to see that. After redesigning Nemo to use Julia much more like the way it was designed to be used, we actually ended up speeding everything up.

nickpsecurity 11y ago
So, to be clear, you had to avoid using dependent type style in Julia and use something very different? And that different thing wasn't another style of dependent types? Am I interpreting it correctly? Reason being that the only emulation of dependent types in Julia being way to slow would be an extra argument against any claims for Julia having dependent types vs real, dependently-typed languages that don't punish you for using them. I'd rather be clear before going that far, though.
- wbhart 11y ago
  Avoiding dependent types wasn't due to a problem in Julia. Proper dependent types are essentially not something you want to mix with Jit compilation due to undecidability, at least not if you want to use bignums in your dependent values. Of course you could emulate them some other way in Julia, but they are deliberately not baked into the language. In the end we used the model that some computer algebra systems, like Sage and Magma use, of having parent objects for the rings in which the element objects live. I'll leave it up to the experts to figure out if this is dependent typing or not. It obviously works very well either way.
  - nickpsecurity 11y ago
    Makes sense. Appreciate the clarification.

by wbhart 11y ago

nickpsecurity 11y ago

So, to be clear, you had to avoid using dependent type style in Julia and use something very different? And that different thing wasn't another style of dependent types? Am I interpreting it correctly? Reason being that the only emulation of dependent types in Julia being way to slow would be an extra argument against any claims for Julia having dependent types vs real, dependently-typed languages that don't punish you for using them. I'd rather be clear before going that far, though.

wbhart 11y ago
Avoiding dependent types wasn't due to a problem in Julia. Proper dependent types are essentially not something you want to mix with Jit compilation due to undecidability, at least not if you want to use bignums in your dependent values. Of course you could emulate them some other way in Julia, but they are deliberately not baked into the language. In the end we used the model that some computer algebra systems, like Sage and Magma use, of having parent objects for the rings in which the element objects live. I'll leave it up to the experts to figure out if this is dependent typing or not. It obviously works very well either way.
- nickpsecurity 11y ago
  Makes sense. Appreciate the clarification.