[withoutboats3]

I'm suspicious about the truth of this claim. I don't think bidirectional typechecking is the problem in itself: the problem trying to do type inference when you have some extremely flexible operator overloading, subtyping, and literal syntax features. It's these "expressive" features which have made type inference in Swift far more computationally complex, not type inference itself.

And certainly not bidirectional type inference; the author of this post's definition of this concept isn't even right (bidirectional typing refers to having a distinction between typing judgements which are used to infer types and those which are used to restrict types, not moving bidirectionally between parent nodes & child nodes). I don't know if the mistake comes from the post author or Chris Lattner, and I don't know if the word "bidirectional" is relevant to Swift's typing; I don't know if Swift has a formal description of its type system or that formal description is bidirectional or not.

EDIT: watching the video the Chris Lattner quote comes from, it appears the mistake about the word "bidirectional" is his. Bidirectional type systems are an improvement over ordinary type systems in exactly the direction he desires: they distinguish which direction typing judgements can be used (to infer or check types), whereas normal formal descriptions of type systems don't make this distinction, causing the problems he describes. "Bottom up" type checking is just a specific pattern of bidirectional type checking.

Regardless, the problem with Swift is that a literal can have any of an unbound arity of types which implement a certain protocol, all of which have supertypes and subtypes, and the set of possibilities grows combinatorially because of these language features.

cf: https://arxiv.org/abs/1908.05839

[foobar99]

Bidirectional type checking is what makes Swift type checking exponential. Operators and literals just really jack up the numbers in the exponential function because they quickly lead to deeply nested expression trees with many choices on each nesting. So that's why they're the most commonly cited examples. They look very innocent and simple but aren't in Swift.

But you can absolutely construct slow expressions just with functions that are overloaded on both sides (i.e. parameters and return type). Generics and Closures also drive up the complexity a lot, though.

[floxy]

I found an online Swift Playground, and here is a smaller test case that produces the "unable to type-check this expression in reasonable time" message:

  print("a" + "b" + "c" + 11 + "d")

...if you reduce it even further to:

  print("a" + "b" + "c" + 11)

...the error message is:

  <stdin>:3:23: error: binary operator '+' cannot be applied to operands of type 'String' and 'Int'
  print("a" + "b" + "c" + 11)
        ~~~~~~~~~~~~~~~ ^ ~~
  <stdin>:3:23: note: overloads for '+' exist with these partially matching parameter lists: (Int, Int), (String, String)

...it still falls down on with the "reasonable time" error on this tiny example, even if you fully specify the types:

  let a:String = "a"
  let b:String = "b"
  let c:String = "c"
  let d:String = "d"
  let e:String = "e"
  let n:Int = 11
  
  print(a + b + c + n + d + e)

...is that pointing to a problem with type-checking or overload resolution more than type inference? Is there a way in Swift to annotate the types of sub-expressions in-line, so you could try something like:

  print((a + b + c):String + n + d + e)

[amomchilov]

The slow-down here isn't just from picking the correct `+` overloads, but also the various types that `"a"` could be (e.g. `String`, `Substring`, `Character`, or something like a `SQLQuery` type, depending on what libraries you have imported)

[amomchilov]

`print((a + b + c) as String + n + d + e)`

(I’m not sure of the precedence, that might need another pair of parens)

[floxy]

Interesting. This:

  let a:String = "a" as String
  let b:String = "b" as String
  let c:String = "c" as String
  let d:String = "d" as String
  let e:String = "e" as String
  let n:Int = 11 as Int
  
  print((a + b + c) + n + d + e)

...has the long timeout, while:

  let a:String = "a" as String
  let b:String = "b" as String
  let c:String = "c" as String
  let d:String = "d" as String
  let e:String = "e" as String
  let n:Int = 11 as Int
  
  print((a + b + c) as String + n + d + e)

...fails pretty much instantaneously.

[pcwalton]

Yeah, I agree. Regular H-M typechecking if you don't have subtyping is actually really fast. The problem is that subtyping makes it really complicated--in fact, IIRC, formally undecidable.

[Weebs]

Afaik that is true of traditional HM, but fortunately there was a big advancement in inferring subtypes w/ Dolan's Algebraic Subtyping a few years ago! It's not nearly as fast as HM (O(n^3) worst case) but generally fast enough in real code

[mmoskal]

It's funny because it's doubly exponential WRT code size. However it's also almost linear (n log*(n) due to union-find) WRT the size of the type and sane humans don't write programs with huge types.

[nextaccountic]

I don't know about Swift, but in Rust there are libraries like Diesel that essentially builds a new type out of the operations you run (in Diesel's case, it's used to type a SQL query), which may lead to huge types in ordinary code.

Programmers don't manually write those types however.

[lamontcg]

I'd trade type inference for expressibility (function and operator overloading in particular). But this seems to currently be a heretical opinion.

[Tuna-Fish]

Rust took the other road:

    error[E0277]: cannot add `i64` to `i32`
        1i32 + 2i64;
             ^ no implementation for `i32 + i64`

It bothered me at first, there are a lot of explicit annotations for conversions when dealing with mixed precision stuff. But I now feel that it was the exactly correct choice, and not just because it makes inference easier.

[lamontcg]

Rust still lets you create your own algorithmic data types so that you can overload traits like Add, Mul, Div and Sub to implement your own e.g. Vector3 class (although I still feel this is too restrictive, but understand why rust chooses not to do that). What Rust blocks in your example there is implicit type conversion/coercion/promotion, and I'm actually okay with that and forcing being much more explicit about type casting.

Go is the language that makes your vector classes required to have syntax like v1.VecMult(v2) and v1.ScalarMult(s) because there's no operator overloading at all (even though there's a largely useless baked-in complex number class).

[adamwk]

the rust traits are not overloading though (at least not in the same way as swift), that’s just implementing a trait on a type. I think the distinction is that with traits or protocols you get a lot of expressivity, reducing the need for overloading

[lamontcg]

You can still create your own vec3 though that implements "<vec3> * <double>" through the Trait... It seems at least superficially equivalent to operator overloading.

[fauigerzigerk]

It is operator overloading. Traits are just the mechanism to do operator overloading in Rust.

But I think what matters in this particular context is that Rust does not support function overloading and this restriction also applies to functions implementing operators. I think this may be why the parent comment claims that it is not really overloading. The meaning of "overloading" is a bit ambiguous here.

So for a concrete type vec3 you cannot define both <vec3> * <double> and <vec3> * <vec3>, which makes type inference a lot easier. It also makes Rust operator overloading less expressive.

[Someone]

Swift does that for integers, floats and doubles, too. https://docs.swift.org/swift-book/documentation/the-swift-pr...:

“Conversions between integer and floating-point numeric types must be made explicit:

  let three = 3
  let pointOneFourOneFiveNine = 0.14159
  let pi = Double(three) + pointOneFourOneFiveNine
  // pi equals 3.14159, and is inferred to be of type Double

“