[dragonwriter]

Dynamic and strong typing are not opposed (dynamic and static typing are opposed, and, to the extent the distinction is valid, weak and strong typing are opposed), dynamic doesn't mean everything is physically boxed (most dynamic language implementations don't box some subset of small primitive values, usually including bools and small ints), and, in any case, flow typing is a feature of static type systems (though some of those offering it are optional static typing systems for dynamic languages.)

But you kind of get at the real answer toward the end despite talking around it most of your post: Sum types plus pattern matching solves the same set of problems union types with flow typing solves, and a bunch that the latter doesn't (like composability.)

[jerf]

Remarkably, a post written in generalities speaks in generalities. None of those things may be "necessary", but there sure is a lot of all the things I said, aren't there?

What you call "speaking around" I call an important thing to understand about a lot of languages: At some point, your data will be physically laid out in memory. If you don't care about performance... and I mean that as a perfectly valid choice in many situations, not a snark... it doesn't much matter how it is. But if you do, and you selected a language based on that, it matters a lot, and you have to view every type system detail through the lens of "what does it look like in memory?" if you want to understand it. The choices this class of language makes for their type systems will never fully make sense if you are not paying attention to this, and also if you gloss over the legitimate difficulties that arise for any sort of "why don't they just...?" sorts of questions.

(In particular, you really don't understand how good Rust is until you look at it through this lens, then look at just how much simultaneous power and convenience they've drawn out while never compromising on the memory issues. It's an incredible piece of work. It probably isn't "optimal" because such things don't exist in our real universe, but it probably is as close as we'll ever see for that class of langauge.)

[dllthomas]

> dynamic and static typing are opposed

Any given typing judgement we might want to make about a particular term can be checked statically or not, and it can be checked dynamically or not.

If the language has terms (... that might be evaluated) that don't get checked statically or dynamically, then it is going to be weakly typed (with respect to those typing judgements we're considering).

If we've already checked something statically, we "know" that it will always hold, and checking it dynamically is in some sense redundant (provided we actually believe our checking to be correct and our environment to be sufficiently robust that things don't change out from under us) and I think that's a part of the reason the two feel opposed, but in principle you could check a property both statically and dynamically for a particular term.

Step back a little to the language level and they aren't at all opposed; you might want to check some properties statically and some dynamically (eg. static checking of class/interface vs dynamic nullability in Java) or check a given property statically for some terms and dynamically for others (eg. gradual typing).

[zozbot234]

Something that's checked dynamically is not a "typing judgment", by definition. It's a proposition established at runtime, possibly even with non-trivial data attached describing "how" the dynamic check succeeds, and possibly affecting program operation in its own right as that proposition object gets "passed" to downstream functions that depend on that dynamic check. These are two altogether different things.

[dllthomas]

Sure. Tip: if something's true by definition, it's usually not interesting. Substitute the appropriate phrase - "observation of a property which, in the static context, might constitute a typing judgement"? Note that we're here specifically considering things that can be typed statically, as outside of that setting there is no question of whether static and dynamic are opposed.

The rest of your comment seems concerned with the fact that the tagging infrastructure typically needed to check these properties at runtime can also be used for other purposes. That's true, but I don't see the relevance.

[dllthomas]

That probably reads a little snarkier than appropriate. My apologies for the tone.

[AlphaSite]

I think swift combines sumtypes with flow typing in an interesting way, where if you use a guard statement it then propagates that information into future uses of the type. If I remember correctly Kotlin also does something similar.

Pattern matching and sum types help, but they solve different problems.