[mnarayan01]

The article could probably do with at least some discussion of https://www.python.org/dev/peps/pep-0484/.

Also:

> Our optional type system was designed from the perspective that a single language can consistently contain the semantics of both a dynamically-typed and a statically-typed language.

The obvious meaning of the word "consistently" here would preclude Turing-complete languages from this (recognition of the same language + undecidability), unless you adopt a fairly idiosyncratic definition of "type safe". I haven't read the whole thing, but it seems like there's a lot of dancing around this without actually coming out and saying it. For me, at least, headlining what you're not claiming would make this substantially more readable.

Edit: Okay, read some more and the "Parametric Types and Stanza's Captured Type System" and "Implications for Safety" sections "dance closer", but it feels like the implications need to be pulled out and moved way up. The covariance assumption in particular...let's just say that I was expecting something substantially different by the time I got to that point.

Finally, if you want some nit-picky editing advice: The terms "Thus" and (to a lesser extent) "Hence" are used...frequently. Possibly just me, but I found it fairly jarring.

[tom_mellior]

> preclude Turing-complete languages from this (recognition of the same language + undecidability)

Can you explain what you mean here? What is the undecidability result you are referring to?

I kind of have the feeling you are trying to make a point about formal languages being "the same", whereas the article uses "the same language" to mean "a single programming language" that allows, but does not require, type declarations.

That such a language can exist should not be a point of contention. You yourself pointed to the PEP that defines such a language.

[mnarayan01]

> What is the undecidability result you are referring to?

Just the correspondence between static type safety and the halting problem.

> I kind of have the feeling you are trying to make a point about formal languages being "the same", whereas the article uses "the same language" to mean "a single programming language" that allows, but does not require, type declarations.

Yes this. To me, it felt like the article was making the "stronger" claim, at least until the end when it starts talking about co/contra-variance.

[tom_mellior]

> Just the correspondence between static type safety and the halting problem.

I'm not sure if you are saying that there cannot be programming languages with decidable static type systems. Because there are programming languages with decidable static type systems. Typically you cannot encode Turing machines in the type system, so you don't get the kind of problem you seem to be talking about. (But you haven't really explained what you are talking about.)

[mnarayan01]

  // ... Well typed things ...
  if (arbitrary_well_typed_function()) {
    v = 0xF00 + "bar"
  }
  // ... Well typed things ...

Let's say this program is well typed iff `arbitrary_well_typed_function()` is falsy. If a static type checker can not compute `arbitrary_well_typed_function`, it needs to make a trade-off which a dynamic type checker need not.

[tom_mellior]

OK. Yes, static type systems need to make trade-offs. If this was your entire point, your original talk about undecidability was hiding it well.

[mnarayan01]

You got my point in your first comment in this thread. Unless that comment was the result of hours of striving, it doesn't seem as if the point was hidden well. If you did spend hours working at it, then I apologize and commend you on your success.