Davi Sales Barreira (Mar 02 2024 at 23:23): Davi Sales Barreira (Mar 02 2024 at 23:23):When I search for "dependent types Julia", I see discussions where it is said that Julia does not have dependent types. Yet, I saw a recent presentation that said that Julia was dependently typed, and gave the example:
StatictVector{Float64,n}
Which indeed does seem like dependent types... So what is the correct answer here?
Mason Protter (Mar 02 2024 at 23:35):Depends on the definition you’re using
Mason Protter (Mar 02 2024 at 23:35):by most people’s definitions though, no Julia is not dependently typed
Mason Protter (Mar 02 2024 at 23:36):But sometimes people say “dependantly typed” to mean “you can have values in type parameters”, in which case the answer is yes.
jar (Mar 02 2024 at 23:53):I think the PL people in that unfortunate thread are mostly arguing that Julia isn't "typed" at all, by which they mean statically typed.
Davi Sales Barreira (Mar 03 2024 at 00:15):I don't quite understand dependent typing, but I guess this idea of having values as parameters is what the person in the presentation was referring to.
Sukera (Mar 03 2024 at 07:05):IMO the thing that's missing for Julia to have "proper" dependent typing is being able to say StaticVector{Float64, 1 <= n <= 3} and have that mean something in subtyping. I.e., StaticVector{Float64, 3} would be a subtype of that, but StaticVector{Float64, 15} would not. It's not in general impossible to add that, but anyone who wants to do that must be able to answer questions like "what if the constraint you want to put there can throw an error? Can it do IO? Is there an upper limit on computation time the query is allowed to take?" because all of that runs in the compiler/type inference, and crashing/stalling the compiler is a big no-no (artificial testcases that don't indicate an underlying issue aside).
Last updated: Nov 06 2024 at 04:40 UTC