Time to put another log into that dynamic vs. static typing fire… 🔥 https://lexi-lambda.github.io/blog/2020/01/19/no-dynamic-type-systems-are-not-inherently-more-open/

The article is flamebait, and it is also wrong. It begins with ad-hominem attacks on people who prefer dynamically typed languages, and insults Rich Hickey. Apparently, we are ignorant, we believe in myths and fallacies, and we need to be educated.

hasn’t rich built a speaking career on the emotional appeal of dynamic types? it’s been a while since i’ve watched on his talks but the one where he introduced transducers in particular is very much in this vein

Sure, it's just an opinion: https://blog.aurynn.com/2015/12/16-contempt-culture/

Implying someone is playing off the 'emotional appeal' implies they're lacking in substance. It is an insult. Rich talks about the ergonomics and constrains imposed by static types. It's ok to disagree with actual positions he had presented. That is not what happened here.

With regards to Corbin’s comments, I’m with the other commenters on this one:

Could you give examples of useful programs that are inexpressible in a typed way without a hierarchy of universes? Even when doing pure mathematics (which demands much stronger logical foundations than programming), most of the time I can fix a single universe and work with (a tiny part of) what lives in it.

Seems clear that Lexi is talking about the kinds of objects in day-to-day coding, not “infinity-categories”.

I’m wading into this having put way less thought into it than the rest of you, but… I’ve done lots of coding in C/C++, js, obj-C, swift, python, ruby, and perl. I’ve pretty much never felt slowed down by strict typing (ok, I admit parsing JSON in Swift with optionals was a bit of a nightmare), and I’ve been bitten in the ass LOTS of times in ruby and js by developer mistakes that their dynamic typing let happen (and would have been caught with stricter typing). There are lots of programming philosophy questions where I feel like I really “see both sides” (e.g., “there’s more than one way to do it” vs. “there’s one way to do it”, or heavy magical frameworks vs. reinventing the wheel), but typing has always seemed like a no-brainer to me — maybe I don’t want to go all the way to Haskell, maybe I want to be able to dynamically type when I want to, but most of the time, strict typing seems like it overwhelmingly pays off in practical terms.

The bit I found interesting (I’m generally tired of the debate too), was the dynamic/static vs. structural/nominal axes brought up in the last part. That I found a useful angle to look at data modeling from.

@Ben Wheeler I think that depends a lot on what you are doing. If a type system fits your problem, it’s a big help. If you have to fight it, it’s your enemy. I always wonder why the appropriateness of a type system for a domain is hardly ever mentioned in these discussions.

Hillel wrote a nicer piece here: https://buttondown.email/hillelwayne/archive/a-totally-polished-and-not-at-all-half-baked-take/

Static Typing and Dynamic Typing are orthogonal

Static means types are attached to syntax expressions and dynamic means types are attached to runtime objects. So you can have both, technically. But a lot of static langs throw away much of the type definition during run time (they don't have to). In 'one world' languages like Smalltalk, types are attached to objects and it is considered dynamically typed. But what if you verify some type safety of a subset of the the expressions present in the system? Does that make it statically typed and stop being dynamically typed? Or does it end up being both? I also tweeted this: The static/dynamic debate requires a point in time such that all information supplied prior to the point is 'static code' and after is 'dynamic data'. This is wrong. At any point the system should be able to verify itself with all available information. The refinement (or dependent?) typing aspect that Konrad brought up is another important concern. This also leads to verification by contracts enforced at runtime for things that are 'outside' what the types express. Side node: why are contracts and types expressed so differently? Shouldn't there be one way to express a constraint and the system can then apply it 'as soon as possible or practical'? I like the verification aspect of static types, but also like the ability to run a part of the program while the whole program may be broken (i.e. doesn't type check) - for fast feedback. That's usually associated with dynamic typing. I guess what I'm trying to say is there are many aspects here that get lost when the debate is brought up as static vs dynamic. I think more interesting models will emerge when we see the system without that lens. For this reason, I try to stay out of static vs dynamic debates. But as you can see, I fail. 😄

@Konrad Hinsen brings up a good point about appropriateness of the type system to the domain. And @shalabh provides an important insight about the relationship between static and dynamic typing. My Curv language is intended for live programming of graphical objects. It's intended for visual artists. But it is also its own extension language, so people with developer skills can use it to define new graphics primitives. To make Curv suitable for these two different audiences, I need a "tiered" structure. "High Curv" is a high level subset that contains everything you need for high level coding: procedural generation of graphical objects. "Low Curv" adds additional features that developers can use to define new library APIs with an easy to use interface and an efficient implementation. I want users to be able to develop libraries of new Curv graphics primitives and distribute them across the internet, without forking the project and hacking the C++ runtime. In particular, Low Curv supports GPU programming. High Curv is for end user programming. It needs to be easy to learn. From empirical studies I have read, the two big barriers to learning a programming language are learning the syntax, and learning the type system. High Curv supports live programming, which requires dynamic typing. And it has a very simple type system with a short learning curve. It is unacceptable in High Curv for a user to get a static type error that can only be fixed by adding type annotations. This also requires dynamic typing. Low Curv supports GPU programming: a Curv function can be compiled into a statically typed GPU kernel. To make this possible, there is a statically typed subset of Curv available within Low Curv.

@shalabh I am aware of one type system implementation that fits roughtly what you describe: the one in Shen (http://shenlanguage.org/). The type checker is an optional tool, you can switch it off. Which implies that types have no influence on the run-time behavior of the code, and run-time type checking is still there. Any property that can be tested can be turned into a type, but you then have to supply deduction rules to extend the type checker. I am not sure if types and deduction rules can be added per module rather than globally, that could be interesting. And of course you are completely free to write alternative or additional type checkers in Shen, though I doubt anyone has done this.