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?
Depends on the definition you’re using
by most people’s definitions though, no Julia is not dependently typed
But sometimes people say “dependantly typed” to mean “you can have values in type parameters”, in which case the answer is yes.
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.
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.
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 22 2024 at 04:41 UTC