The Axiom [1] developers created a special purpose dependently typed language to capture mathematical abstractions: SPAD/Aldor [2]. Maxima uses Lisp. [3] These packages contain many man-years of work.
Julia is JIT-compiled, a Lisp (under the hood) and (somewhat) dependently typed.
Is that enough to port (or even transpile) modules from the big open source CAS without an entire rewrite? Is there enough similarity between CAS to make "foreign" modules even a remote possibility?
Otherwise, Nemo will likely not achieve a great unification of math packages, since the required effort goes way beyond the resources of a small dedicated group.
I mostly just follow articles on Julia for now. Aside from it having LISP-like macros, where's a page that says it's a LISP underneath? And I didn't see dependent types mentioned in the page below despite some things sounding similar. You got a link that straight up shows dependent types in Julia or how to emulate them?
Every expression is transformed internally to an AST representation that can be seen as a lisp-style s-expression. And this gets transformed, JIT-compiled, and so on. [1]
Furthermore, the Julia internals contain an entire lisp implementation (femtolisp [2]). That has influenced the metaprogramming capabilities.
And I didn't see dependent types mentioned in the page below despite some things sounding similar.
Integer matrices can be represented as Array{Int64,2}. So the type of the matrix depends on the Int64 datatype and the dimensionality 2. But that's not necessarily what type theorists understand to be a dependent type. There was an epic discussion that led to the phrasing "dependent" being removed from the Julia docs. [2]
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.
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.
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.
My own research was partly working to integrate LISP's and imperative programming. Seeing it already happen some way in Julia is totally awesome! I'll have more praise for it in the future I see. Ok, for dependent types, it doesn't have dependent types but one or more pieces of that capability? Maybe more once I've read the linked pages.
Thanks for the answer and links!
Edit: Just read the debate. I agree with 'tel' that the phrase dependent types has such a specific meaning, capabilities, and whole literature devoted to it that nobody should use it unless it's consistent. The Google search point was especially smart. Per that discussion, not my own analysis of Julia, Julia doesn't have dependent types & it's good they took that phrase off the site. Its different enough to justify a custom term to promote its usefulness while not misleading.
Comments
The Axiom [1] developers created a special purpose dependently typed language to capture mathematical abstractions: SPAD/Aldor [2]. Maxima uses Lisp. [3] These packages contain many man-years of work.
Julia is JIT-compiled, a Lisp (under the hood) and (somewhat) dependently typed.
Is that enough to port (or even transpile) modules from the big open source CAS without an entire rewrite? Is there enough similarity between CAS to make "foreign" modules even a remote possibility?
Otherwise, Nemo will likely not achieve a great unification of math packages, since the required effort goes way beyond the resources of a small dedicated group.
[1] http://www.axiom-developer.org/
[2] http://www.aldor.org/
[3] http://maxima.sourceforge.net/
I mostly just follow articles on Julia for now. Aside from it having LISP-like macros, where's a page that says it's a LISP underneath? And I didn't see dependent types mentioned in the page below despite some things sounding similar. You got a link that straight up shows dependent types in Julia or how to emulate them?
http://docs.julialang.org/en/release-0.3/manual/types/
Every expression is transformed internally to an AST representation that can be seen as a lisp-style s-expression. And this gets transformed, JIT-compiled, and so on. [1]
Furthermore, the Julia internals contain an entire lisp implementation (femtolisp [2]). That has influenced the metaprogramming capabilities.
Integer matrices can be represented as Array{Int64,2}. So the type of the matrix depends on the Int64 datatype and the dimensionality 2. But that's not necessarily what type theorists understand to be a dependent type. There was an epic discussion that led to the phrasing "dependent" being removed from the Julia docs. [2]
[1] http://julia.readthedocs.org/en/latest/manual/metaprogrammin...
[2] https://github.com/JuliaLang/julia/tree/master/src/flisp
[2] https://github.com/JuliaLang/julia/issues/6113
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.
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.
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.
Makes sense. Appreciate the clarification.
My own research was partly working to integrate LISP's and imperative programming. Seeing it already happen some way in Julia is totally awesome! I'll have more praise for it in the future I see. Ok, for dependent types, it doesn't have dependent types but one or more pieces of that capability? Maybe more once I've read the linked pages.
Thanks for the answer and links!
Edit: Just read the debate. I agree with 'tel' that the phrase dependent types has such a specific meaning, capabilities, and whole literature devoted to it that nobody should use it unless it's consistent. The Google search point was especially smart. Per that discussion, not my own analysis of Julia, Julia doesn't have dependent types & it's good they took that phrase off the site. Its different enough to justify a custom term to promote its usefulness while not misleading.