- 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.
After giving it enough time and rereading, I feel I have a better understanding. The crux IMO is here:
> 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
Now for the flip side. IMO the post also contains "enough rope" to hang static typing with. The picture that emerges is that programming in a statically typed language, as the author conceives it, consists of separate phases of "data modelling" (making assumptions about the external world, and at each module/function level about the inputs and outputs), and writing code. Often the former is the hard part to get clear, and this explains the phenomenon familiar to programmers in a statically typed language like Haskell, that once you get the types exactly right, the code basically writes itself: the types guide you towards the right code, like gravity.
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.
I thought the article was good and addressed a real point of confusion, as evidenced by
the two included comments (from Reddit and HN). You can consume arbitrary data using
a program written in a statically typed or dynamically typed language. Whether it's decoupled
from changes in the data depends on how the code is written and the data model, which
have nothing to do with static vs dynamic typing.
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?
I think it's a question of efficacy and productivity. People routinely make mistakes using type systems. While static typing tends to be really good at solving problems it itself introduces (change a type and, wow! My IDE knows where that type is everywhere and can change it for me! Nevermind that only the producer and final receiver should care, it's everywhere now...)
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.
> 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.
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].
Well what I should have said is there has been a lot of studies on the efficacy of type systems, but much has been shown to be flawed. I haven't looked at your citations mostly because of the use of typescript which I have personal experience with and I know it's not helping. I'm not going to debate this with you, though; too little good papers on the topic so too much heat and too little light. I've spent most of my career using static typed languages in hindsight I've found most of the static typing not helpful for successful projects.
> 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?
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)?”
No! The "default state" for not knowing anything at compile time about the values your data will take is typelessness, exemplified by machine-oriented languages like BCPL and most assembly languages. In this state, the machine knows nothing about the types of your values at any time. Each operation that you apply to a value just assumes that it has the right type for that operation.
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.
Hence ORMs. It's possible to do much better than ORMs though. The object/relational type system mismatch is a property of how technology evolved, it's not fundamental.
> You can consume arbitrary data using a program written in a statically typed or dynamically typed language.
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?
I believe that such system cannot fully process the data, as is written in that data's specification, without providing the type system that is in that specification.
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.
I'm quite sure it's not. Statically-typed programs can recursively parse data, and they can also monadically (sequentially) parse data. The same is true of dynamically-typed programs.
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.
I don’t get it. Why are you concerned with 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.
The situation is not written entirely with static types if the run-time processing requires the expression of dynamic typing. That's based on some actual dynamic typing from the language, or else some ad hoc dynamic types cobbed together in the program itself.
That first one looks dynamically typed through a List * type, and tags put into pointers. That algebraic type in Haskell also looks dynamic: an Expr can be any one of four things.
This supports the case the article was making. Clearly the type system in Haskell doesn't prevent it from handling arbitrary data - it's hard to imagine a program more open to change in the input data than a Lisp interpreter.
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'.
Well, just one rule: if we are looking at type tags at run-time, it's dynamic typing! Whether that be things put into C pointers, or integer fields discriminating unions, or algebraic sum types with pattern matching.
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?
I think there's a perhaps irreconcilable disconnect between 2 camps here, but I also think that's ok and different people are allowed to like different things.
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.
Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can be expressed by Haskell's type system: i.e. they can succinctly express more about the "entire code" than Haskell's types. Types are not the only way to write formal assertions and assumptions about code. The difference between the two is in the level of sound inference that can be made (stronger with types) and the strength and expressivity of the assertions (stronger with contracts).
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.
Techniques like Ghost of Departed Proofs are the most exciting thing to me as a casual correctness enthusiast. It acts as a means of combining static types with contracts.
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.
Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure).
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
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.
That's an interesting angle. Another way of saying it might be that GoDP on the face of it can make one-off proofs for a value. Proofs for a function requires making proofs about all possible inputs, which is where your property test comes in handy. I could have `Named a (List x -> List x -> List x)` as the function I'm proving things about.
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.
> 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
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.
> If dependent types would accept unsound proofs, the soundness of the entire type system would be compromised to the point of undefined behavior.
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
For
op : A -> A -> A
More generally you can express associativity itself with:
isAssociative : (op : a -> a -> a) -> ((x, y, z: a) -> x `op` (y `op` z) = (x `op` y) `op` z)
> If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language.
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)
There's also no reason not to define a predicate `isAssociative`.
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.
Well sure if you lie to your specs all bets are off. Buffer overflows, bounds checking, use after free (if you're in a non-GCed language), resource leakage, etc. You're always at the mercy of your runtime system as soon as you lie about your pre-runtime checks, no matter what system you use, types or otherwise.
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.
My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness
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.
> whereas the contracts we're talking about here are usually checked at run time
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.
No, they can be checked in many different ways, hence their power.
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.
> 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.
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.
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.
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.
Also, the following part isn't necessarily because of dynamic typing vs static
> 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.
Spec is at heart a data modelling system. So for example,
(s/def ::integer integer?)
is very explicitly not a definition of an "integer" type. It is preparation to model some data x and check that the data will evaluate to true if someone uses the predicate (integer? x). However, this is obviously enough to implement a type system.
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.
> 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.
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.
When spec was proposed I remember some talk of compile-time checking of some annotations. I don't know whether anything came of that, but in theory it would allow what you're talking about. That has no relation to seq, though, which is the kind of thing supported by many statically typed languages.
Your comment is spot on. But the opposite can also be true. I totally have the same issues you do at times by trying to understand types (which I feel type hinting, editors, and good variables names go a long way to help with). But I also find myself using a lot of cognitive load trying to get a correct type definition, etc (for the non simple tasks). Whether its trying to figure out how to get a certain object, because of the interfaces, factories, etc. Or trying to create a new object and trying to map things correctly. What if I just want to have a hash map full of varying object structures? (I am not saying its not possible, I am saying its a use of cognitive load)
Agreed, perhaps it's something like the difference between top-down vs bottom-up learning in teaching. People don't all use the same mental models and allowances need to exist for both groups. But I suspect this is true of most contentious topics in programming.
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
Yes. Perhaps this is an indication that we actually need automated type annotation. E.g. you initially write/prototype your program in a dynamically typed form, then you click a "magic" button, and a tool converts your program into statically typed style.
This already exists in Haskell. Firstly, Haskell has type inference so you can write entire programs without any type annotations. Second of all, since type annotations actually help to document your code, it’s recommended as good Haskell style to annotate all top-level definitions.
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).
Type inference does not automatically "typify" your code. The type system -- whether the type annotations are explicit or the types are inferred -- determines which expressions are "well-formed" (i.e. syntactically correct), and so you can't write arbitrary code. E.g., in Haskell, you can know for a fact that at one call site a Maybe instance is Just, but whether you annotate your types or rely on inference, the type system will still force you to match on the constructor even though you don't really have to from a correctness perspective.
If you're talking about the fact that you have to unbox the Maybe, that's not really related to type inference or static types but how "null" values are represented in the language.
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.
> If you're talking about exhaustiveness checks, you can disable those and use `-fdefer-type-errors` to compile programs which don't type-check.
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.
If the reason you know your Maybe T is a Just _ is that you tested it locally: in any language that favors the Maybe pattern, the idiomatic way of performing that test makes the result available to the type system (destructuring / combinators / 'nads). On the other hand, if you know your Maybe is a Just because of non-local information, you will eventually turn out to be wrong :)
No, you can know -- and even prove -- that at a certain callsite, a Maybe would be a Just, and if you were using a dependent type system, you can prove that in the type system (although it probably won't be automatically inferred -- you may have to work hard for the proof), but Haskell's type system is too weak to express such properties and such proofs, at least in the general case.
I’ve been out of the game for a number of years but I used something called ghc-mod [1] with its associated vim plugin [2] to get this functionality. Moving forward, it seems that all of the effort has moved over to Haskell IDE Engine [3]. It looks like this exact feature hasn’t been brought over yet but it is planned. In the mean time you could still use ghc-mod though.
Thanks for the tip! Haskell IDE engine is exactly what I've been using til now and would've been very pleased to find out it had such a convenient feature.
Ghcide is on my list to try next as it's gotten a lot of attention lately.
Yes, it already has a code command to automatically add top level type annotations. The caveat I that it can only work if you add -Wall to your compilations flags.
I'm curious why you quote this like it's a fact when it's an opinion. The understanding of type inference used as the basis for making the argument in that blog post is superficial. Type inference doesn't just allow you to leave off type information from variables. A good inference engine will infer the most generic type for variables (and functions!), it's a discovery that you can query the compiler for in order to do type driven development.
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.
If type inference damaged readability, we would expect companies/projects that use languages such as OCaml and Haskell where type inference is possible but not mandatory to have policies against it in their style guides. In my experience with OCaml, the widely agreed on style is to only annotate types of functions that are part of some public interface (although since this annotation is necessary to define the public interface of a library, it's not even necessarily true that type inference impairing readability is the primary reason for this).
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.
Companies do have policies against using type inference (e.g., the use of var in C#).
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.
> Companies do have policies against using type inference (e.g., the use of var in C#).
That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?
Yes! Any company that has adopted MyPy or TypeScript often have policies for this. One team I spoke to at Facebook said that any new code should have type annotations. I believe Dropbox had a nice blog post about new code should have type annotations too. It is hard to get these details from companies/teams (and be allowed to talk about it).
That's because (a) these are not historically type-inferred languages–runtime typechecking doesn't count as type inference–and (b) the gradual typechecking approaches like Mypy and TypeScript often have a lot of type inference issues which force people to try to overcome them with manual annotations.
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.
Do they mandate that only function types (and any ambiguous ones) should be annotated, or that all types (i.e. including those of local variables which mypy can infer) should be? I strongly suspect the former, which implies that they view type annotations more as a necessary evil to allow type checking rather than a benefit in their own right. After all, there was nothing stopping people putting "type annotations" in Python 2.5 code if you wanted, by writing `x = get_thing_count() # int`. But AFAIK no-one did that until annotations could actually be used to check type safety.
Typescript will infer the 'any' type by default in a lot of cases, that's the reason teams will mandate type annotations. It's really just not the same thing. These are bolt on type systems to dynamic languages where if you fail to put a type annotation you're actually losing information. That's not the case in Haskell, type inference causes no loss of precision for types.
I don’t agree with readibility (there are pros and cons, ie. terser code vs. implicit types) but, at least in Haskell, it improves usability by inferring the most generic type to your expression.
Agree on what? "Type inference" is a broad feature, feel free to post the resources.
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.
In practice, not really. A good type inference system like Hindley-Milner infers the most general type of any expression you give it. This usually makes your code more polymorphic i.e. generic than if you would have manually written down the types.
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?
Yes, some programming languages take this approach but I don't think that prototyping is as easy in such languages as it is in a dynamically typed language (e.g. Haskell vs Python).
Productivity can be really subjective. Those that are used to modeling the problem domain with the type system find that their most productive approach, even with prototyping.
Right, and the type system is such a big help in refactoring - especially in small projects - that you don't have to be all that right in your first N cuts at the model. You can write code and find out where you're wrong, and fix it fast.
It’s even more help in larger projects :) The dividends of type-checher aid refactoring really start paying off once the project is above a a certain size/age.
Yeah, I think I was unclear. Given a need to refactor, it's a bigger help on a bigger refactor.
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.
What would be neat is if you could take a Python program and run type inference on the program and it would output a type annotated version of the code.
Unless your type system is very weak -- and in effect, an untyped language can be considered to already be doing what you said only in a type system that has a single type -- this is generally impossible (halting problem and its extensions). So you have the choice of something that's not very useful or something that's impossible -- take your pick.
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.
TypeScript can come close to this, especially with the latest release with Assertion support. You make assertions about your code, and the downstream types are inferred based on your assertions. Thus, the runtime behavior of your code gives you progressively enhanced type-checking. If you do these assertions at the borders, your "correctness" is dependent on the strength of your runtime assertions.
> 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
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.
If you don't have to think about what mutation each method performs, if any, when switching to static typing, you're not just switching to static typing.
I've come to the conclusion that the benefit dynamic typing brings to the table is to allow more technical debt. Now of course technical debt should be repaid at an appropriate moment but that appropriate moment isn't always "as soon as possible". Let me illustrate, say you're adding a new feature and create lots of bugs in the process. Static typing will force you to fix some of these bugs before you can test out the feature. Then while testing out the feature you decide that it was a bad idea after all or that the feature should be implemented completely differently. So you scrap the implementation. In this case fixing those bugs was a waste of time. Dynamic typing allows you to postpone fixing those bugs after you're more certain that the feature and its implementation will stay.
It isn’t even a benefit, really. Statically typed languages don’t force you to model things with types; you’re completely free to use strings and doubles everywhere and take on all the technical debt you want.
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.
It’s true that with static typing, you are usually forced to propagate your changes to “your whole codebase” to get it compiling before you can run any of it. That stinks. However, it turns out you can lift this restriction in static languages, and this is what Unison does:
I haven't given Unison a try so I won't dismiss it outright but to me having to explicitly propagate your change to your entire codebase before you can run anything doesn't suck at all, it's actually the killer feature of statically typed languages.
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’d read through the link and see what you think, but TL;DR is that you can still propagate a change everywhere in Unison (and Unison tracks this for you), but even if you’ve partially propagated, you can run all the code that you’ve upgraded so far. So if a change has 500 transitive dependents and you upgrade 7 of them, you can run those 7 (and this might help you figure out that you want to do the change a bit differently) Whereas you’d typically need to upgrade “the whole codebase” before being able to run anything, including code unrelated to the change being made.
Surely if the code was unrelated then you wouldn’t have to change it? It might be tangentially related to the change at hand but the fact it breaks means it must be given consideration and not just as a “geez I have to update all these cases” but also in terms of how the change impacts them.
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.
The idea is that you wouldn't need large refactorings in more dynamic languages in the first place since you are operating on a different abstraction level.
In the JS based project i recently joined (previously i was writing C# ), what i notice is that in a team of 6 people 4 are doing refactorings every sprint for the past 8 months.
This is talking about the case where you're just testing something out – prototyping it for a few branches before implementing it for the whole thing. In this case, _you_ are your own user, so it doesn't matter if you see the type errors.
If I’m making a potentially wide-reaching change, I’d want to test it against everything else so I know for sure that it’s actually viable in the context of every instance of its use.
Also, some statically-typed languages (like Haskell) allow you to defer type errors to runtime if you really want.
Thanks for pointing me to Unison, I have yet to dig into the details, but its core idea is something I've been thinking about lately and it's fantastic to see that it exists!
To be fair most of the time that type change propagation is just manual work guided by the compiler. Some smart IDE would even be able to make the changes for you.
Yep. Being able to work fast and dirty is a huge boon when testing ideas and figuring out the initial design, and it is deeply annoying that so many typed languages refuse to permit this. The faster you can write code, the faster you can throw it away again; and arriving at good code almost invariably requires† writing lots of bad code first. If writing bad code is made expensive (another example of Premature Optimization), authors may be reluctant to try different ideas or throw anything away.
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.
This is why TypeScript is so popular. JavaScript is very loose, but you can progressively enhance it using TypeScript with stricter and stricter types, many of which can be inferred, and since 3.7 can be derived by runtime assertions, and the strictness of which can be controlled with compiler flags.
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.
If you think it helps to quickly write some code without types (I don't really agree with that in general, maybe in some specific cases), but you want to, when you're happy with the design, just add the types, there are many languages that support that!
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)
Yeah, it’s not a new idea; but I’d say “some” languages rather than “many”. Dylan’s another case; great pity it didn’t fare better. (I’d much rather be using it than Swift.)
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.)
let mut s = Vec::new();
s.push(Pair::new("a", 1));
s.push(Pair::new("b", 2));
s.push(Pair::new("c", 3));
Both are statically typed, but one uses inference. It practically feels like Python everywhere except where type declarations matter most to me -- function signatures:
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].
TBH, I think that’s as much accidental as by design. ObjC didn’t do generics until just recently, so the standard collection classes (NSArray, NSDictionary, etc) couldn’t specify element types so had no choice but to leave those APIs typed as `id` (effectively `void`).
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.)
One point based on my observation. Programmers coming from languages with good type system seems to have low probability of being a glueman. While good type system doesn't need to have static typing, in general they tend to have a way to explicitly declare things when you need to.
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.)
It's not so much allowing debt, it's that the barrier to entry is extremely low. You can hack around and get a feature "working" without having a great understanding of what you're actually doing.
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!).
The trade-off is that the bugs flagged by static type checking are usually quick to fix (eg: function expected an int but was passed a float). With dynamic typing, the subtle bug that arises from the function unexpectedly truncating your float could take an hour to track down and outweigh any time saved from dynamic typing. This applies even when trying out new experimental features.
Depends on the language. I do agree that lossy coercions are a Bad Idea; a [mis]feature added with the best of intentions and inadequate forethought (e.g. AppleScript, JavaScript, PHP).
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.)
You're supposed to have written a test that catches that bug. Which of course also takes more time and effort than simply using a type checker in the compiler of a typed language..
Static types enforced by a compiler catch more bugs in logic that can be encoded in the type system at build time. How costly are these bugs? It probably depends on context. For a business app/SaaS, is the compiler going to prevent your broken business rules from allowing -100 items to be added to a basket, crediting the "buyer"? I would say a developer who knows how to interpret requirements is more important here. On the other hand, a compiler is probably an amazing place for static types, but I don't write compilers and I'd wager most jobbing devs don't either.
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.
To reinforce your point: static typing doesn't just force you to fix some bugs earlier, but it also forces you to spend more time doing design upfront, often when you still don't have clear specs. That can be a big drag when you need to do a lot of experimentation/iteration.
But you don't need to have a final design straight from the beginning. You can start with only what you need right now and evolve the types/schema over time.
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.
Interesting, I would have said static typing allows more technical debt. Illustrating example: Lets say you pass a double variable from some part of your code through 13 layers of APIs until it is actually looked at and acted upon. Now you realise that you not only need a double, but also a boolean. In dynamic typing, you can make a tuple containing both and only modifying the beginning and end points. In static typing you have to alter/refactor the type everywhere.
It’s often considered bad practice to pass around raw values for that very reason. Introduce a (minimal) abstraction, that is, give the thing you’re passing through those layers a name. Then you can change the endpoints at will and still get static checking (as a plus, you can‘t accidentally pass the wrong bool, or mix up the tuple order).
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.)
You'd love Perl. Just pass @_ through your callstack. Want a new value available 20 functions deep that is available at the top? Just toss it in @_ at the top and you are done.
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.
And on layer 10 you missed that you were using and treating the argument as if it were the double. Now you have a bug that the type system would have solved. Or you can alias that input early if you know with a good certainty it has possiblity to change, and now you just update the alias and everything gets checked all the way down without a refractor.
I think at that point you probably need a major refactor, regardless of the language being used. While I don't want to be in that situation, I'll typically use a helper class if I'm forced to pass something through 13 layers (a class containing all the arguments).
However, that's pretty much the textbook example for designing with dependency injection in mind. Static typing won't fix a terrible architecture.
I haven't read that textbook. Do you have a good reference. I may have been intentionally been using an anti pattern. I often have a POD class that gets passed down a processing chain.
YMMV. There's probably at least one good use case for virtually every design. What you're doing could be totally reasonable.
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.
I'm keeping that line. More wrong places... That is koan worthy. What is DI dynamic initialization? I can't imagine passing a const bit of POD through 13 layers without it bein used, but not every layer uses all of it probably.
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.
> Lets say you pass a double variable from some part of your code through 13 layers of APIs until it is actually looked at and acted upon. Now you realise that you not only need a double, but also a boolean. In dynamic typing, you can make a tuple containing both and only modifying the beginning and end points. In static typing you have to alter/refactor the type everywhere.
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.
According to this, languages statically typed but offering a dynamic type (any in typescript) allow best of both world.
And using the right types is a matter of refactoring.
The hard part is not offering a "dynamic" type (which is generally just a variant type with a bunch of RuntimeType cases) but making the "static" and "dynamic" portions of the language truly, tightly interoperable. Generally, this implies that the compiler and runtime system should be able to correctly assign "blame" to some dynamic part of the program for a runtime type error that impacts "static" code, and this can be quite non-trivial in some cases.
I agree, and I think that's one of the reasons TypeScript works so well, and why it's a shame that some people dismiss it beforehand because they generalise from other statically typed languages to TypeScript. Not only are you able to consciously take up some technical debt somewhere, but it's also clearly marked by the type system.
Which is entirely plausible. If all the decisions about what data should be flowing where in a program have been made there is no particular reason not to have static typing. It won't make things worse, will enforce discipline and will probably catch bugs.
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.
>If all the decisions about what data should be flowing where in a program have been made there is no particular reason not to have static typing.
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.
> - so we try to decide about just the most crucial architectural aspects and make the rest as easy to change at possible,
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.
It's called Postel's law, and it's one of the burdensome idiocies Unix programmers have saddled us with, along with text-file formats and protocols, null-terminated strings, fork(2), and the assumption that I/O is synchronous by default.
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 :)
The problem right there is in the definition of “liberal”.
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).
In Clojure you generally accept any kind of map, do some operation and return 'copy' of that map, or pass it on.
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.
But I believe this is also with the spirit of the article. Your functions still assume something about input and are polymorphic over everything else in it.
AFAIK this can also be done in a type safe manner in languages which support extensible records/row polymorphism.
Almost nobody uses Ada, though, while one of the most read programming language-related websites (lambda-the-ultimate) is written in a dynamic language. Also, in the day-to-day interactions of the real world we almost never carry out “validation”, we stop at “parsing” most of the time, otherwise almost nothing will ever be done.
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.
> 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.
> (where “holding food” is the structure a type must implement) while
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.
> 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".
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 ;).
The article demonstrated that with Haskell — as with just about any other language — you can choose to silently ignore malformed input. There is absolutely no fundamental necessity to "blow up at runtime" as the parent comment erroneously posited.
Who’s applying Postel’s Law to programming? Citation please.
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.
I have developed and maintained several large systems in both dynamic and statically typed languages.
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.
There are two aspects to maintenance. One is in maintaining a codebase, which is what you're referring to. This greatly benefits from static typing as you can have good guarantees about your code before you deploy it.
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.
> Static type systems will typically require you to state the full type of o.
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.
The difference between static and dynamic typing isn't about how explicit you are about the assumptions in your code. You can be equivalently explicit in dynamic and static languages. The fundamental difference lies in when you want the types to be verified. In static typing, that is before the program is run. In dynamic typing, that is before the code is executed if you are explicit, or when the code is executed if you are not explicit enough.
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.
Yes, you're right, it's not about how explicit you are, or even how explicit you have to be. You can write "stringly typed" code in a static language where none of your assumptions are apparent in the type system. Conversely, regardless of your typing discipline, you can be completely explicit about your assumptions just by writing comments.
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.
Structural typing doesn’t save you unless you add other stuff to it.
Example:
var o = ...; // Value comes from somewhere, doesn’t matter where so long as it’s opaque
if (p)
... = o.f
else
... = o.g
In dynamic typing, we only assert that o has f on the then, and only assert that o has g on the else.
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.
Structural static typing lets you do exactly what you claim static type systems are incapable of letting you do. It's fair to say those systems are not common--Typescript is the only one I know of--and I wonder why that is, but it's not an inherent failure of static type systems.
I think the author is offering "you can’t process what you don’t know" as an example of something that dynamic proponents claim that statically-typed languages can't do, followed by a refutation of it.
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.
The author actually argues against Haskell as an example of their philosophy, because Haskell has poor support for open static types. They generally have to be faked in unintuitive ways by relying on the typeclasses feature, and something like OCaml's support for structural, extensible records and variants seems to be entirely off limits out-of-the-box.
The whole point of row polymorphism (for both records and variants) is that it allow for implementing open types in a static typing context. And OCaml supports this out of the box whereas Haskell does not.
Yes, that’s true. I’m not disputing that. Perhaps I misinterpreted your previous comment. I think the point I want to make is that in the argument between static vs dynamic, the structural vs nominal argument is not really relevant.
I actually really enjoy your views on dynamic typing.
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.
Having moved from Python to C# I'm still coming to terms with how I feel.
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?
Unfortunately C# does not have a very nice type system compared to more modern typed languages - elm, haskell, ruby's sorbet. That is probably part of the reason you are feeling that way.
“my observation that API's in Python tend to much nicer and much less verbose”
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).
This have a mirror with the "sql"/"nosql" debate. Being "schemaless" is supposedly a great advantage of nosql, but the thing is that sql/relational is as schemaless as you want!
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??.
>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.
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;
gives you
chars
-------
a
b
c
It's called table-valued functions and it's extensible. Obviously, it's not quite as general as what you are talking about because the values are not actually stored as tables. To get a bit closer to that you could use composite types and arrays. I'm not convinced it's worth the added complexity though.
"Nitpickers will complain that this isn’t the same as pickle.load(), since you have to pass a Class<T> token to choose what type of thing you want ahead of time. However, nothing is stopping you from passing Serializable.class and branching on the type later, after the object has been loaded."
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.
Hmm, that may be true for JSON, but I think that Java binary serialization holds enough information about the original types to allow deserialization without having to explicitly pass the expected class (though what the runtime system does behind the scenes may be equivalent).
To paraphrase Churchill, “If a programmer doesn't like dynamic typing by the time he is 20, he has no enthusiasm. If he is not static typing by the time he is 30, he has not learned from experience.”
Definitely dynamic typing is not about modeling the world. And it's much broader than that. Static typing, strict or loose, also isn't about modeling the world. OO design isn't about modeling the world. These things are successful because they're effective methods for organizing code. They're about as useful for modeling the world as the Dewey Decimal System is.
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.
I don't think it makes much sense to compare between static and dynamic typing in general. Given the choice between static typing as in e.g. Java and dynamic typing in Python, I'd pick Python almost every time, because Java is just too verbose and the type system is kind of bad so the benefits are minimal anyway. But that's a false dichotomy: you can have static typing without the verbosity and with more significant benefits (like no null pointer exceptions) by using something like OCaml.
It’s fine to compare static and dynamic, but it’s important to understand the things you are comparing so you don’t make silly (and very common) false dichotomies like the one you point out. The problem isn’t the comparison, but laziness.
Recently I worked on a project where initially we though about writing it in Rust, because why not, it seemed initially a good idea. It turned out to be a completely wrong idea. The project was a simple web API, nothing fancy, GraphQL and a SQL database. After a lot of frustrations we decided it to rewrite everything in TypeScript and did that in a week.
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.
In their defence, rust is alright to spin up simple APIs or even complex backends. It wouldn't take me more than a few hours to write a small graphql api in rust.
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.
There has been a movement in the Rust community to position it as good for backend web development. This is why there's been so much work on async, excitement about Actix, etc. It's not hugely surprising that this has given outsiders the impression that Rust might be a good choice for backend web development.
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.
To add to this, dynamic typing is proper tool to use for API, because the input payload is just formatted text, without / with very few type definition. My experience said that it's hard to play with JSON on static typing, without adding a strict data validation / conversion at the start. Serialization comes with a set of strict rules that need to follow and state beforehand too.
The contrary, on dynamic typing language nested object as well as array can easily be parsed natively and be used immediately.
This is absolutely false. Not a single word you have written in this comment is true. This is a pervasive myth that you are perpetuating. If you had read the article, you would know that what you have said is demonstrably false.
There is nothing stopping you from operating on arbitrary JSON in Haskell.
Ok, but this works just fine in Haskell. If you have a well-formed JSON string and you want to parse it as a generic value, you can parse it into the Value type. If you have a typed record (something less general than a Value) and a JSON string that has enough of the structure to be parsed into that typed record, you can parse it into that typed record. If the JSON string has extra structure/data/fields your parser didn't expect, it's fine. Your JSON parser in Haskell can ignore those extra things. Just like any dynamic language.
We switched out some API code from Perl and Python to Go. JSON has been a pain at times for sure. Arbitrary nesting, values that are sometimes strings or sometimes integers (3 vs "3"), dynamic keys, and null vs zero value. These JSON structures were much easier to deal with before because we could be sloppy. Having to have a typed schema was a pain at first, but we love it after. And better yet, we can be confident of the values that we emit and our customers (internal and external) can be now use something statically typed if they like as we did all the heavy lifting.
It sounds like you think adding a conversion at the start is difficult and cumbersome, but it isn't if you use a good serialization library. E.g. with the Rust library serde, you just define the shape you expect your JSON data to have and plop a #[derive(Deserialize)] on it. Boom, fully failsafe JSON deserialization into the type.
Structural typing is extremly helpful/practical, it lowers "type-friction" a lot. I have a dream that flow/ts will be lifted up to js spec one day (yes, I know, that's why I said "dream"). With this the language would be open to things like multiple dispatch a'la julia/traits/typeclasses and/or pattern matching - which would (imho) place the language at the top for couple of decades. This kind of stuff is unfortunatelly outside of scope of flow/ts as it would require runtime support, which flow/js explicitly don't provide (ie. stripped types makes valid js, all type-stuff happens at "compile" time only, without access to runtime at all).
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.)
This is a decent description of how to handle unwrapping a payload in a language with ADTs.
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 don't think this is a swipe at Rich Hickey, unless it's considered a swipe to call someone out for repeatedly making misinformed statements about things they don't understand properly.. which is what Hickey does a lot in his talks, about Haskell's type system in particular.
The author says that Rich Hickey has built a speaking career on emotional appeals to the superiority of dynamic types.
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.
The Manifold project [1] nicely illustrates the author's proposition regarding structural typing and static type systems. Using the Manifold library you can indeed create structural interfaces [2] in Java similar to those in TypeScript. Manifold also enables the use of structural interfaces with Maps, it's pretty amazing.
We are seeing a natural evolution where the size and complexity of software is making strong typing almost a necessity. Python now has a type hint system. Types can be checked with external tools but Python 4.x may (?) have that built in.
Ruby is also moving in the same direction, as far as I know.
Every time this comes up, I think about how the pendulum swings back and forth. For example, if we take static and dynamic type systems in a slightly larger scope, we’ve just recently moved from a static system to a dynamic system, because the static system was being mis-used by “libraries”.
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?
Protobufs don't follow this model. For example, a User message type will often be defined in one place and code generated from it in multiple languages. Every server and client uses essentially the same type, modified as suitable for that language. As a result, clients are usually working with types that they don't control and that have many more fields than they actually use.
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.
It probably would work, provided that each client takes the original proto file and removes all the fields they don't use, so they are treated as unknown fields?
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.
Seldom mentioned in type system discussions like this is the notion of openness. For instance, F# is one of the very few languages addressing openness where schematic structure in data can be directly and type-safely reflected by the type system e.g., using "type providers." This general area of research is relatively untapped and, in my view, offers huge potential given weak links with conventional type system/data bridging solutions (eg code generation). Structural types emitted from something like type providers would be a game changer.
The author doesn’t really address the issue raised in the first (longer) quoted post.
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.
I think it's absolutely addressed. With either a dynamic or static language, you have to make decisions about which fields are essential, whether you can ignore additional fields, etc. And this post shows how you can do that in Haskell.
Versioning is hard, because it's a coordination problem, but it's not the type system that produces the pain.
> And this post shows how you can do that in Haskell.
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 or reasoning about unknowns diminishes the advantages of static typing.
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.
>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
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.
> 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.
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.
Wouldn't that boil down to the communication between the distributed components? I think this author's solution to that is well detailed in his post "parse, don't validate".
A general principle in a complex system of components is for each component to accept the widest range of inputs is reasonably can (and generate the narrowest range).
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.
> 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.
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.
Some kinds of static type systems (by which I mean all of the widespread ones which aren't Haskell or similar to Haskell) make extremely specific guarantees static, such that you can't change mere implementation details without rewriting a lot of code. For example, if you're using a library which specifies floats as an input type, and you now need doubles, you're pretty well screwed: You either rewrite and recompile a huge chunk of code or you decide you don't need to expand your precision after all.
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 would posit that, the more specific the rules of a system, the fewer behaviours can be expressed by it.
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!
I wrote the pickle.load comment [1]. I want to defend it here.
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.
I can easily write you pickle in Haskell. In fact you can easily embed Python's single type in Haskell and thus do everything you can do in python.
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).
EDIT: I was in a snarky mood earlier when I wrote this comment, I was tempted to just delete it, but I’ll leave the text as a reminder to myself to find better wording for comments despite my personal mood in the future.
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 think the reason for static types is up to the user of static types. There may be multiple reasons or motivations for static typing. In particular, static linear type systems are useful for, in addition to other reasons, the ability to fully specify the creation, usage, and consumption of resources. This is a direct performance benefit. Incidentally, this can be said of substructal types in general. Types equipped with Algebraic effects for the management of ‘side-effects’ and uniqueness types also are useful for direct specification of several things, one of them being the soundness if updating data structures in place. Again, a direct performance benefit.
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?
>> but they simultaneously advance an implicit belief: that dynamically typed languages can process data of an unknown shape.
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 don't think there was any reason to assume a post title starting with 'dynamic type' would use open to refer to open-source - how could there possibly be a correlation?
The reason would be am unfamiliarity with the use of the term "open" in a typing context. Without that knowledge, "open source" would be the next most plausibly related usage.
> We don’t have to respond to an ill-formed value by raising an error! We just have to explicitly ignore it.
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.
- 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.