Does Julia’s type checker show these problems too?
By the way, there is a document explaining the Swift’s type checker.
1 Like
good question, let’s try it
julia> @time try
address = "127.0.0.1"
username = "steve"
password = "1234"
channel = 11
url = (
"http://" * username
* ":" * password
* "@" * address
* "/api/" * channel
* "/picture"
)
print(url)
catch
end
0.000085 seconds (10 allocations: 392 bytes)
nope.
3 Likes
The specific example is not a problem (mostly because that example is typed very differently in Julia than it is in Swift), but there are absolutely cases where type inference is sluggish:
Regardless, this is an extremely niche/artificial scenario. This is to be expected - any type checker/inferencer has pathological cases.
1 Like
It’s far more interesting to think about why this works in Julia (where * has 214 methods) but breaks in Swift (where + has 17 overloads).
You can definitely get Julia into corners where type inference “gives up” — it happens all the time — but it can give up so much faster because it’s not catastrophic. A static AOT compiler needs to resolve every expression ahead of time. A dynamic language can happily work with Anys — and that’s just what Julia does when type inference gives up.
I’m not a Swift programmer, but I think a rough equivalent here is how Julia can infer types based on which methods exist. And right now, Julia gives up and doesn’t even try if there are more than just 4 methods. And increasing this number does grind Julia’s compile times (or TTFX) to a halt¹.
Fortunately, we don’t often need to divine out types from the method table; it frequently happens when you need to recover from a type instability, so just fix the type instability in the first place. And it’s really not a huge runtime issue… if you have a runtime, that is.
This all gets much more interesting with AOT-compiled Julia.
8 Likes
It’s not about being static AOT or not.
It is a largely Swift-specific problem.
In Julia, expressions don’t have types, but instances of objects do.
So,
address = "127.0.0.1"
username = "steve"
password = "1234"
channel = 11
url = (
"http://" * username
* ":" * password
* "@" * address
* "/api/" * channel
* "/picture"
)
in Julia, address, username, password, and channel all already have types, and those types can NOT be influenced by any expressions they appear in.
Thus, Julia specifically requires the method *(::String, ::String, ::String, ::String, ::String, ::String, ::String, ::Int, ::String).
Julia can then move along the type lattice to look for a match.
The situation is a little worse in C++ 20 (which introduced auto return types; auto function arguments came much earlier), because while each particular expression has a type, C++ has implicit conversions. Thus, in some situations, it needs to build up a set of reachable-via-implicit-conversion candidate types.
Of course, if you have a generic
auto string_join(auto x...){
}
then, just like Julia, it doesn’t need to do that. It only needs to consider a single match: substitute the actual types for the templated/auto types.
The situation in Swift, on the other hand, is bad. Its type inference is bidirectional. It isn’t only the definition that influences a type, but also the uses!
That is, the type of
address = "127.0.0.1"
isn’t only a function of the definition above, but also how you use it. Address could have different types in these two programs:
address = "127.0.0.1"
foo(address);
vs
address = "127.0.0.1"
bar(address);
depending on what foo and bar actually are.
What kills performance for swift is figuring out what the types of all the variables actually are. If the fast path fails, it apparently does this via an exponential time check of all possible type combinations of *.
I imagine they could do better, by having some concept of what types are reachable from a definition, rather than rejecting methods that are not reachable, but that is all far out of my wheel house.
I don’t know swift, let alone how things are implemented, or why they’re implemented the way they are. It’s probably difficult to avoid regressions, limiting their ability to change it now.
But, I think using a “bi-directional Hindley-Milner type checker” is a bad idea.
Mojo follows closer to the C++ approach, for example (but presumably without implicit conversions, which C++ people almost universally think is a bad idea/guides almost always recommend declaring your constructors and conversion operators explicit to opt out). Both Mojo and Swift were developed by Chris Lattner, Mojo coming later, strongly implying that its original developers agree the bi-directional type checker was a mistake.
16 Likes
FTR, this is currently configurable using Base.Experimental.@max_methods or Base.Experimental.@compiler_options (experimental, obviously).
1 Like
Is there a programming language that uses the bidirectional Hindley-Milner type checker without these issues?
It’s unlikely that it can be avoided, see note here:
Non-linear behaviour does manifest itself, yet mostly on pathological inputs.
1 Like
Julia’s subtyping is also non-linear and at least EXPTIME[1]. The interesting thing with complicated algorithms like these is how you can get fast-paths through the system — or perhaps more relevantly, how thoroughly you can avoid the slow paths.
2 Likes
OCaml, for example, has Hindley-Milner type inference but avoids these problems because it doesn’t have function overloading (or multiple dispatch).
4 Likes