Dynamic type systems are not inherently more open
lexi-lambda.github.io
lexi-lambda.github.io
- Structural typing, i.e. instead of "you eagerly write a schema for the whole universe", just limit to what you need (basically, encode only the same kinds of assumptions you would make in a dynamically-typed language).
- It’s easy to discover the assumptions of the Haskell program [...] In the dynamically-typed program, we’d have to audit every code path — Left implicit in many debates about these topics are the "weights" that one attaches to these things, the importance and frequency of attempting such activities. Surely they vary, depending on everything from the application (Is it "code once and throw it away", or does it need to be maintained when the original programmers have left?) and down to the individual programmer's approach to life (What is the cost of an error: how bad would it be to have a bug? Etc).
- "This is a case of improper data modeling, but the static type system is not at fault—it has simply been misused." — To me this shows that bugs can exist in either the data modeling or the code: in a dynamically-typed language the two tend to coincide (with much less of the former) and in a statically-typed language they tend to be separate. (Is this good or bad? On the one hand you can think about them separately, on the other hand you have to look for bugs in two places / switch between two modes of thought, but then again maybe you need to do that anyway?)
- Structural versus nominal typing, where the latter involves giving a name to each new type ("If you wish to take a subselection of a struct’s fields, you must define an entirely new struct; doing this often creates an explosion of awkward boilerplate").
- "consider Python classes, which are quite nominal despite being dynamic, and TypeScript interfaces, which are structural despite being static." — This is highly illuminating, and just this bit (and the next) elaborated with some examples would make for a useful blog post on its own.
- "If you are interested in exploring static type systems with strong support for structural typing, I would recommend taking a look at any of TypeScript, Flow, PureScript, Elm, OCaml, or Reason [...] What I would not recommend for this purpose is Haskell, which [is] aggressively nominal"
For what it's worth, my opinion is that posts like this, on hotly debated topics, would do well to start with concrete examples and be written in the mode of conveying interesting information/ideas (of which there are a lot here) rather than being phrased as an argument for some position, which seems to elicit different sorts of responses — already most of the HN comments here are about static versus dynamic type systems in general, rather than about any specific ideas advanced by this post.
> The above JavaScript code makes all the same assumptions our Haskell code does: it assumes event payloads are JSON objects with an event_type field, and it assumes signup payloads include data.user.name and data.user.email fields.
What the post points out is that these exact same assumptions, and the same behaviour of what to do with an unknown event type, can be encoded into the Haskell types and code. Similarly, in the case of “val = pickle.load(f)” in Python, the moment we try to do anything with “val” we'll inevitably make some assumptions about it, and those assumptions are its type. (For example, if all we assume that `val` has a `.foo()` which returns a string, then that type can be expressed in a static type system, even in Java.) And for proxying unknown data, just don't specify more in your type than you actually need.
So the post repeatedly emphasizes that static typing does not mean “classifying the world” or “pinning down the structure of every value in a system” (and conversely with dynamic typing we never can process truly unknown data: whatever we assume, that's the type). Overall, the key thesis (“static type systems are not fundamentally worse than dynamic type systems at processing data with an open or partially-known structure”) seems (to me) convincingly demonstrated, and it seems everyone who understands the argument can get on board with her conclusion:
> There are many patterns in dynamically-typed languages that are genuinely difficult to translate into a statically-typed context, and I think discussions of those patterns can be productive. The purpose of this blog post is to clarify why one particular discussion is not productive
----
However, I think the word “inherently” or “fundamentally” is doing a lot of work here, to the extent that if the words “are inherently” were to be replaced with “tend to be”, then a good argument could be made afresh. The post admits to much the same thing, around “These two styles facilitate very different flavors of programming”:
> many dynamically typed languages idiomatically reuse simple data structures like hashmaps to represent what in statically-typed languages are often represented by bespoke datatypes (usually defined as classes or structs). [...] A JavaScript or Clojure program may represent a record as a hashmap from string or symbol keys to values, written using object or hash literals and manipulated using ordinary functions from the standard library that manipulate keys and values in a generic way.
and points out that this has many advantages (“the practical, pragmatic advantage of a more structural approach to data modeling”) to the way things are done in Haskell, and even more so in “all mainstream, statically-typed OOP languages”. These advantages are coming to “modern statically-typed languages” (see list).
So does this defeat the point of the whole post, if ultimately the approach usually taken in dynamic languages has advantages over the approach usually taken in ("typical") statically-typed languages? No, it's an matter of clarity — it's worth it to be clear when the issue is structural-versus-nominal-typing, not static-versus-dynamic-typing. So all this:
> may give programmers from a dynamically-typed background who have historically found statically-typed languages much more frustrating to work with a better understanding of the real reason they feel that way
But unanswered are questions like:
1. Should they be separate? In a dynamically typed language the two are blended, you write and run code (with representative inputs) to discover and refine your assumptions. You don't have to switch between two modes of thought. In a statically typed language, bugs in your assumptions will be pointed out by the compiler, and bugs in your logic will be pointed out by the program's execution.
2. Is it always worth being explicit about your assumptions? One can often get useful work done even with unclear, undefined, or even inconsistent assumptions.
3. Fine, the same set of assumptions can be encoded in both kinds of languages, but how different is the experience of arriving at the right assumptions?
Look at these quotes from the post, and think about the words "only", "just", "simply":
> static type systems only make already-present assumptions explicit
> We just have to be explicit about ignoring it.
> A static type system doesn’t require you eagerly write a schema for the whole universe, it simply requires you to be up front about the things you need.
Being explicit or "up front" in this way surely has a cost. At the same time, not being explicit also has a cost (of bugs). What the trade-off? (One does not always operate in environments where bugs have a high cost. For example, even code that does the right thing for 90% of users, but something catastrophic for 10% of them--like lose all their data--may be ok, depending on the importance of the "data" (previous scores in your game?), what expectations you've made clear, etc.)
In fact, too-enthusiastic data modeling can also lead to its own kinds of bugs:
> Suppose we’re consuming an API that returns user IDs, and suppose those IDs happen to be UUIDs. A straightforward interpretation of “parse, don’t validate” might suggest we represent user IDs in our Haskell API client using a UUID type [..] this representation is overstepping our bounds. [...] This is a case of improper data modeling, but the static type system is not at fault—it has simply been misused.
The claimed benefits are also all similar, and may not often be wanted:
> easy to discover the assumptions of the Haskell program just by looking at the type definitions [...] In the dynamically-typed program, we’d have to audit every code path
> If we want to ensure it [UserId field inside SignupPayload type] isn’t actually needed [..] we need only delete that record field; if the code typechecks, we can be confident...
> ensure application logic doesn’t accidentally assume too much
> the type system helped us here: it caught the fact that we’re assuming the payload is a JSON object, not some other JSON value, and it made us handle the non-object cases explicitly.
> The runtime representation of a UserId is really just a string, but the type system does not allow you to accidentally use it like it’s a string
> the parsing style of programming has helped us out, since if we didn’t “parse” the JSON value into an object by matching on the Object case explicitly, our code would not compile, and if we left off the fallthrough case, we’d get a warning about inexhaustive patterns.
Whether this is really a help is probably the big question. Incidentally, while I was rereading and thinking about this, came across a related paragraph in an unrelated article:
> requires covering 100% of the conditions, not just 99%. Edge cases must have applicable code, even when the programmer doesn’t yet know what the happy path should do. During early development, these edge cases can often be addressed by causing the program to crash, and then rigorous error handling can be added at a later point. This is a different workflow than in languages such as Ruby, where developers often try out code in a REPL and then move that to a prototype without considering error cases at all.
(From https://stackoverflow.blog/2020/01/20/what-is-rust-and-why-i... )
Ultimately, there's selection bias:
> programmers in statically-typed languages are perfectly happy to supply their assumptions up front
-- of course: programmers who are happy to supply their assumptions up front tend to be happier with statically-typed languages.
To me the stronger argument is that the boundary between programs is dynamically typed (interpreted and checked at runtime). This is true in the statically typed example as well - the JSON is interpreted and checked at runtime, not at compile time. There's nothing your compiler can prove in advance about what's in the JSON that you'll receive at runtime.
If systems that extend beyond a single program require dynamic typing, doesn't it make sense to invest more in ways to do dynamic typing better?
There hasn't been a lot of study on this topic* but what little there is shows that 3% of errors found can be mitigated with type systems, where they do not exist, fixing these classes of errors takes less time than it took to use the type system.
* https://www.infoq.com/presentations/dynamic-static-typing/
It seems to me like you're cherry picking evidence. Copy-pasting from a previous comment I made in another thread (https://news.ycombinator.com/item?id=19530274):
There is plenty of evidence showing that modern type systems reduce bugs considerably.
In Airbnb, they found out that 38% (!) of bugs could have been prevented by using TypeScript[1].
Another scientific study discovered that TypeScript and Flow could prevent about 15% of bugs in committed code [2]. And these aren't even measuring reduction of bugs in non-committed code!
Stripe is also writing their own type checker for Ruby and engineers have reported an increase in productivity[3].
[1]: https://news.ycombinator.com/item?id=19131272
[2]: https://blog.acolyer.org/2017/09/19/to-type-or-not-to-type-q....
Isn’t dynamic typing more or less a default state of not knowing anything at compile time about the values your data will take?
One could equally well ask “given that the boundaries of our systems are necessarily characterized by unpredictability, doesn’t it make sense to invest in more ways to isolate that unpredictability better (e.g. by use of static analysis)?”
Programs in such languages must be statically type checked --- by the coder.
Sometimes (usually?) those languages define the effects of type punning, so type mismatches are not necessarily errors. The programmer must know which are intentional (to be analyzed for correctness from a type-punning perspective) and which are bugs. This could come from comments or naming conventions.
Dynamic typing is a huge increment over this situation; what is surprising is how early the original Lisp people figured it out, while also inventing useful abstractions like symbols and whatnot.
Many interfaces have declared, enforced static types. I don't have to write any code to handle
SELECT birthdate FROM employees WHERE id = ?
Really? Okay, below is something that meets the definition of "arbitrary data". Can some static program process it and evoke its full meaning without the programmer having to develop an ad-hoc dynamic typing system?
(defun defset-expander (env macform name params newval setform)
(with-gensyms (getter setter args gpf-pairs gpr-pairs ext-pairs
pgens rgens egens all-pairs agens nvsym)
(let* ((ap (analyze-params params))
(exp-params (car ap))
(total-syms (cadr ap))
(fp (new fun-param-parser form macform syntax exp-params))
(fixpars (append fp.req fp.(opt-syms)))
(restpar (if (symbol-package fp.rest) fp.rest))
(extsyms [keep-if symbol-package
(diff total-syms (cons restpar fixpars))])
(xsetform ^^(alet ((,',nvsym ,,newval))
,,(expand ^(symacrolet ((,newval ',nvsym))
,setform)
env))))
^(defplace (,name . ,args) body
(,getter ,setter
(tree-bind ,params ,args
(let* ((,gpf-pairs (mapcar (op (fun list) (gensym)) (list ,*fixpars)))
(,gpr-pairs (if ',restpar
(if (consp ,restpar)
(mapcar (op (fun list) (gensym)) ,restpar)
(list (list (gensym) ,restpar)))))
(,ext-pairs (mapcar (op (fun list) (gensym)) (list ,*extsyms)))
(,pgens (mapcar (fun car) ,gpf-pairs))
(,rgens (mapcar (fun car) ,gpr-pairs))
(,egens (mapcar (fun car) ,ext-pairs))
(,all-pairs (append ,gpf-pairs ,gpr-pairs ,ext-pairs))
(,agens (collect-each ((a ,args))
(let ((p (pos a ,all-pairs (fun eq) (fun cadr))))
(if p
(car (del [,all-pairs p]))
a)))))
^(alet (,*,gpf-pairs ,*,gpr-pairs ,*,ext-pairs)
,(expand ^(symacrolet (,*(zip ',fixpars
(mapcar (ret ^',@1) ,pgens))
,*(zip ',extsyms
(mapcar (ret ^',@1) ,egens))
,*(if ,gpr-pairs
(if (consp ,restpar)
^((,',restpar ',,rgens))
^((,',restpar ',(car ,rgens))))))
(macrolet ((,,getter () ^(,',',name ,',*,agens))
(,,setter (,',newval)
,',xsetform))
,body))
,env)))))))))The requirement for dynamic typing can either come from the language, or it can be "Greenspunned", or some combination of the two.
For instance, in that data we can construct objects, and we can write expressions which interrogate an object's type.
Thus, that is an example of input data whose processing requires dynamic typing.
If the detailed requirements describing the inputs require dynamic typing, then the statically typed program has to whip up a facsimile of that dynamic typing. It's not an implementation detail; it shows up in visible, testable system behaviors.
And then, there you are, with the possibility of errors that are not caught at your compile time.
The debate that the article is addressing is the supposed difference of capabilities between programs written with static vs dynamic types, at runtime.
Here's one in C (less than 200 lines): https://carld.github.io/2017/06/20/lisp-in-less-than-200-lin...
Here's one in Haskell: https://www.defmacro.org/ramblings/lisp-in-haskell.html
You seem to have a set of rules that you think code in a statically typed language has to follow in addition to the type constraints in order for you to consider it sufficiently 'typed'.
If someone writes Haskell applications by defining an Expr type that is a sum of several dozen things, and then makes al their function arguments and return values of type Expr, is that still bona fide static typing?
My experience, having gone from dynamic typing to static typing and now pining for more expressive type features in my chosen language is that static typing changes where you have to spend the cognitive complexity budget.
To my mind if I return to a piece of dynamically typed code written any time other than in the same session I have to load a whole mental model of the entire code, what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs. I suppose the trade-off is that advocates say you can prototype things more easily when requirements are not known.
With static typing I only need to load 2 things, the high level goal, what I need to achieve, and the local context where I need to make the change. The rest is taken care of by static typing, I can encode all that cognitive complexity in the types and I never need to think about it again. But as I say, that's how my brain works, yours might work differently and that's fine.
Of course, one could say we should have both, and some languages -- like Java with JML, C with ACSL, and SPARK, as well as some research languages like Whiley and Dafny -- do. But this could add complexity, and the interesting question is, if you could just have one, what are the relative merits of either? My guess is that types would be better for enforcing code organization and for tooling (more efficient AOT code generation, safe automatic refactoring, code completion), because automatic transformations require automatic and sound inference, while contracts are better for correctness because they can more easily express stronger properties of interest, and require less effort to verify them (types require formal deductive proofs, while contracts can use those or a range of other techniques that vary in their cost and their soundness).
In short, types are not the only form of formal specification, but the different forms do have different practical characteristics. What matters is not just what we want to know about the rest of the code, but how we want to use that information and how certain we need to be. Unfortunately, theoretical results tell us that we cannot have a perfect system that is always correct, cheap to use, and can allow us to express rich properties.
Types are sound mostly because they are a stupid mini language, so easily enforced, like you said. Contracts are practical and convenient because you tend to write them in the language or a subset thereof that you’re checking. That’s hard to ignore.
GODP has you write a runtime check in regular code, and return as a result a proof value. Put that code in a module boundary. Then you have upstream functions expect a proof argument along with the value the proof is about. They’re tied together with a unique type variable (rank n or existential are the mechanisms of delivery for Haskell, but may differ in other languages).
head :: NonEmpty n -> Named n (List a) -> a
In this way you started from a dynamic, runtime piece of code, and ended up using a static type system to just ensure everything is passed around correctly which is trivial.
A single proof in this technique is nominal in the type (e.g. not null or positive or sorted ascending/descending), but combining them is done at the value level so there’s flexibility.
The bang for buck potential is large. I’m more interested in stuff like this than the dependent types direction that people are pushing for in GHC. If I wanted dependent types I have Agda, Coq, Isabelle, Idris, etc. to play with.
Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to express associativity with a contract system. Contract systems are very well-suited for imperative contexts (see e.g. Hoare Logic), where you have procedures rather than functions and you usually don't think about e.g. whether a procedure is associative or not. They work for functions, but are not as great a fit.
Dependent types allow for further expressivity, and, crucially, as long as you separate theorems from code (that is as long as you don't take Curry-Howard too seriously), there's no reason you're forced to prove a theorem with the type system if you find it too difficult.
Imagine:
concat : List a -> List a -> List a
concat = ...
concatSumsLength : (xs : List a) -> (ys : List a) -> size (concat xs ys) = size xs + size ys
concatSumsLength = proofByPropertyTest concatPropertyTest
concatPropertyTest = (1000 different lists concatenated together and then checking that their sizes add up)
There's no reason that concatSumsLength needs to be satisfied by a true implementation, unless you require that its value be usable at runtime. However, as Idris 2 shows, there's no need for that to be true (or even Coq with Prop vs Type). You can just annotate it as erased at runtime.
If you have a way of ensuring that certain values are never used at runtime, then there is no reason that your proof obligations must be met through satisfying the type checker.
With some template-haskell you could run the property test at compile-time, and then use that proof later (e.g. for an instance of Semigroup which would require a argument proof of associativity), in languages like Unison that never run the same test suite twice (due to Content addressable code), this would be feasible. Or just run the property in your test suite and hope that the developer runs the test suite often. GHC erases data types that aren't actually evaluated in many contexts, so we even have erasure too.
I like your angle!
Contract systems can express anything that can be expressed about a program. Some allow you to specify separate lemmas (e.g. see http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_toc...) . The difference between dependent types and contract systems is that contract systems can be verified by deductive proofs, or by a host of unsound techniques, while dependent types require deductive proof (or, in some experiments, other sound techniques like model-checking). If dependent types would accept unsound proofs, the soundness of the entire type system would be compromised to the point of undefined behavior.
The problem is that deductive proofs have so far shown significantly worse scalability than other formal methods, which is why most of formal methods research is looking elsewhere.
If dependent types could be made more flexible, they will be as good as contract systems.
This seems like too strong of a statement. Every language that allows for nontotal functions has a type system allowing for unsound proofs. This does not mean the type system is compromised to the point of undefined behavior.
Dependent Haskell is explicitly going to be unsound even in the presence of totality (type in type). Idris allows for partial functions by default (although you do need to annotate if you want to use it at the type level and the compiler doesn't know it's total). Dependent type systems are not required to be sound by any means.
If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language.
Leaving that aside, my point is that as long as you don't need your proofs at runtime, you don't have to use a deductive proof with dependent types! Substitute the property check thing there with a model checker if you want 100% assurance, but you don't even need a sound verification! If you're okay with just 99% confidence instead of 100% then just do the property test and be done with it (that's my example with concat and chrisdone is talking about when you would run the property test). If you're feeling really adventurous just assert the statement without proof and move on. If you don't run it at runtime how you prove something or even if you do is up to you.
Also out of curiosity, how do you express that, say, a static method with two arguments is associative in JML or any other contract system, Hoare Logic based or otherwise? I suspect you can, but I also suspect it looks annoying and hacky where you essentially encode a function application counter in your ambient state and have to basically make an inductive statement. EDIT: ah ha in JML you have the keyword pure that extends Hoare Logic so I suppose you do an assert with pure? But then how do you express the general notion of associativity? By requiring purity as a precondition and then writing out the condition again? Can you specify purity as a precondition? I'm not sure how you do that, presumably you'd need JML to be able to recognize a SAM class and then be able to tie purity to that, which seems hard if not built-in.
Whereas with dependent types it looks very similar to the usual notation.
(x, y, z : A) -> x `op` (y `op` z) = (x `op` y) `op` z
op : A -> A -> A
isAssociative : (op : a -> a -> a) -> ((x, y, z: a) -> x `op` (y `op` z) = (x `op` y) `op` z)That depends on the runtime type system. If you can switch an int for a string (which is not hard in a dependent type system -- rely on the output of some silly arithmetic function that you only tested and omit a proof and use it in some function that indexes types by integers, and you just might cast an int to a string), you will more likely get some UB and quite likely a security problem.
That's why I think that when it comes to correctness contracts are superior to types, and when it comes to tooling and organization, types are superior to contracts. Functional correctness is one area where flexibility is crucial, and soundness is never required because it's impossible anyway. Types, which are used for automatic transformation and code generation is one area where soundness is quite important; we shouldn't mix the two.
> Also out of curiosity, how do you express that, say, a static method with two arguments is associative in JML or any other contract system, Hoare Logic based or otherwise?
I don't know the arcana of JML, but I see no reason why, at least in principle, you couldn't do the same thing:
pure
\forall A x,y,z; foo(x, foo(y, z)) == foo(foo(x,y),z)
However, there is a difference -- not between specification with dependent types and contract systems, but between the semantics of the language where expressions mean something similar to "partial functions" (or even something similar to functions) and a language where they mean something else (like predicate transformers). In the latter, we don't in general represent computation as functions, so specifying something like associativity would normally be done as follows: define `isAssociative` on functions (not computations), and then specify that a computation computes a function (that is associative). That's how I would do it in TLA+, for example; I think that in Why3 as well.
Finally, it's important to remember that the very concepts can be different among languages. For example, all specifications of "higher-order" computations in functional languages (i.e higher order subroutines) become first order when you describe them in TLA+ (https://pron.github.io/posts/tlaplus_part3#higher-order-comp...). Lamport had this to say:
> Comparisons between radically different formalisms tend to cause a great deal of confusion. Proponents of formalism A often claim that formalism B is inadequate because concepts that are fundamental to specifications written with A cannot be expressed with B. Such arguments are misleading. The purpose of a formalism is not to express specifications written in another formalism, but to specify some aspects of some class of computer systems. Specifications of the same system written with two different formalisms are likely to be formally incomparable… Arguments that compare formalisms directly, without considering how those formalisms are used to specify actual systems, are useless.
The difference here is, then, not between specifying with types or with contracts, but between different formalisms.
That's different than UB in the type system itself, which if you lie to it at worst just becomes inconsistent, but although that sounds quite scary, it's not really a big deal if you're not using dependent types as a theorem prover and you know where the inconsistency stems from.
Now perhaps your contention is that dependently typed systems tend to have weaker runtime checking, which I still disagree with. You do have weaker runtime guarantees with Idris 1's native code generator and of Agda's code extractor, but this is not true of Idris 1 on JS or its other code generators, which inherit their hosts' runtime systems, or Idris 2's native code generator, which inherits Chez Scheme's runtime system.
RE computations and functions yeah I definitely overreached. I somehow completely forgot that Hoare Logic has the ability to have unrestricted first-order logic. I got too fixated on JML, where in retrospect the difficulties only come from the awkward way that Java tries to handle higher-order methods like reduce (that was my initial impetus, verification of parallel reduce). I totally forgot I've done the isAssociative property in Dafny before and there it's exactly as you say, it's a function that you then put on top of a method (Dafny's notion of "computations").
The Lamport quote is a good reminder not to poo-poo different formalisms, but I've had a great time with systems like Dafny. I don't think dependent types are the holy grail of verification. My contention in fact is that the gulf between dependent types and contracts is not as large you're making it out to be.
Dependent types break down if you have pervasive mutability, i.e. as in an imperative language, for which Hoare Logic is very well-suited for. You have to express the mutability at a type level that's also is transparent enough to the type system to make assertions which makes things very annoying. (And no I don't use mutability/imperative as dirty words, most of my day-to-day work is in imperative languages and that's just fine by me, a lot of algorithms flow more naturally as imperative ones).
But if you have a language where everything is immutable, dependent types are fantastically expressive. And as long as you don't use the type inhabitants at runtime, their "proofs" or lack thereof are also very flexible. Hell, you could even generate a runtime assertion from a dependent type if you wanted to and have the compiler automatically insert those in place! You could even do that generation in a user-defined library without compiler support if dependently typed languages supported typecasing and didn't impose parametric polymorphism in all cases (useful in a non-dependently typed language, less useful in a dependently typed one). They don't, but that's a different story (for all my excitement about dependently typed languages, there's so many other ergonomic hurdles to get over first, as is true of a lot of the current state of code-based verification tools).
Indeed, dependent types and contracts converge in many ways if you have pervasive immutability. The main difference is that dependent types are more integrated into the language and don't have as many contract-isms. An invariant required by a function becomes just another argument. A lemma is just another function. Those contract-isms are necessary in a mutable environment (it would be rather painful to try to drum up some sort of type-indexed loop monad to try to express the notion of a loop-invariant in a dependently typed language, especially if the loop accesses non-local resources), but are not so much in an immutable one.
Oh BTW, speaking of limitations of formalisms, I'm pretty sure you're right on Twitter that Hillel Wayne's hyper-property isn't actually truly a hyper-property and can be described with the temporal quantifiers TLA+ has. A better example (that I don't think can be expressed in TLA+) is something like "variable independence," the statement that for any behavior where a variable "a" takes on some trace, there is another behavior such that "a" has a different trace, but all other parts of the behavior are the same. That is you can delete "a" from your spec and nothing would look different, no behavior would ever change (this requires either quantifying over all predicates or manipulating behaviors directly). Another example would be something like "x 'usually' takes n steps" for some definition of usually (mode, median, average, anything that's not a strict upper bound). Even expressing "n steps" in TLA+ is kind of wonky, but do-able with an additional counter variable (although that makes TLC unable to check termination).
Oh and of course since you've linked your own TLA+ link, many many thanks for your TLA+ series. It was an invaluable source right alongside Lamport's own materials when I was learning TLA+ on my own.
I see what you're getting at, but there is one other crucial difference: the types we're talking about here are usually checked at compile time, whereas the contracts we're talking about here are usually checked at run time. Although the latter may be more expressive if other things are equal, other things are very much not equal in this respect.
How much that matters depends on the nature of the software and how it is to be deployed and used. If you're writing a program for your own use, it might not matter much at all. If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.
No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes.
> If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.
Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.
Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time.
Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases.
As someone who has worked on relatively high-reliability systems, I can say with 100% confidence: it depends. This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. In such cases, a powerful static type system certainly can be a useful safeguard against introducing defects during the translation.
Not really. What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. This means that some deep properties either require a lot of work (using a type system such as Idris's) or are excluded from the type system at all. Contracts allow you to check a property in unsound ways, too.
As far as correctness is concerned, contracts do everything a type system can, but more flexibly. Type systems, however, have advantages related to tooling and efficient code generation by an AOT compiler.
> This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code.
Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.
I think you're making the same point that I am, but perhaps from the opposite direction.
Of course contracts are more general, but the aspects of a contract that you can prove automatically in advance are similar to what you can typically do with a good static type system, and the limits of a decent static type system fall around the point that contracts become more powerful but only at runtime. This isn't an accident, it's a fundamental equivalence.
For example, you mentioned SPARK before. One of the interesting things about SPARK is the extra flexibility you have when adding constraints on integer data types. The proof system can verify certain properties (or warn you that it can't). That can provide safeguards against, among other things, some very common logic errors like out-of-bounds access to data structures.
However, the fact that we're dealing with integer values is very helpful in this respect. Lots of behaviour is fully specified no matter how much we manipulate those values. For the same reason, dependent type systems can often provide similar guarantees. The curious property of C++ templates that they allow integer as well as type parameters has allowed for all kinds of handy metaprogramming tricks along similar lines.
Now, suppose we're working in the much less convenient world of floating point values. It's still helpful to have warnings about, for example, potential underflow or overflow conditions, for all the same reasons. However, given the inherent imprecision of floating point data, it is impossible to prove such conditions in advance in almost any non-trivial case. You can certainly have a precondition on a relevant function that, for example, adding two input values must not entirely lose the smaller value due to loss of significance, but you won't find out about inputs that violate the contract until you run your program.
Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.
You can do the specification in any number of ways. Unless you want to classify all of mathematics as "a contract system", which is true in a sense but so general as to lose any useful meaning of the term, your statement above is too strong.
> what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs
But more about what the language offers. Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) and normally stays away from mutation, but when needed, makes it really explicit and easy to find those mutations.
Goes beyond types? Statically-typed languages can have polymorphism.
(s/def ::integer integer?)
But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function.
So spec can used to implement a type system but also to implement things that aren't type systems.
Check out dependent type systems. These allow you to define, mindbreakingly enough, types that __depend on the values you assign at runtime__, and functions whose type depends on the values passed as arguments.
Don't ask me how it's done; it's all dark magic to me. All I know is that people who use dependent type systems claim they are very good at certain uses involving incoming streams of unknown data, like parsing binary protocols.
For what it's worth I definitely agree there can be a lot of overhead added by typed code especially in Java or C#, but I suspect it might have less to do with the type system and more with the enterprise-ness or otherwise of those code-bases. Designing a good typed API for other people maintaining the same code-base is difficult
To aid you in the latter task, you can press a key in your editor to fetch an automatically-inferred type for the name under the cursor and insert it into your code, then refine it as necessary if you find it to be too general (inference always gives the most general type possible).
If you're talking about exhaustiveness checks, you can disable those and use `-fdefer-type-errors` to compile programs which don't type-check.
Although I will say that most of the time when you have a Maybe instance that you know is Just, it means you're branching in the wrong part of your program.
Right, but if you were using, say, Idris, the program would type check. It's just that Haskell's type system is too weak. Disabling type checking is not what the question was about. The program is type-correct, yet not in Haskell's particular system.
> Although I will say that most of the time when you have a Maybe instance that you know is Just, it means you're branching in the wrong part of your program.
Perhaps, but that doesn't change the fact that if you write it in some way that is perfectly correct, Haskell's particular type system will still not accept your program.
[1] https://github.com/DanielG/ghc-mod
Ghcide is on my list to try next as it's gotten a lot of attention lately.
A full rebuttal of this blog post would take much longer, but suffice to say inference does the exact opposite of what they are claiming; it increases readability and usability.
A few human-subjects studies from different labs have recently been ran on this and the findings mostly agree with my opinions. Papers forthcoming.
Also, if lack of type annotations were a common problem, you would expect Java programmers who switch to Python to frequently want to annotate all their types. But as far as I know this is not the case: even now that mypy is becoming popular, people only annotate the types that it can't infer.
But how would companies/people know if it damaged readability? There has been little research on this (a few studies are currently in peer review!) and our intuition about such things is often inaccurate. There are so many other confounding factors that it is hard to isolate just type inference/annotations.
That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?
In languages with even reasonably good type inference you'll find that the idiom is not to annotate types at the very least inside function bodies. And in OCaml, which has principality of type inference i.e. the types it infers cannot be overridden and corrected by manual annotation, the idiom is to not annotate implementation files at all.
edit: In Haskell it goes beyond just locally inferring variables, it enables a new type of development with typed holes that feels more like a back and forth conversation with the compiler. I don't see how "I can leave the types off my C# variables" has anything to do with that.
You talk about cognitive load of looking up type info but there's also a cognitive load to having to parse every type annotation over and over again whenever you read the code. And since code is read more often than it's written, that's really just optimizing for the wrong load. As you re-read a codebase over time you'll get familiar with its types. And then the annotations start to get in the way. This is in fact one of the reasons people prefer dynamic typing.
> My response? Go refactor your hideous code.
To what? Would be very interesting to see your suggested refactor of that code.
> Before every language designer blindly accepts type inference as a good thing, I propose that some research be conducted.
What would be the research question(s) specifically?
How many systems have you prototyped in Haskell?
That's very much my experience, as well. Assuming - and it's a very big assumption - that your use case has equivalent library support.
But a large refactor on a large project is still a pain. By the time you get there, you still want your model stable and/or flexible enough that you don't need to do that much.
On a small enough project, every refactor is easy enough that you can lean into it. Make a bunch of assumptions you're not confident about, setting up the types so you're sure you'll know what needs fixing when they're wrong. Then you test those assumptions as you write - and run - more code.
After typechecking it leaves provisional stubs in .pytype/pyi/, and it has a tool to merge them into the original code.
mypy has stubgen: https://mypy.readthedocs.io/en/latest/stubgen.html
As far as I know it's less powerful since mypy isn't really built for unannotated code and pytype is.
Type inference, as others have suggested, does not do what you want. If your program is well-typed according to a particular type system which you must have in mind while writing the program, they'll save you from writing explicit type annotations, but they cannot come up with "correct" type for a correct program that's not written for that particular type system.
This is one reason my favorite model is the "egg model" - hard outer shell (static typed signature) of a function with a soft gooey center - dynamic code internally. It lets you use the convenience of dynamic typing but confines the scope of the mental budget to understanding just a few lines of dynamically typed code. Languages like groovy are pretty good for this type of code.
People who are only used to dynamic languages may feel like a static language’s type checker is an overbearing teacher (from the 1950s) standing over your shoulder, just waiting to jump on you for every silly mistake! While that feeling is common and valid as you’re learning the language, when you become fluent you see the compiler as more of an ally. You can call on it with a keystroke and it will find many problems that would otherwise only happen at runtime, possibly months or even years in the future!
Moreover, in more advanced languages (such as dependent typed languages), the compiler can actually infer the body of your functions which leads to a totally different style of programming that feels like a snippet plugin on steroids.
https://www.unisonweb.org/docs/refactoring
In Unison you can implement a change and propagate it just far enough to run one little experiment. There’s no need to upgrade all your code at once.
I've written big applications in python, every time I made a significant architectural change (which might not even be huge code-wise, just far-reaching) I feel super uncomfortable. I know that I have to follow up with an intense testing session to make sure that I go through all code paths and everything still works correctly. Even then sometimes the testing is not thorough enough and you end up with a regression in production.
As a result I tend to avoid these types of changes as much as possible, even I believe that the application would benefit from them.
Meanwhile in Rust it's a breeze. Yesterday I decided to make a small but far-reaching change in an emulator I'm writing: instead of signaling interrupts by returning booleans, I'd return an "IrqState" enum with a Triggered and an Idle variants. It's more explicit that way, and I can mark the enum "must_use" so that the compiler generates a warning if some code forgets to check for an interrupt.
It's like 4 lines of code but it means making small changes all over the codebase since interrupts can be triggered in many situations. In Python that'd be a pain, in Rust I can just make the change in one place and then follow the breadcrumbs of the compiler's error messages. Once the code builds without warnings I'm fairly certain that my code is sound and I can move on after only very superficial testing.
I’m sympathetic to the idea that you want to solve the immediate problem first rather than have to move the entire codebase through several iterations. I’d be interested how well Unison handles that on a complex codebase in reality though.
Why I would want to go to dynamic typing is beyond me. My performance/efficiency would greatly decrease. .
The next change I will implement will likely be to not allow null in a property, which can be done in c# 8
Dynamic typing won't help with that.
One of those is worse.
Also, some statically-typed languages (like Haskell) allow you to defer type errors to runtime if you really want.
Ideally, you want a language that starts out completely untyped, efficient for that initial “sketching in code” phase. Then, as your program takes shape, it can start running type inference with warnings only, to flag obvious bug/coverage issues without being overly nitpicky. Then finally, as you refine your implementation and type-annotate your public APIs (which does double-duty in documenting them too), it can be switched to reporting type issues as errors.
Unfortunately, a lot of typed languages behave like martinets, and absolutely refuse to permit any such flexibility, dragging the entire process of development down their level of pedantry and generally making early development an almighty ballache. Conversely, untyped languages provide sod all assistance when tightening up implementation correctness and sharpening performance during late-stage development; it’s pure pants-down programming right to the bitter end.
Mind you, I think this says a lot more about programmers (particularly ones who make programming languages) than it does about languages themselves.
--
† (Unless, like, you’re Donald Knuth.)
Additionally, it is fairly typical in js to use functional programming styles, making type inference a breeze / provable / not introducing much boilerplate by adding types.
For example, in Haskell: https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...
On the top of my head:
* Dart (just don't give a type and the variable is dynamic)
* Groovy (add @CompileStatic or @TypeChecked when you're ready)
* Racket (start using typed-racket)
Also, none of them are in the mainstream, which creates general challenges to adoption. Fortune favors the entrenched.
...
Another thing worth considering IMO is structural rather than nominal typing, which fits more with the “if a value looks right, it is” philosophy that untyped language aficionados enjoy without going for full-on pants-down duck-typing. ML favors this, IIRC (I really must learn it sometime).
I find nominal typing can get a bit excessively OCD, demanding so much additional annotation as to obscure the code as much as clarify (“Hi, Swift stdlib!”).
I also wouldn’t mind being able to define sets of permitted type mappings in advance, and letting the compiler figure out where in the code to insert (implicit) casts. For instance, if I’m passing a variable typed as integer where a float/string is expected, it really wouldn’t kill it to promote it automatically; most are perfectly happy to promote integer literals where a float is required after all. (And if I do want to know about it, which I usually don’t, I can always turn warnings/errors on.)
std::vector<Pair<std::string, MyInt>> s;
s.push_back(Pair<std::string, MyInt>("a", MyInt(1)));
s.push_back(Pair<std::string, MyInt>("b", MyInt(2)));
s.push_back(Pair<std::string, MyInt>("c", MyInt(3)));
Look at this Rust code:
let mut s = Vec::new();
s.push(Pair::new("a", 1));
s.push(Pair::new("b", 2));
s.push(Pair::new("c", 3));
fn foo(x: f64, y: f64) -> Point {...}
def foo(x, y): ...
std::vector<std::pair<std::string, int>> s;
s.push_back({"a", 1});
s.push_back({"b", 2});
s.push_back({"c", 3});
That IS better than Rust since it migrates the type from n container members to just the 1 container. It doesn't seem possible to replicate that in Rust[0].
My Rust evangelism IS hurt by this. But its HP bar is big[1].
0: https://news.ycombinator.com/item?id=10891892
1: https://www.reddit.com/r/rust/comments/bya8k6/programming_wi...
Also, being a C, you still have to declare* all the types, even when only `id`, which is tedious AF. Also-also being a C (which doesn’t so much have a type system as a loose set of compiler directives for allocating memory on the stack), it’s not as if declaring exact types does much to improve program correctness. You can still stick any old object into an `NSString*` at runtime; it just dumps stack when you try to send it an NSString-specific message is all.
Oh, and one more: the ObjC compiler can have trouble recognizing selectors (method calls) when the receiver’s type is `id`. Being a C, obviously you have to import all the headers just to use them at all, but if in searching those headers it finds two method definitions with the same name but different parameters then its superficially Smalltalk facade quickly breaks down. (I’ve run into this, it’s very annoying.)
The current dynamic language ground is riddled with linters and additional tooling that static languages have solved already. This costs developer time (god, the amount of time people spend on writing an eslint config and selling it.)
Statically typed languages will confront you with a lot of obscure errors and just generally get in the way.
Eventually the good developers will eventually learn the language and get burnt by float32 / sql injection / xss / dates / not validating input and they'll learn enough to become extremely productive.
Static languages have evolved a lot; now the standard error messages are far better and the tooling is amazing. At the same time a lot of dynamic features - usually reflection based - have come along and provided their own breed of arcane and nutty rules and errors which seem designed to catch out only the strongest developers (the ones which break SOLID are the best!).
OTOH, a good [weak] untyped language should accept a float where an int is expected as long as it has no fractional part (otherwise it should throw a runtime type error, not implicitly round). Depending on how weak the language is, it could also accept a string value, as long as it can be reliably parsed into an int (this assumes a canonical representation, e.g. "1.0"; obviously localized representations demand explicit parsing, e.g. "12,000,000.00").
A good rule of thumb, IMO, is: “If a value looks right, it generally† is.” This is particularly true in end-user languages where conceptual overheads need kept to a bare minimum. (Non-programmers have enough trouble with the “value” vs “variable” distinction without piling it with type concepts too.)
--
† Ideally this qualifier wouldn’t be needed, but there may be awkward corner cases where a simpler data type can be promoted to a more complex one without affecting its literal representation. That raises the problem of how to treat the latter when passed to an API that expects the former: throw a type error or break the “no lossy conversion” rule? There’s no easy answer to this. (Personally, I treat it as a type error, taking care in the error message to state the value’s expected vs actual type in addition to displaying the value itself.)
Predicate assertions instrumented to run during development catch an equivalent amount and more, since they can evaluate data at run-time.
Dynamic types combined with argument destructuring allows for very loosely coupled modules. I can see it being similar to row polymorphism, but then you have to ask whether it's worth the extra time? In many business apps a significant portion of LoC is mapping JSON/XML to DTOs to Entities to SQL and back. If everything starts and ends with JSON coming from an unverified source, forcing it into a "safe space" statically typed business program is almost ignoring the forest for the trees, possibly even giving a false sense of security. It's (over) optimising one segment of the system; it's not necessarily a waste but it's probably time which can be better spent elsewhere.
In fact, proponents of static typing would argue that the types make your code easier to refactor later, because you will be aware of all the usages, and able to move things around with confidence.
The drawback is that you need to make the entire codebase correct (or commented out) every time, not just some isolated piece you're experimenting on.
I agree with the GP‘s point that static typing forces you to do that kind of design work earlier.
(Edit: You raise a good point, though. I think a lot of people run into this kind of problem with static typing.)
The problem? Every one of your 20 levels of functions/subroutines has an unnamed grab bag of variables. You get to keep that in your head. If you want to know if you have a value in a given branch of code, your best bet, aside from reading the code of the entire callstack, is to dump @_ in a print statement and run the entire program and get it to call the function you are in. Oh, and if one of those values contains a few screens worth of data, you will need to filter that out manually. Even "documentation" in the form of comments or tests will be unreliable due to comment-rot or mocked test assumptions.
Even in Python, I'll often have to go up the callstack to know what a named parameter actually is. And if similar shenanigans are going on, I again have to pull out a debugger or print statements to know what I can do with an argument.
With a static type, I see plain as the text on my screen what type I have as a parameter and I immediately know what I can do with it. As weak as Go's type system is, it is worlds better than Perl and Python for maintaining and creating large, non-trivial codebases. The price is passing it around at the time of writing.
If you only have to write the type once at the top of the 10 layer, you don't have to do much to change it.
However, that's pretty much the textbook example for designing with dependency injection in mind. Static typing won't fix a terrible architecture.
The original description sounded like 13 functions being manually chained together, each inside the last. Where to go from there is very situational.
Using a POC is pretty much a given.
For transformation in the simplest form, I'd typically have a series of extension methods (or some equivalent, like a transformation class which only has methods and holds a reference to the object) which can be called to transform and return the object or return a modified copy of the object. That's easier to test and debug as each method doesn't need to know about the one above/below it (they get called in parallel). You can also easily modify the order of the transformation, or cut out parts of it. When testing/debugging, you just initialize data to some state, then test the broken piece of the pipeline.
If the 13 vertical calls are for initialization, DI allows you to turn that into 0 calls. You probably need reflection in your language to make DI work though. I've never liked DI frameworks built by others, and have generally made my own.
All that said, I'd stand by my point that if 1 item is passed vertically through 13 functions before it gets used, then there's probably some way to either make things a bit more horizontal, or to automate the passing.
Another strong belief: If DI or some other "good" design tool results in more lines of code or significantly more confusing code, then either it's being done wrong, or it isn't applicable to the situation. There are generally more wrong places to use a tool or pattern than there are right places to use them. A power drill is a terrible hammer.
It's basically a fancy way of saying 'Use reflection to read all of the dependencies that exist in my code, and then automatically initialize those dependencies and pass them to the classes which need them.' This (for me) is a recursive process which starts at root "singleton" objects (single per DI session), then moves down through the tree that is my code and its dependencies.
Typically, dependencies are passed via constructor then stored in a field. I personally think that's a dumb way to do it, as I'm using DI to eliminate boilerplate code, and you don't often get code more boilerplate and tedious than copying a variable into a field. I instead mark fields with obvious attributes that show that DI is used for initialization, then have my DI framework automatically fill them in.
People often overuse interfaces with DI, which leads to very difficult to trace code. I consider that an anti-pattern unless writing a library for others. Unfortunately, I think the people doing this have made DI seem like a trade off: you remove boilerplate code, but you lose clarity. You'll see this in virtually every DI tutorial, which is unfortunate. DI can be done just as well with concrete objects.
If you're using a language with reflection, I'd highly recommend learning a DI framework. Once you've figured out what you don't like you can find a framework that works the way you prefer, or in the worst case write your own. You definitely have to structure your code for DI, and it's difficult to add after the fact. That said, I was able to chop 5 to 10k lines off a 100k project I converted last year, and more importantly adding new functionality became much faster and easier. Again YMMV.
Adding a double and boolean field to a Context object, I don't have to touch anything at the intermediary API layers. Just as with your tuple/dict.
As far as static types are feasible they are great to have. Clojure's spec is the gold standard I work to; if anyone has a better system it needs a lot more publicity.
But this is exactly the GP's argument, no? According to the agile philosophy (and my personal experience), we don't have enough information at the start of the project to make right decisions about all parts of the implementation - so we try to decide about just the most crucial architectural aspects and make the rest as easy to change at possible, learning as we go.
From this perspective, the argument is that dynamic languages make it easier to postpone some decisions and allow us to quickly experiment with the things we've left flexible. And then, over time, once we're more confident in our decisions, we can put in the effort to repay this technical debt and lock things down to some desired level.
that is exactly why I like static typing - I can just change stuff and ask the compiler to kindly list all the places that need to be updated to accomodate for the change.
Yes, taking an unknown structure in your program is the easy part. Programming against an unknown structure is where the problem lies.
I'd love to hear more examples of programming against such input that are beneficial over "parse don't validate" idea.
Of course, once you adopt a "follow the spec or GTFO" stance, you reap other benefits as well; for example you are free to adopt a sensible binary format :)
A cautious, forward-thinking designer-developer would interpret it as “allow for unknowns”. Whereas sloppy-ass cowboys think it means “accept any old invalid crap” and pass their garbage accordingly.
One of these philosophies gave us HTTP; the other HTML. And no prizes for knowing which one is an utter horror to consume (an arrangement, incidentally, that works swimmingly well for its entrenched vendors and absolutely no-one else).
A simple example is a ring web stack, where request flow threw different functions that transform the http request.
Each function just assumes the keys its needed are there, or to do input validation, you just validate that the incoming map has the keys that you require but does not care what else is in there. Clojure Spec will also do validation of the value in that key, even if it is an arbitrary complex map.
What this gets you is that you can pass around generic structures, that can be used with all standard Clojure functions and most libraries, validation is applied as needed on those keys that you need.
AFAIK this can also be done in a type safe manner in languages which support extensible records/row polymorphism.
This works in Haskell, just as it does in Clojure.
f :: Map String String -> Map String StringAgreed. There's a reason that serious correctness-oriented languages, like Ada, do not use this approach.
In other words “walks like a duck/quacks like a duck” is enough for most of the open world operations, no need for Platonic-like ideals or Aristotle-like categorizations. In the real world we can still use any piece of wood or stone as a table as long as food doesn’t fall off it, because said piece of wood/stone quacks and walks like a table, while Plato or Aristotle or most of the static type proponents would argue that we shouldn’t do that as that piece of stone or wood doesn’t have 4 legs and as such is not really a table/doesn’t correspond to the idea/type of a real table.
You’re advocating for structural typing, which is a property of (many) static type systems. The view you project onto Aristotle/Plato/static-type-advocates is nominal typing, which is just a different kind of static typing. Many languages support both kinds (for example, Go, Rust, and Python’s static type system, Mypy).
Note that languages with structural typing will correctly accept your stone table and reject objects unsuitable for holding food (where “holding food” is the structure a type must implement) while a dynamic type system will happily allow anything to be passed in as the table, including a waterfall or communism and you’ll be none the wiser until your bread is wet or your country is starving.
I guess it's turtles all the way down, because (from my pov at least) deciding on what "structures a type must implement" is pretty similar to saying "a table is a table only if it's got 4 legs". Again, from my pov, a dynamic-like language is a lot more tolerant with the unknown unknowns of which the open world is full of, it doesn't depend on any "structure implementation" being defined or on anyone else counting the legs of said table.
The idea is that callers/clients define the structure they’re going to use. If the caller needs something that can hold food, then only things that hold food can be passed in. If the caller depends on having four legs, then only things with four legs can be passed in. If the caller depends on four legs and can hold food, only objects that satisfy both properties can be passed in. The type doesn’t choose which structures it implements (that’s nominal typing) the type just is and it either implements a contract / has the right structure for a given client or it doesn’t. Check out Go’s interfaces for a more concrete example.
> Again, from my pov, a dynamic-like language is a lot more tolerant with the unknown unknowns of which the open world is full of, it doesn't depend on any "structure implementation" being defined or on anyone else counting the legs of said table.
This is inherently untrue because structural typing is simply the formalization of the same logic you use when composing programs in a dynamic language. The same logic that lets Python document an argument as “file-like” is formally expressed in a static language as “anything with methods read(), write(), seek(), close(), etc”. This still gives you the openness you need (you can pass in other types even if they don’t know about your file-like interface) but it guards against runtime TypeErrors and AttributeErrors.
Give static typing an earnest try. And be discerning about the source of friction you encounter: is it because static typing is making it harder for you to write big-prone code? Is it because the language makes heavy use of inheritance (and nothing to do with static typing at all)? Is it because the language is very verbose (and nothing to do with static typing at all)? Or maybe the language has a bizarre syntax and jargon-laden, conflicting documentation, in which case these also aren’t properties of type systems but rather functional languages ;).
When you can't afford to be sloppy -- when human lives are literally on the line -- correctness-oriented programming comes roaring back into vogue.
Clojure specifications can also be converted into other forms of specification like graphql schema, database schema, json schema etc
The best I've seen a type system do on user input is blow up at runtime and that's not good enough for me
Then you haven’t been looking closely enough. The article addresses exactly this wrong argument.
What happens to the example code if UserName is an Int?
It was intended for network protocols/distributed systems communications — situations with extremely loose coupling between components. It’s useful in this very specific paradigm, not for arbitrarily programming anything.
From a maintenance point of view, the statically typed ones definitely win out.
Trying to reason about bits of code with no idea what was supposed to be passed in. Working out which bits of code are actually dead and can be safely removed. Refactoring bits of code. All incredibly difficult in the dynamically typed systems.
Given the choice, I would not embark on a large complex system without the benefit of a strongly typed language.
The other aspect of maintenance is in keeping a running system up without any downtime. There are plenty of of use cases where recompiling code and relaunching an application is not a viable solution. You need to be able to patch a running system. Dynamic typing is beneficial here because you need the old running code to be able to call into the new code which it knew nothing about when it was originally compiled.
This article really bends over in strange ways to say otherwise.
Fact is: dynamic typing is all about making fewer claims in your code about what you expect about the world around you. With dynamic types, to load a property you might just have to say the property name and receiver. With static types, you usually also have to say the type of all other properties of the receiver (usually by calling out the receiver’s nominal type). Hence as systems experience evolution, the probability that the dynamic property lookup will fail due to something changing is lower than the probability of the static lookup failing.
The heading “you can’t process what you don’t know” is particularly confused. You totally can and dynamic typing is all about doing that. In the dynamic typing case, you can process “o.f” without knowing the type of “o.g” or even the full type of “o.f” (only have to know about the type of o.f enough to know what you can do to it). Static type systems will typically require you to state the full type of o. So, this is an example of dynamic types being a tool that enables you to process what you don’t know.
This is not the case for languages with support for structural typing (as the article mentions in the appendix), and most modern statically typed languages have some degree of support for abstract interfaces of some sort which also support writing functions with only partially known information about the type.
I think one of the core insights in the article is that your code will always make at least some assumptions about what it is processing (unless you're implementing the identity function, or a function which does not inspect its argument at all), and these assumptions are your type. So if you expect "o" to have a field called "f", and this field should return something on which a "+" operator is defined, then these properties form your type (in structural typing this is easy and boilerplate-free to express, with interfaces there's some boilerplate but it's definitely expressible).
In that light, the difference between static and dynamic typing isn't how many assumptions you make in your code, but rather how explicit you are about them, and to what extent you make your assumptions amenable to automated reasoning.
An example of dynamic typing being used pervasively in what we commonly call statically typed languages is the downcast. (SubType)superTypeObject is a dynamic typing construct. It is saying "defer unification of these types until runtime," because there is insufficient information at compilation type to determine the real type of superTypeObject.
Of course, such downcasts are discouraged in statically typed languages without explicitly checking the type of superTypeObject before performing the downcast, but not all type systems are capable of asserting these checks are all in place at compile time. Some statically typed languages don't even have a downcast.
You can be completely explicit about checking types before using them in a dynamically typed language, and have the proper error handling in place in the case that the type unification you're expecting doesn't happen.
This fits in a larger point that, in the end, the technical qualities of a language in many ways matter less than the culture surrounding the language. Even Haskell has unsafePerformIO which means that none of its guarantees about referential transparency actually hold, in theory. In practice, the culture of the language ensures that, when you pull in a library, you can be pretty sure that it's not riddled with unsafePerformIO, and you can almost always treat code as if referential transparency is guaranteed.
A language may facilitate certain habits and discourage other habits. I feel that statically typed languages do not force me to be explicit about my assumptions, but they certainly encourage it by providing immediate benefits to doing so (automated reasoning), and through the culture that surrounds these languages.
Example:
var o = ...; // Value comes from somewhere, doesn’t matter where so long as it’s opaque
if (p)
... = o.f
else
... = o.g
Structural typing or abstract base classes or whatever would only save you here if you were very careful about giving o some top type and then casting. But that’s more work - so the tendency is that the static types version of this program will assert that o has both f and g at the point of assignment. And that represents a tighter coupling to whatever produces o.
The way I understand it, a part of the issue is about possibly deferring the time at which the type of data is known to the time at which the data is operated upon, since calling a numeric addition function on not-numbers, e.g. strings, is a type violation, no matter which programming language you are writing in. The question is where you want your parsing-or-validating to occur, since this decision makes piece of the software either more tightly coupled or more heterogenous in which kinds of data they accept. The author makes and proves a claim that this decision, which is naturally postponable in JS due to its highly dynamic and schemaless-by-default object nature, is similarly postponable in Haskell.
The other part about ignoring unknown keywords is very simple and understandable to me - you can indeed allow a statically typed program to ignore unknown schema keywords as you can allow a dynamically typed one to error on them.
To learn more, Google for “Haskell row polymorphism”.
The author correctly points out that structural vs nominal is a separate argument from static vs dynamic.
But, if we agree on this definition then is it not an admittance that "dynamic type systems" don't actually exist and instead we are simply talking about evaluation/validation being programatically specified by the programmer instead of embedded evaluation/validation by the compiler and/or runtime? And since it is being specified by the programmer, then we run into the possibility of that validation being incorrectly implemented or possibly forgotten entirely.
Any type system that had better verification of self-programmed type validation code from the programmer would solve this issue, no?
One definition of a "dynamic type system" that I am aware of is that there is runtime-existent information about types of particular pieces of data - or, somewhat equivalently, that types are information associated with values, not variables. Therefore, one could imply that e.g. Java has a dynamic type system.
The way I understand the question you're asking is: if a language has an "eval" function that accepts arbitrary code as input, what prevents it from having static-type-system-class parsing and type safety guarantees as a part of its functioning? It essentially means that the compiler for a language must both be permanently present in memory (like for Javascript, or Lisp, or Smalltalk) and it must implement the static type checks for all code that it parses (like for Haskell).
I think that these two requirements are orthogonal to each other and therefore they don't really clash with each other. Either there will be languages which implement both of these paradigms at the same time, or there already are such languages, and I am not yet aware of their existence.
It's really hard to express but I do have a nagging feeling that something has been lost that other commentators haven't quite put into words either. You just write different code in dynamic languages - even ignoring type declarations. And in many cases it feels like better, more humane code.
One piece of evidence for this elusive difference is my observation that API's in Python tend to much nicer and much less verbose (again - ignoring the obvious differences based directly on type declarations). APIs tend to feel like they were designed for usability rather than mapping directly on to library code and user be damned.
Is this a cultural difference or does something about static typing lead to different patterns of thought?
I trust you don’t mean Python’s stdlib APIs, which are an inconsistent mess. (Python 3 did very little to improve this, unfortunately.)
There’s also a lot to be said for only having to annotate interfaces once and once only, and have that information reliably applied at compile/run time (depending on language) and across all documentation and tooling too. Docstring schemes are the pits (though most typed languages are little/no better than untyped ones here).
The only thing is that rdbms push to create a static modeling of the FINAL STORAGE that is close to be the ideal of it. But anyway, you can create/delete/change tables as you wish (is not impossible to see dbs withs 100/200 tables), and SQL in fact build on the fly relations with the schema you want (SELECT field, field....).
Where is truly weak is that not extend the relational model to INNER values (so you can't "SELECT (SELECT chars FROM name)) but is a limitation of sql, not the relational model.
BTW, I think the relational model is very close to the ideal here? is nominal, is structural, you can re-model data AND types(relations), can have reflection and still see with clarity all the types you have use. What else it need to be useful??.
True, but fortunately most database systems have proprietary ways to achieve some of that. For instance in PostgreSQL
select * from regexp_split_to_table('abc', '') chars;
chars
-------
a
b
c
Is that actually true in Java? It seems to me that the way that you'd implement that load() method is by using generics to inspect the class you were passed, figuring out what data it wants in what slot, and pulling that data in from the input. You could hold on to the input and return a dynamic proxy, and you would be able to see when someone calls a getFoo() on that proxy, but then you wouldn't know what the type of the foo it expects is. And I don't know whether you could even make your proxy assignable to T.
And kotlin even includes a key word to say: if cast does not work, just return null.
And that's fine! 'Modeling the world' is a grandiose philosophical kind of activity and usually not something you need to do when you develop software.
TypeScript gives you the benefit of statically typed languages with the benefit of dynamic typed languages, in the sense that you type only what you decide to type, you don't have to type everything from the beginning, if you want to test something fast just stick and any type or simply ignore TypeScript errors and come to fix the errors later.
Dynamic features are also necessary, for example Rust lacks of a decent ORM, there is Diesel that is implemented with macros and breaks every time, plus is not a real ORM but rather a layer on SQL syntax, doesn't automate nothing.
Also compilation time has to be considered. Rust is so slow to compile, especially when you start to have 200 dependencies, with some that include a lot of macros. That means that testing is so much slower. With dynamic languages you can even have hot reloading of your code.
I'm not saying that statically typed languages are stupid, there are situation where they make a lot of sense, for embedded or system programming for example I would never use node, and surely Rust will have a future in these contexts.
But the point is that you should use the most appropriate tool for the job, and a dynamic language is in a lot of contexts the appropriate tool.
I think this is the problem rather than static typing or rust.
Can you tell me what do you want your ORM to do?
If they decided to write an API in rust just because, chances are it's not anything important (I hope). From their post, it seems like lack of familiarity is the core issue.
The reasons for this movement escape me. We already have many good options for backend web development. None of Rust's unique strengths offer any advantages for it. Focus on web has diverted effort from areas where Rust could really make a difference, like embedded, drivers, and desktop.
The best i can come up with is that a lot of people have come into Rust from other languages where web development is a big deal (eg Ruby), and it's just impossible for them to imagine that a language could be good and successful without winning at web development.
Or something like prisma - https://github.com/prisma/prisma2
The contrary, on dynamic typing language nested object as well as array can easily be parsed natively and be used immediately.
There is nothing stopping you from operating on arbitrary JSON in Haskell.
Literally nothing.
All of this was demonstrated in the article.
But flow/ts is major step towards practical solution, it covers something like 65% of properly typed language (properly = algebra on types, structural+nominal typing, opaque types, nullability exposed at type level, aggressive inferrence etc.)
The swipe at Rich Hickey at the beginning is ill-considered, however. This is the sort of use case that clojure.spec is designed for, and it can, and does, handle validation at an equivalent level of detail.
You can watch him building his speaking career on the emotional appeal of specifying the types of your payloads here: https://vimeo.com/195711510
I would prefer to say that Rich Hickey has built a dynamic programming language which includes a powerful typing system and that he's largely responsible for its design.
It's difficult to reconcile those two statements.
[1] https://github.com/manifold-systems/manifold [2] https://github.com/manifold-systems/manifold/tree/master/man...
Ruby is also moving in the same direction, as far as I know.
I’m speaking of the recent move to deprecate user agent strings, and the pushing of “feature detection”.
It’s just human nature in the end. We’re not computer. We will never use a static spec to its full potential; we’ll break a type system wide open the moment we get to our limit of tolerance for not getting the job done.
We need type inference more. The computer has built the AST, why do compliers seem so incapable of traversing that tree and finding the type errors for us?
Maybe clients should declare their own types containing just what they need and copy the data into them from the protobufs? But this does get tedious. On the other hand, in a schemaless JSON system, there is nothing statically checking that the clients and servers have compatible ideas of what a message should contain.
How’s it different from the proposed model where you start by parsing the data you receive and, once it’s parsed and know it’s good, you process it?
I don't know if there's a supported way to do this, though. To leverage it for refactoring, there would also need to be a way to do a query to find out out which clients use which fields.
Given a set of reasonable requirements I think pretty much no one would claim a general-purpose language couldn’t satisfy them without too much trouble. In fact, that might be a fair definition of a general-purpose language.
I’m fine with strong and expressive static type-checking, but you need to hold the main limitation in mind as you use it in a distributed environment: the guarantees are static. They pertain only to your little binary and don’t say anything about the rest of the system.
People can tend to make the mistake of assuming other components in the system will continue to behave as they do on the day their own component was compiled.
Versioning is hard, because it's a coordination problem, but it's not the type system that produces the pain.
the actual critique of the first post wasn't really that Haskell can't do it in a literal sense, but that ignoring or reasoning about unknowns diminishes the advantages of static typing.
Sure, you can define an "unknown" type if you want and make your static language as permissive as possible, but then you lose the actual static guarantees, which is automating reasoning about the correctness and capacities of your program at compile time.
The question then is if you're already conceding that there are so many unknowns which better ought to be dealt with at runtime, what is there to be gained from making that explicit in your program other than just having to write more code?
Ignoring the unknowns that are unnecessary to solve the problem at hand, is literally the essence of software abstraction. Why would you want to do more work than is necessary to solve a given problem?
> you can define an "unknown" type if you want and make your static language as permissive as possible
And 'unknown' type doesn't make the language permissive. Since the type is 'unknown' it doesn't permit any operations at at all on it. Hence, the opposite of permissive.
> you lose the actual static guarantees, which is automating reasoning about the correctness and capacities of your program at compile time.
You absolutely don't lose the actual static guarantees which are actually relevant to solving the problem your program wants to solve. If your program's job is to add a signature field to a JSON object, why would you want to parse and decode the entire JSON object into a strongly-typed value? You would just parse it into a reasonable Map data structure and add the signature as a key-value pair to the Map.
> you're already conceding that there are so many unknowns which better ought to be dealt with at runtime
That's exactly what we're not doing here, we're creating software abstractions which again, is an essential part of software development. Please see Liskov & Zilles, 'Programming with Abstract Data Types', 1974.
> what is there to be gained from making that explicit in your program
What you always gain from static typing–exposing the assumptions and invariants of your code as first-class parts of the code, making it easy for readers to understand at a glance what they are, making it easy to change the code with compiler assistance to ensure the invariants are honoured.
This is essentially what I was getting it. To me the static typing seems to be almost more about naming things that it is about verifying the correctness of your program in the face of unknown or interesting behaviour.
And there is a very obvious cost to this because not all code is 'your code'. That's the problem with a coupling that is mentioned in the first part of the article but not really addressed. With typing, it is very easily possible for someone to create bad abstractions that you have no control over, you simply inherit them. It breaks with the principle of leaving interpretation to the receiver of data who encapsulates it.
And this is a very practical problem in real static code, because people create bad abstractions all the time, so the type system rather than just making valuable claims about what we know produces all sort of entanglements you have no control over.
Here is where the dynamic and static typing distinction crosses over into the OO debate. Alan Kay pointed out that the 'late-binding of all things' is one of the key principles of object oriented programming. Static typing interferes with this in very strong ways by allowing developers to impose meaning on your program way too early.
That's exactly backwards. The point is not naming things, the point is encoding behaviours and invariants in the type system so the compiler can help you check them.
> With typing, it is very easily possible for someone to create bad abstractions that you have no control over
It's possible for programs to be written badly in any typing discipline, static or dynamic. Neither saves you from the bad decisions of others. I've personally seen PHP code that no one could understand and everyone was afraid of touching because it heavily used reflection. I've heard of this for Ruby and Objective-C code too.
This improves reliability and minimizes the scope of changes needed for the system to continue to work when something changes. This is particularly important in distributed system, where you can’t generally update the system coherently and instead need/want to update it piece-meal or progressively.
Strong type systems tend to encourage you to specify strong constraints on the typed values. While you’re specifying your types you need to be careful to not over specify, making assertions you don’t need to make, ending up with a brittle system what will break unnecessarily.
There are nice advantages to strong expressive types, but the advantages are all within the local component and it takes some extra care to avoid imposing inflexibility on the system.
To argue that a static type system is not valuable because it doesn't enforce constraints on other external systems it doesn't know about is a pretty wild case of moving the goalposts.
Does the library code really need to use 16-bit floating-point values, or does it only use them because someone twenty years ago believed in some superstitions about performance? That information isn't available. It isn't in the type system, so it can only be in the documentation... oh, wait, documentation focuses on How and not Why, doesn't it? Your static type system was made by people who failed to disambiguate between storage size specifications and semantics, so you're left with "16-bit IEEE floating point" as the only semantic information you're ever going to have.
I didn’t.
When a language restricts the usage of things by the type of thing being used, it restricts the set if behaviours that can be expressed in that language.
You can get around this by adding more rules to specify the behaviours needed. (Boilerplate?)
In this way, a dynamic language permits more behaviours with less rules. It is more “expressive”.
This can be good and bad, some of those behaviours are probably unwanted!
And this is just a theory.
https://www.reddit.com/r/programming/comments/eqv6yd/no_dyna...
King (the author) places "dynamically typed" and "statically typed" in opposition. But keep in mind that many languages have both: Java, ObjC, TypeScript, C#, etc. I like to say that a a language "has" static and/or dynamic types, but "is" dynamic if it supports runtime features like reflection - of course this is a sliding scale.
King observes that static types allow you to make explicit what you know. After calling `pickle.load` you don't know anything about the result, so its static type is going to be something quite constraining like `String -> Object`. It seems we are in violent agreement on this point.
King then goes on to make a different claim: that it is possible to implement `pickle.load` in Java and also in Haskell. It is possible in Java but not in Haskell.
Here's the key line for Java:
However, nothing is stopping you from passing Serializable.class and branching on the type later
Notice the subtle shift in meaning for "type": from static type to runtime tag. It is possible to branch on the type at runtime, because the type is available at runtime, because Java has dynamic types. They're awkward and painful to use, but it is possible.
For Haskell:
Can we do this in Haskell, too? Absolutely—we can use the serialise library, which has a similar API to the Java one mentioned above.
Absolutely you cannot! The Serialise libary requires you to list all of the possible result types up-front, "by providing a set of type class instances." There is no way for a Haskell program to deserialise a value whose static type was not visible when the program was compiled. There is no way in Haskell to "get a list of all types" (it's hard to even formulate this).
Implementing Python-style pickle isn't really about types, it's about the language's dynamic features. Can you look up a types by name, reflect on a value at runtime? Dynamic features really do bring new capabilities to programs.
The difference to Java has nothing to do with reflection, really, but rather with a uniform object representation (in Java you know the shape of all values by default).
A Java pickle.load would need to lean heavily on its dynamic features including reflection. For example, looking up a class by name.
https://hackage.haskell.org/package/base-4.12.0.0/docs/Type-...
If that's to complicated, just create an ADT of all the python values and translate Pickle's implementation directly.
I clearly do not understand the overwhelmingly dedication type system proponent have against dynamic languages, particularly as evidenced by the previous comments in this thread. I would note that it seems to be the same, but reversed, for proponents of dynamic languages. Other than two or three mentions of Rust, all the examples and discussions have been about primarily interpreted or JIT languages with extensive runtimes. So there is little argument that these type systems are saving users (and I mean developers) from “memory safety” bugs or potential vulnerability exposing errors (those would tend to be problems with the interpreter/runtime implementation).
Maybe I’m missing something, but if we are talking about managed language runtimes and, again based on the languages dominating the discussion, are nearly universally garbage collected, who cares what, if any, type system is in use for a given program?
I don’t know for certain (I don’t do any web based work) but I can’t recall ever reading about using typescript to boost speed or memory efficiency over vanilla JS. There is some performance benefit to say compiled Haskell vs interpreted Python, but that is apples and oranges, but based on a limited amount of googling, it looks like Clojure and Haskell are reasonably close for performance concerns.
Also, most of the type systems being discussed are complex and high level, so where does C and C++ fit into this topic? They are statically typed languages (I am aware the type systems used are fundamentally weaker than those of HM type systems) but no one seems to be arguing that they are good examples of why static typing is beneficial. Rust, while a more typical functional programming style type system, is still not really being discussed. I know that the article doesn’t address these areas or languages, but for those advocating so strongly for types, why no present something other than technical debt, easier reading, and organizational benefits. For dynamic proponents, why not address the lack of user visible benefits, i.e. no real performance win in common usage scenarios, the lack of assistance weaker type systems give to protect from differing types of errors, etc.
All I can tell is that some people like types and some people don’t. And most of the discussion seems to center on your standard CRUD app, web based applications, does it even matter?
I agree that there are more reasons than performance to advocate static typing, I just don’t understand why that would not be a point of advocacy in a discussion about the pros and cons of typing systems in general.
1. Author attacks premise of dynamic type systems argument.
2. Author presents premise for static type system (which is practically confluent/equivalent/equifinal to premise he just undermined).
>static type systems allow specifying exactly how much a component needs to know about the structure of its inputs, and conversely, how much it doesn’t. Indeed, in practice static type systems excel at processing data with only a partially-known structure, as they can be used to ensure application logic doesn’t accidentally assume too much.
Chances are you are wrong about 'how much you need to know' irrespective of your type system. Nobody gets it right the first time.
When we figure out that we were wrong about how much we need to know about the structure of our inputs (e.g we assumed too little) we do this thing we call... "extending our code" [1].
The question then is simply: which type-system is better at extensibility?
And I have no idea how to define "better".
1. HN commenter misses the point of the article.
2. HN commenter even misgenders the article's author.
The real difference is that dynamic type systems don't pretend to. Static type systems have a way of putting developers at ease on auto-pilot. Arguments which compare dynamic type systems with static type systems should be more focused on reality rather than hypothetical, idealized use cases where the developer is a completely rational agent who understands everything about the project's direction and strategy. The reality is that the vast majority of developers can't design software properly; they can't even select the best data structure to solve the simplest problems and they over-engineer and can't create good abstractions that make sense and aid the project's evolution. Most developers don't know what a good abstraction looks like because they don't have a long term vision for the product that they're working on.
All these safety features which static typing supposedly introduces don't actually protect the project's code from the real threat which is poor design at an architectural level. I would even argue that dynamic typing can encourage worse design because it gives developers an incentive to keep inventing strange abstractions/types that don't correspond to the high level picture of what the software actually does... Most statically typed projects I've seen tend to be full of weird and unnecessary abstractions like: 'Interactor', 'Builder', 'PrimaryAdapter'... these kinds of abstractions do not bring the code any closer to alignment with the end user's perspective of the software (which should be the primary goal of any abstraction), instead, they impose constraints on developers working on the project... but as requirements change, these constraints have a way of becoming redundant which is why sometimes large amount of logic needs to be re-written.
Static typing encourages short term development strategies centered around constraining developers from doing certain things based on speculative and often completely arbitrary concepts that the lead developer felt in their gut was important. Maybe if the abstractions were designed around some long-term vision of the evolution of the project, but this is almost never the case (and I've worked on many different projects, for many different companies for over a decade), most of the time, abstractions and the constraints that they impose are in fact based on nothing but arbitrary technical decisions that may as well have been the result of a coin toss.
Developers should have an incentive to create fewer (and only necessary) abstractions, not more. By forcing developers to rely on their memory instead of their IDE to figure out which variables hold what kinds of objects, there is a strong incentive for them to keep abstractions as simple an non-confusing as possible.
Any tool which makes some aspect of life easier for the user will invariably make the user lazier and complacent in that domain. Abstractions are not something one should be complacent about, they're very difficult to get right.
I meant static typing... By making it easy to keep track of interfaces/types, it creates incentives to create more different kinds of abstractions.
The point of the article is basically "dynamic type systems are not inherently more open because we can just ignore type errors in static type languages [which means, of course, that we're making them behave like dynamic languages]"... Well, shoot.
Ultimately, this seems like her previous article was just contributing to that six-decade-old flamewar. Since this is a flamewar, it got comments disagreeing, and now she posted an article disagreeing with the disagreements.
Everything worked as expected and nothing that hasn't been said before (over and over) was said.
Why can't people just be ok with "I like this paradigm and it's ok if you like another"? Sure, the discussion has led to plenty of advances in programming language design, but at this point it's pretty clear that, if it were possible to absolutely prove that one type system is better than another, we would have done so already. Meaning that everything pretty much comes down to opinion.