[fooker]

This is not a fixable flaw. Solving these constraints efficiently can definitely get you a Turing award, it's basically the SAT problem.

And without this type system, swift is just Objective C in a prettier syntax, so Apple has to bite the bullet and bear with it.

[coldpie]

It sort of is fixable, though. If you think about it, the problem is a bunch of functions are all mapped to one of a small set of names: +*/, etc. That is, the operators. If we didn't try to cram all this functionality into a tiny handful of symbols because of some weak analogy they have with basic math operations[1], then the compiler would have far fewer name conflicts to try to disambiguate, and the problem goes away on its own. Like yeah, the problem still exists if we made a few dozen functions all called "a", but the solution is to not do that, not give up on an otherwise fine type system.

I'm convinced operator overloading is an anti-feature. It serves two purposes:

1) to make a small set of math operations easier to read (not write), in the case where there are no mistakes and all readers perfectly understand the role of each operator; and,

2) to make library developers feel clever.

Operator-named functions are strictly worse than properly named functions for all other uses. Yes, yes, person reading this comment, I know you like them because they make you feel smart when you write them, and you're going to reply with that one time in university that you really needed to solve a linear algebra problem in C++ for some reason. But they really are terrible for everyone who has to use that code after you. They're just badly named functions, they're un-searchable, they make error messages unreadable, and they are the cause the naming conflict that is at the root of the linked blog post. It's time to ditch operator overloading.

[1] Or because they look like the same symbol used in some entirely other context, god, please strike down everyone who has ever written an operator-/ to combine filesystem paths.

[fooker]

It's more about potential protocol conformance than overloading.

If you discard that, we are back to Objective C.

[Apocryphon]

So you’re saying one potential solution is to use the APL character set?

[shagie]

> ... it's basically the SAT problem.

I am reminded of this classic CodeGolf.SE challenge of "P = NP" https://codegolf.stackexchange.com/a/24419

The problem was set as:

> Your task is to write a program for SAT that executes in polynomial time, but may not solve all cases.

To which Eric Lippert wrote:

> "Appears" is unnecessary. I can write a program that really does execute in polynomial time to solve SAT problems. This is quite straightforward in fact.

And has a spoiler that starts out as:

> You said polynomial runtime. You said nothing about polynomial compile time. This program forces the C# compiler to try all possible type combinations for x1, x2 and x3, and choose the unique one that exhibits no type errors. The compiler does all the work, so the runtime doesn't have to. ...

Unfortunately the blog post which it was linked to that went into greater detail at https://devblogs.microsoft.com/ericlippert/lambda-expression... is no longer available (even via wayback).

[fweimer]

I know that historically, we were taught that NP-complete problems are unsolvable for interesting problem sizes, but that was already a bit of lie in when I went to university. (TSP was presented as a warning example, but even back then, very efficient approximations existed.)

These days, when you have a SAT-like problem, you're often done because you can throw a SAT solver at it, and it will give you an answer in a reasonable time. Particularly for such small problems like this one here. We routinely solve much larger and less structured SAT instances, e.g. when running package managers.

[EdiX]

> These days, when you have a SAT-like problem, you're often done because you can throw a SAT solver at it, and it will give you an answer in a reasonable time

I don't know. All my experiences with SAT solvers have been bad. Sometimes adding constraints (and making the problem overconstrained) makes them orders of magnitude faster, sometimes it makes them orders of magnitude slower. Same goes for changing variables from integer to real or vice versa. And it varies from SAT solver to SAT solver, even on the same problem. I know enough about SAT solvers to know why this might happen but they're complete black boxes (as far as I can tell) and I can't predict their performance at all nor can I predict if a change I attempt will make them behave better or worse. I can't even tell if the bad performance is my fault or just the problem being legitimately to hard. And when it works I'm never sure if it will always work or if there are some inputs we have that will slip through the cracks of the heuristics it's using and hit us with a running time measured in days. If I could never use a SAT solver ever again I wouldn't.

[fooker]

I know, my PhD was about verifying software correctness with SMT solvers.

The reason we don't do this in production is that the solvers take an unpredictable amount of time. A small problem can take forever and a large problem can be instant. You can't gave that in a compiler.

There are enough people at Apple who know about SAT solvers. :)

[agent281]

On the other hand, they might know about SAT solvers, but not have enough time to actually experiment with it and integrate one into the language. Especially if there are other high priority issues.

[cerved]

depends what you consider interesting and/or acceptable solution I suppose

[Dylan16807]

Both your points can be addressed by: It's not a choice between infer everything and infer nothing.

[fooker]

It's worse that infer everything.

It's infer everything and make sure there's only one possible interpretation, with certain exceptions.