Clojure vs. The Static Typing World
lispcast.com
lispcast.com
I feel the opposite way. I find a dynamic approach useful in some places, but in most places I miss having static typing to help catch errors faster and give my IDE better auto-completions and make exploring new APIs faster without constantly needing to look things up. And rather than small intricate algorithms, I find the most important place for static typing to be when making big refactorings that span the whole codebase. I think my ideal language would have static typing by default but you could disable it in places.
The water is nice, you should jump on in.
It seems to me, that types are useful for useful for expressing the boundaries of components, but they seem rather awkward constructs to be wrestled with to express the invariants and predicates about the state of the program that I invariably end up using in my head to insure that my code is correct.
For example, one might simply want to insure that three variables, say x, y and z, satisfy the relation (x <= y && y <= z) while inside a loop. The x, y and z might be integers or account-numbers or zip-codes or anything else with the <= predicate.
What I want is not to twist the type system around to say that just while in this loop the type guarantees that (x <= y && y <= z). What I want in a programming language is to be able to express this as a claim I'm making about the program at this point and to have help from an interactive theorem prover that it is so. I'd expect some sort of dialog with my tooling that would point out where I needed to make changes to guarentee this or to indicate that it is a claim stronger than needed for the program to run correctly (and satisfy it's specifications). Type systems just don't seem very natural for this; I would think we would use something like Dijkstra's weakest-preconditions or temporal logic over program states.
I really am asking for help in understanding where research on programming correctness is currently headed. (You don't have to explain it like I'm a fifth grader, I've been programming for 50 years, many in grad school.)
--------------------------------
(quote from someone named Racketnoob) “I have the strange feeling that types hamper a programmer’s creativity.”
The above sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages — that they are losing something, a degree of freedom that the writer identifies as hampering creativity.
Is this true? I will argue, to a degree — yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel’s incompleteness proof, is that the human ability to recognize truth transcends our ability to capture it formally. In computing terms our ability to recognize something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work.
That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. The invitation of adding types was thus taken up by myself, and the journey to making this program type secure in Shen emphasizes the conclusion in this
I wonder if it might be possible to feed predicates from clojure.spec to the inference engine/type checker from the Shen java port to gain static type checking. I wish I had more time to work on this kind of fundamental research, but alas I'm merely a working programmer schlepping data to and fro.
imo without those the argument (to anyone outside Clojure world) appears to be "lets just use open maps for everything", which is not really conveying the larger point - that one can have reasonable structure and description/enforcement of that structure using predicate language, which to some extent can be applied during compile time and enables static analysis tools. it's a compromise between rigidity of haskelly type system and the wild-west of tossing open maps around.
If instead it was merely a form of static analysis, then it could easily be seen as something that can be added. Which, in many languages, it can be. The forms of analysis the advanced tools can give for C codebases is quite impressive. All without having to rewrite the system with more precise types.
Similarly with LISP. It is widely lauded as a very popular dynamic language. However, there is nothing stopping you from statically analyzing it. Obviously some practices make this more difficult, but sometimes just having an escape hatch for the developer is enough. Just as obviously, these practices that truly make it hard to analyze statically aren't used that often. That is, a decent sized program will almost certainly use the features in a few spots. But only a few and the majority of the code can still be analyzed easily statically.
Well, sure there is. Someone has to decide it's worthwhile to build it, then they have to build it, and polish it to a point where it's usable which generally means a community has to form around that tool.
Years of work.
Doesn't surprise me that people think it's more worthwhile to just use a statically-typed language.
But, and this is my point, this was effort that had to happen in creating the static languages, too. Just now we locked out the benefits to existing problems to problems that are rewritten in the new languages. Contrast this with hardening existing codebases by running enhanced tooling against them.
This also ignores some of the analysis for lisp languages. I know typed racket comes up every week for this topic. It didn't invent type checking for lisp, either.
Sometimes I wonder why there aren't more 'empirically' typed languages, i.e., you write a function and some unit tests that exercise it and from that the compiler can determine what are the actual types and values the function sees for every variable.
As an easy example, if you are looking for functions that can return a Foo, autocomplete does little to help you know that you have to call .convertToFoo() on any of the baz instances in scope. There is already more than just basic type mapping going on. (To that end, a graph traversal assuming shortest path from symbols in scope to the desired shape works. So it is doable, of course.)
To your question of "empirically typed", that is close to some of the stuff that more advanced tools can do. I liked showing folks that Coverity wouldn't just tell you that you forgot to check for null, but would show you how the null would get there from the call patterns. Quite impressive.
Dynamically typed languages, on the other hand, don't really have that much more research that can even be done with them. Can't do any more research on the type system because there isn't much of one. Really the only thing you can do is introduce language features that are difficult to type in a static system, but at that point you're just giving more theory CS phd students targets of things to find a novel way to type.
That being said, the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out. Using haskell? Is it GHC or is it some alternative ... because that impacts some type class definitions that are possible.
Eventually the static types are going to win because we'll slowly figure out how to type everything (well, nearly everything) and we'll slowly figure out how to package that power in a way that everybody can understand.
However, in the mean time there is a very real cost to having to learn any given static type system that doesn't exist if you live in a dynamically typed system. Additionally, if you do understand some type theory you can bring over the lessons learned to your dynamic system. You won't get type checks at compile time, but you will get a more disciplined way to produce code.
[1] - http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=029...
I do agree that "eventually statically checked specifications are going to win", but I'm not sold that those specifications will take the form of (something easily recognizable as) a type theory. (However, neither outcome would surprise me).
> the problem with static type systems is that there is a lot of details that you need to figure out to A) be able to use it and B) be able to avoid the edge cases. You'll eventually need to learn about type theory ... which isn't just one thing. Agda and Idris have incompatible definitions of equality and that has an impact. Are your dependent types intensional or extensional? It matters. And that's just the theory side. Two different type systems with the same theory might have different implementation details that impact the programmer. Are you using ML? Is that an applicative functor or a generative functor? Hey, you're using first class modules, cool. Btw you can't use that with applicative functors, don't ask why it has something to do with complicated type theory stuff that took people years to figure out.
that in itself is one of the best arguments for strong dynamic systems with small set of ground types - if before solving your problem you have to solve the problem of how to type your problem and before that you have to learn man-years worth of category theory.. no thanks.
In these instances you might as well create a dynamically typed system and see what happens when it meets real life. Yeah it might fail, but the static version was going to fail too. You can save time by not having to worry about what the "proper" type is.
The other side of this is: What do we really want our types to do for us? This isn't always the same thing for everyone. I've created DSLs in a dynamic system that failed in weird places and when I tracked down the reason it was because I was using two functions together that did not agree on the "type" they were passing between themselves. In this instance, type theory wasn't going to help solve my problem, but a quick "typecheck" of the code would have pointed me in the right direction to find a silly mistake. On the other hand, sometimes you can use types to solve your problem. I know it's a bit cliche, but rust is a good example of this. If you want to avoid GC but still want high level programming features and no memory corruption then linear types is one way to achieve that.
No you don't. Most of the most prolific Haskell programmers (Don Stewart, Neil Mitchell, Lennart Augustsson, probably SPJ himself) would tell you they don't know any category theory.
In the same way that static systems are moving toward something that looks like dynamic typing with static safety, so are dynamic systens via gradual typing and optional static analysis tools. I don't think static or dynamic as we know it now are going to win, the dominant model of the future may well be one where broad inference allows statically verifying most constructs without type annotations, and languages support either allowing and disallowing constructs that aren't verifiable (and maybe even support disabling static analysis entirely, though people who use that option for anything but prototyping will be mocked as unprofessional.)
What would it mean for a StaticScript program to typecheck? It doesn't guarantee it will have no type errors. The model you typecheck against may be very different from the runtime truth. Browsers are different and provide different features, and will change after your program is compiled.
Static type checking has a fundamental limitation: it happens too early. The more divergence between the static model and runtime truth, the less useful static typing is. This is a fundamental limitation, a place where static types can never supplant dynamic ones.
In any case, your example is one in which static languages are no worse than dynamic ones, so it is not one which prevents static languages from displacing dynamic of they are otherwise superior.
1. When accesses are resolved dynamically, the failure mode is better controlled, e.g. exception instead of buffer overflow.
2. The failure is deferred to the point of execution (instead of e.g. load time). It is easy to omit features that depend on missing runtime support, just arrange for that code to not be executed.
3. Dynamic types allow you to interrogate which interfaces are supported, via reflection.
We see all of this at work in (good) web sites. They gracefully degrade, they can dynamically choose implementations based on what the browser supports, and failures are JS exceptions instead of aborts.
> In practice, of course, that's a bigger problem with interpreted than compiled languages
Why does interpreted vs compiled matter? IMO the key distinction is dynamic linking vs static linking. When you link against code compiled after yours, the less assurance static types give, and the more important dynamic types become.
> static languages are no worse than dynamic ones
The proper comparison is between languages with dynamic types and languages without. TypeScript has both static and dynamic types. If it had no dynamic types, it would not be a viable JS replacement.
Dynamic typing changes a little bit about how the solutions are implemented, but not the difficulty or even the basic logical approach.
> You'll eventually need to learn about type theory ... which isn't just one thing.
I'd say that most Java developers are comfortable with its type system, including the parametric polymorphism that it supports, and most of them probably don't know much about type theory. The same can probably be said of C#.
> we'll slowly figure out how to package that power in a way that everybody can understand.
I think we're already there. Java's generics appeared in 2005, and while there probably was some cultural shock in the Java community in the years that followed, it's safe to say that most of this community can claim to have a reasonable understand of generics in general. The addition of C# and its type system helped disseminate this knowledge further.
> This is just a guess, but at the time he wrote Clojure, those type systems most likely were Java-style (Java, C++, C#) and Haskell
SML and OCaml pre-date some of the languages in that list, and certainly pre-date clojure.
The "positional semantics" section -- and that whole class of arguments -- never made any sense to me. All languages have hash maps, so this is about program design rather than language design. Or perhaps, at most, an argument for having nice syntactic sugar for hash maps. In any case, I'm not sure what this has to do with fundamental language design issues. The "can Haskell..." stuff has a similar smell to it. The answer is always "yes, Haskell (and everyone else) have hash maps and HOFs."
At best, it's an argument that those languages should provide a bit of extra syntax around the "everything is a map" programming style. Which, I won't disagree with :)
> In the kinds of systems Rich is talking about, any data could possibly be missing... At the limit, you would need to make everything Maybe
Which is why ML-family languages have both exceptions and algebraic data types.
The discussion of abstraction is just confusing. The author seems to define "abstraction" as "literally any list of information". And I guess it's true that pathologically bad abstractions do exist, but... what point is being made here? I don't get it.
The "screwing around in the type system syndrome" thing actually makes sense, but you can see the same thing in dynamic languages (e.g., with meta-object protocols or macros). There's something more fundamental here, and it's more about human psychology than language design.
I have to agree with keymone, though, that the really interesting thing about clojure is not its design but rather clojure.spec. Sure, you lose a lot of static guarantees, and along with them some of the maintainability/correctness that come along with statically typed languages. But perhaps recovering static checks, and tooling based on static checks, is best done on a library-by-library basis via compositional specification checkers specialized to the particular library. Rather than by a single general-purpose type theory that's rich enough for the "real problems in the messy world" type of programming. And the article kinda starts hinting at this toward the end. But I think keymone really hits the nail on the head when it comes to what you should take away from learning/working in clojure.
+1 !
If necessary you don't need to use and ADT+pattern matching on JSON. You just work with the hashmap directly.
But the code that results is very simple while remaining strongly typed.
It ends up being not that different in style from something like hpricot in ruby.
type Object = HashMap Text Value
The keys of the hashmap are Text and the leaves are "Value" which contain more JSON
here are different well-formed json values that both resolve to the same type, A.Object (either you get a parse error String for not-well-formed json, or an A.Object)
>>> A.eitherDecode "{ \"name\": \"Joe\", \"age\": 12 }" :: Either String A.Object
Right (fromList [("age",Number 12.0),("name",String "Joe")])
>>> A.eitherDecode "{ \"name\": \"Joe\", \"age\": {\"foo\": \"12\"} }" :: Either String A.Object
Right (fromList [("age",Object (fromList [("foo",String "12")])),("name",String "Joe")])
Or, as noted by chowells, you can use lens-aeson which can be thought of as a DSL to perform queries in a dynamic fashion:
retrieve value of "foo" in "age"
>>> s = "{ \"name\": \"Joe\", \"age\": {\"foo\": \"12\"} }" :: String
>>> s ^? key "age" . key "foo"
Just (String "12")It's not different for that type. The point of using a statically typed language is you can give static types to other entities in your program!
> The tools Haskell gives you are great at some things, but dealing with arbitrarily nested ADTs is not one of them.
There's nothing more natural in Haskell than recursion and processing of ADTs. There are dozens incredibly well-research patterns for processing just about anything under the sun.
> What we wound up doing was nesting pattern matching to get at the value we wanted. The deeper the JSON nesting, the deeper our pattern matching.
In my experience that works great for moderately complicated and ugly JSON messages. Tried that in Haskell, OCaml and Rust. Rust was most clunky due to the way things are represented in serde (I expect that's more performant though) but still worked nicely.
Alternatively, lenses would allow for incredibly easy access to just about anywhere in any JSON document. Want to hit multiple nested targets in weird locations? No problem!
> But imagine if more and more of your code is dealing with JSON. It would be nice if there were some easier way.
Sadly the author skipped explaining that mythical "easier way".
However, I was parsing some ugly format that doesn't deserialize cleanly:
match v.as_slice() {
&[Value::String(ref s), Value::Object(ref o)]
if s.as_str() == "i" => {
// more code here and still need to unpack x and y from o
}
case j of
Array [String "i", Object o] | Just x <- HashMap.lookup "x" o, Just y <- HashMap.lookup "y" o ->
// code goes here, can refer to x and yMLs are widely cited as some of the best languages for implementing compilers in, and large chunks of a compiler consist of transforming various ASTs. An AST being a particularly complex recursive ADT, it seems strange to claim that's a weak point of statically-typed languages.
Rich's biggest complaint is that our tools should be a la carte not forced down our throat at every turn. Type verification (static or not) should be a tool, not a religion. (In this way, Rich renders the perennial static vs. dynamic debate stupid: it's a false dichotomy that most statically typed languages needlessly force us into.)
In Rich's talk, the bigger target of his attack is ADTs -- that is, processing information in any way that doesn't make properties first-class. (It's easy to mix up his argument against ADTs and static types, probably because ADTs are kind of like the go-to idioms for people programming in statically typed languages.)
I think one of Rich's one-trick ponies (i.e., one of his goals) is to remove the impedance between thinking and coding. We humans don't naturally think in terms of ADTs (e.g., when you open a dictionary, you see vocabulary/words, not categorical types/ADTs.) Computers only ask us to be precise and ADTs are unnecessary to achieve precision -- properties ("words") capture all of the precision needed to solve our information-processing problems.
All Rich is doing is trying to remove that impedance between thinking and coding.
Static types are also unnatural and unnecessary to the precise expression/coding of solutions to our "situated" programming problems. I don't think any static typing enthusiast would disagree. What the static typer would say, though, is that they've done something clever: they're adding the extra impedance of type verification to achieve a higher level of problem-solving throughput. (Because their static types reduce other impedances: bugs, refactoring ease, etc.)
Are the static typers right? Rich seems to imply no. (Because even though he says typing should be a la carte, you can clearly see in the talk that he has his predilection.) The fight here is usually left to our intuitions and habit, but my guess is that someone smarter than me could model this programmer-productivity problem as an optimization formula, showing how over time software-construction slows down due to certain constant impedances like juggling static types and certain accumulative impedances like coupling and code quality in a large code base.
My guess is that this formula would show that in low-quality code bases with lots of coupling, the static typing tax would win. But that in higher-quality codebases the static typing tax wouldn't pay for itself. This jives with my instincts of course but you also find that the better programmers (the ones that know how not to couple shit) favor dynamic typing while those that regardless of experience haven't learned how to keep coupling at bay prefer static types.
Haha, wow. That is some serious reaching there. And let it be known, I'm not referring to myself as some great programmer, because I don't think I am.
1. You imply static typing is a tax rather than something that reduces cognitive overhead as time goes on.
This point is very debatable.
2. You imply that 'clearly, anyone who doesn't favor dynamic programming is a lower quality programmer who doesn't know how to keep coupling at bay'.
That's pretty ridiculous, if you weren't cackling with anticipation at the responses to your flamebait then I have to assume you're serious, and you've already drunk the koolaid.
(add [x y] (+ x y))
(add [^Integer x ^Integer y] (+ x y))
2:
I don't mean to make such the broad generalization that you're jumping to here. What I mean to say is that static typing in the traditional mode (non-a la carte, applied everywhere, w/ all of the typical idioms of ADTs, pattern matching, etc etc) may help in cases where your code is heavily coupled, complex etc, but I think that its a needless impedance in higher-quality codebases.
let plus x y = x + y
Also, the fact that types are dynamic doesn't mean you don't have to think about them, you still have either type errors (like in most lisps) or implicit coercions (like in JS, you probably don't want that).
There are genuine arguments between static and dynamic typing. The assumed annoyance of writing type signatures is only a valid point for specific type systems such as Java, and is certainly not a generic concern.
As usual: https://ro-che.info/ccc/17
When my product manager comes to me and says "I want a button here that when you press it, it add the user-entered value in input box 1 to the value in input box 2."
Okay, done:
(button :on-click #(+ (box1-value box2-value)))
Let's say that night I wake up sweating realizing that the user could type in the String "one" and "two".
Thankfully this before my push to production, so I go re-implement "+" to support English numbers.
Okay, now I go live. Well, now my user types in roman number "I". And a weird value is produced.
My product manager doesn't care about this class of users, so great I do nothing.
The point of this is that every step of the way, my choice to type check or not is a la carte. Not forced down my throat. Types are my tool, not my religion.
Clojure does have a few features that support dynamic dispatch, so there may be some games there to play as well.
The key point though is that "+" is really just my name for something that "adds two numbers together" -- that is strong enough semantics for me to express my function/business problem in terms of it. How I grow the supported range of that function...there are a number of ways I could go about that.
(I'm not saying this is how to code, but I'm clarifying that you don't have to think about types to get the semantics/precision. You just want to think about types, can't help thinking about types, or something else, you tell me.)
Nope. No thinking in types required there.
> I am simply saying I want "plus" semantics to be identical to "+".
Yup. And that's exactly what the code that Drup pasted does.
> If "+" is capable enough to add the String "one" and "two" together
Yup. And that's exactly what the code that Drup pasted will do.
If you're telling me you don't have to think about types, then you and I are on the same page.
But it sounds like we're talking Haskell here, so afaik, somewhere Haskell is going to ask you to specify types so that it can complete its type-proof (i.e., compile.)
If you're saying No, Haskell doesn't need that, then I'm afraid you have a dynamic language on your hands.
Prelude> myfun x y = x ^ 2 + 2 * y * x - y ^ 2
Prelude> myfun 3 6
9 myfun x y = x ^ 2 % 2 * y * x - y ^ 2 55 % 102 would produce 55102
And if your answer is "I only need it to work on integers" then don't blame Haskell when I choose to specialise it to Int!
This is a silly example, of course, but the real world isn't short on creativity/silliness.
Suppose your types are Strings. And your plus operator can add "one" and "two", but fails adding roman numeral "I" and "II", my guess is you'll another type/ADT into your static typing called RomanNumeral so that your type proofer will check you at compile.
Meanwhile I will do exactly nothing because my product manager says he doesn't care if the user types in roman numerals.
Which means I will be building my next business feature while you're still doing type math.
Hmm, no. Why would you guess that? That makes no sense at all.
If you say "I choose just String. I.e., I overload String to contain both types of values. Then you are doing dynamic typing. So why in that case do you choose dynamic verification, but in other cases not? What is your criteria for when you choose static types versus dynamic types? Or do you just go by instinct?
This breaks the HN guidelines. If you're going to comment on a flamewar topic, you need to do better than this, even when someone else posted flamebait. Especially then.
There are many languages in which the `+` operator can be applied to types that are not integers.
Are you trying to say plus two integers -- if you are trying to say something specific about the types -- then you have to say types to be precise.
But if all you're doing is saying I want "add" to have the same semantics as "+", regardless of types, then you are perfectly precise and you are done.
This is a toy example, obviously, but this line of reasoning extends to real-world examples.
In a static type system with inference, both examples would just be
(add [x y] (+ x y))
2:
In my experience, ADTs (and pattern matching in particular) make coding problems much easier to solve (and the code itself considerably simpler) than the alternatives in many languages. For example, I'm writing a compiler in Go, for fun, and a lot of tasks would be far easier and more concise to express with ADTs/pattern matching. Another example is working with pattern matching in Elixir/Erlang, especially with binary data, which is beyond easy to express a parser for with pattern matching. Elixir and Erlang are dynamically typed, and have gradual typing via Dialyzer (though it's rather different from clojure.spec I believe), but pattern matching is pattern matching, and it's indispensable in my opinion.
Using something dynamic, like Lisp/Javascript/Ruby/Etc. would make it much more difficult to navigate the code for something like a non-trivial compiler (in my experience), and more difficult to reason about how it will execute. The other thing I don't see mentioned very often is that if the compiler can't reason well about your code, then it can't optimize it very well. Even with a JIT, you are paying a performance cost that is non-trivial, unless you happen to be using a language with a particularly good JIT, performing tasks that the JIT is good at optimizing at runtime. For a lot of tasks, this overhead doesn't matter, but I would rather lose some flexibility to be able to use the same language for a broader array of tasks.
Recently I was taking a stab at translating some code for an Earley parser from some dynamic languages (Javascript and Python) to Go, again for fun, and in both cases found it was impossible to do so because of the way the dynamic features of the language were abused - basically I would have to throw out everything and write it from scratch. The code was hard to reason about, because while reading it, you think you are working with values of a certain type in one function, but the same value somewhere else is getting treated like a different type. You basically have to execute the code to see what it does. Such flexibility can make for more concise code, but when the code _isn't_ concise, it can make it incredibly difficult to untangle. That's just my experience though. I'm an Elixir/Erlang programmer during the day, so I'm not anti dynamic languages by any means, but I have definitely found it easier to build certain types of applications in statically typed languages.
1: The inference allows me to express that part of my program without thinking about types. But somewhere in Haskell (or what-have-you) I have to express the types so that the compiler (type-prover) can do its proof-thing. This is required afaik by the non-optional static typed language. In a dynamic type language I can go into production without having to (help my compiler) prove anything.
2: Interestingly Rich Hickey goes to great lengths to make a distinction between writing device drivers, logic systems, etc and the other kinds of (majority) industry programming. He kind of stays hands-off on the former types of systems where he might agree with your points. For your example, in a compiler I might have an ADT represent a node in an AST and this helps facilitate a lot of what you're doing. And you're willing to take on the rigidity of having the ADT there b/c you probably don't suspect it to be a volatile construction, constantly undergoing revision, etc.
But in the other kinds of programs the Hickey talks about, your Person ADT/class is only hurting you. You are no longer in the cozy safety of some compiler/logic system. And (almost?) always your Person class is not stable (you'll be processing these Persons in many different contexts over time and the whole conception of those first-name, last-name, age, etc. properties having to clump together in one type is (almost?) always going to change). So in the other world of these "situated" programs (his term) you are creating a lot of work for yourself by introducing that ADT/Person class.
1: That's true for anything which isn't a primitive type, or built in to the language, sure. Most of the time though, the type you have to define is not exactly complex, take records for example (using a Haskell-ish syntax):
data Person = {name: String, age: Int} deriving (Eq, Show)
Once you get into a place where you are writing abstract code to work across types, with no type constraints, where higher-rank polymorphism is likely to be front and center, then yes, you will spend some extra time up front annotating those functions with their polymorphic type, and that can be annoying sometimes. Even that's not a given though, in Haskell for example, one can define a typeclass (such as Eq, for equality), and write code which operates on instances of that type without needing to do anything more than:
foo :: (Fooish a) => a -> a
foo a = # do something Fooish with 'a'
You can go into production writing code without your compiler proving that what you expressed to it is valid, but if something is wrong, you don't have any tooling (short of debugging) to fall back on, you have to figure out what went wrong, try to fix it, deploy again and hope you actually fixed the problem. With (good) static type systems, you may be slower to production that first time, but the compiler has ensured that you haven't made any mistakes based on what you told it you were trying to do. One can of course still make mistakes with a type system helping you, but at that point it's a conceptual mistake, i.e. you've told the compiler to do A, and it did A like you asked, but the right thing was actually B.
Nevertheless, I understand the desire for a compiler to just do what I say, regardless of whether the compiler thinks it's ok; but most of the time when I do that, it means the next person working the code behind me isn't going to understand it - if it's not clear to the compiler, it's probably going to be unclear to a reader of the code too. That isn't a hard and fast rule, but I have certainly seen instances of that.
In my experience, most of the dynamicism I rely on in such languages is for metaprogramming, all of which I would rather do at compile-time via macros anyway, and thus doesn't require a dynamic type system. For everything else, I'm having trouble thinking of an example where types would interfere, other than writing code which ignores things like checking if a result exists or not, or is a datastructure vs an error - and I would rather have the proper handling of those things done and enforced by the compiler rather than ignore it until something blows up in production. That's my take though, and for those who are desperate to get something in to production ASAP, it's probably not the right fit.
2: I'm not sure that working with arbitrary data leaves you in a situation where you are no longer within the realm of safety the compiler can provide you. You will have code that cares about aspects of that data, imposing some kind of logical structure to it, whether that's encoded in a type or not. The only difference between dynamic and static processing of that kind of data is that the dynamic code has to search for the structure it expects, while the static code defines that up front, and only has to try to match the data to that structure - working with it after that point is not going to differ much between the two. With dynamic code you'll still need to check if a field is present or not, and whether it's of the type you expect it to be. It is certainly easier to create arbitrary heterogeneous structures in a dynamic language (I won't argue that!), I don't buy the argument that a static type system is somehow ill-suited to the processing of such data.
I will say that it is annoying that before you can start writing code to process the data in a static type system, you have to define the types/interfaces that the data will take - sometimes I would rather just mold the raw datastructure via traversing it and pattern matching on it - but I think in the end that extra time up front ends up a wash with a dynamic type system because you spend less time on the tail end chasing bugs that the compiler can catch.
For Rich's argument to resonate with me, I think I just need a good example of what he's talking about - every time this topic has come up, I haven't been able to come up one, and I haven't seen anybody else do so either. An example where Rich (or whoever) thinks the dynamic solution is clearly superior, and no static solutions come close.
At the end of the day, I say use the right tool for the job, and if a dynamic language clearly solves a problem better than the static one, then hey, I'm not complaining (after all, it's why I'm using Elixir/Erlang to solve problems, though I don't think the problems they solve are necessarily at the dynamic/static divide).
Let me go through some work I just went through. Scrape web blog post, generate some semantic data about the post, send that data through some processing which perhaps infers some new facts, maybe discards some posts, then sends the data over the wire to be mapped and written to a searchable data repo. Which of course will be queried, read, and displayed in a web app.
This is pretty standard-fare programming in industry/web world.
I wrote this in Java, but here's my take: the easiest way to both implement and maintain this code is to model the web page data as a simple Map of facts -- properties with clear semantics ("author", "title", "content", etc.) and their values. The very minute that my scraper needs to introduce a new fact it does literally nothing from a code declaration point of view. It simply puts a new fact (say, "publication-date") into the Map. Absolutely no downstream code needs to be touched in order for me to do this. I just produce the fact/knowledge. That was just one use case.
Now to do this same thing with an ADT/class/record, I have to at minimum go declare that property in the ADT. But usually I also have to go update the ADT serialization code to make sure that it is writing this new property into the serial format -- the JSON, or what-have-you. Furthermore, on the other side of the wire, I have to make sure that guy is either using my ADT or map to his ADT, whatever.
Oh my gosh, this is just one use case and the non-ADT scenario asked me to do literally nothing to introduce some knowledge, some simple little fact, and the ADT scenario has me jumping through hoops to get my release out.
Mind you, this data-process-to-web-display architecture is very common in industry programming. And it is very common to find this jumping-through-hoops.
And we haven't even started talking about the webapp/display side of things.
Now I wrote this in Java, the whole way dodging ADTs and types where I didn't need them (ie, lean on Strings when in doubt), and using simple Maps. But even then the syntactic negotiation was quite large. Clojure embraces this map-centered/fact-centered view of the world at its core and this program would have been much much less lines of code and much much less cognitive overhead written in Clojure.
Now I know a static typer person is going to say, okay fine, but jumping through those hoops I've saved you a bunch of bugs. But I say no you haven't. Unless you go all the way with your types and have a Content type and a Title type ... because my bugs were to do with payload sizes and things like that. Things that even static typers will end up checking via some dynamic logic in their code.
The StringMap is trivial, and the GADT requires declaration, but is straight-forward pattern matching/construction from that point onward, so I don't think either option impose any "real" additional cost here.
Navigating/extracting datastructures via lenses or recursion/pattern-matching is clear and concise, definitely not onerous by any means.
I'll gladly admit that my argument hinges on using a state of the art type system, but in my opinion, if we're going to debate the merits of static typing, then we should be looking at the best it has to offer. It seems like perhaps you haven't had an opportunity to work with Haskell or something like it (want to be clear that's not a judgment statement, and I'm solely basing this on your last comment, if you have, sorry about that!), which is fine, I mean, I only ended up learning some of it due to diving down the rabbit hole of type system research while designing my compiler - but if the first thing I had to compare a dynamic language to is Java, then yeah, it's no contest I would use Clojure instead.
I think something important to remember is that I don't think one should be a "static typer" or a "dynamic typer" - dividing the world into right/wrong, good/bad, black/white is almost always the wrong point of view. If I'm automating something, or doing some exploratory programming, I'm probably going to reach for bash/python/etc.; if I'm writing a command line tool or simple service I'm probably going to use go; working on a concurrent system, I'm probably going to reach for erlang/elixir/go/pony/etc. - but if it's even remotely complex, I'm always going to favor the option with the best static type system, because I know it's going to help me (and anyone else working on the system, especially newbies) keep things sane. Over half of what I just listed do not have static type systems, but I still have a clear preference - it is possible to use the right tool for the job without compromising your ideals. Part of why I started working on my own compiler was that I wanted to design something that both provided the strong type system, while still functioning well as a "get shit done" language, something with the concision of Haskell, but the flexibility of ML (permitting both functional and imperative paradigms), a comfortable FFI, and good tooling, including the ability to run scripts interactively (for example, via shebang scripts). I haven't found a language that mixes all of that together in a way that satisfies me, which is why I still use a variety of languages for different tasks. So I guess what I'm saying is, try not to divide people into two camps - it's possible to live in both at different times, but still prefer one or the other :)
This is the usual general claim from one arguing for using static type verification in a given situation, but this is pretty fuzzy statement, no? "Keep things sane." We need to have more clear reasons than that, don't we?
In my view, the end goal in business is to optimize productivity throughput over time (i.e., make sure that we can deliver business value as quickly as possible.) But I realize this is not as simple as today's immediate throughput at tomorrow's throughput's expense. So there is this goal of keeping things maintainable (probably what you mean by "sane") -- but to be even more clear: it's productivity/delivery throughput we are talking about, no?
And if that's the case then we have to really justify that the static type dance is truly giving us that overall throughput. How do you do that? What is your general decision process about when to introduce type verification and when not?
To be specific, let's say I need to ensure that the value for my "title" doesn't ever exceed 80 characters. I imagine that even in Haskell you would make this a String, no? So you would defer that length constraint to dynamic validation/logic? (Correct me if I'm wrong.) Well, then why are you choosing dynamic verification in that case but for other cases like "publication-date" choosing to have the type checker verify that it is a proper date value? What is your criteria?
In my experience programmers usually just do what is idiomatic or most convenient in their programming language. Okay there is a Date primitive, I will use that. There is no Title or MaxString<Length> primitive, so I will just use an unbounded String. In other words, it's not a like a reasoned choice. Which makes me think, in general, the reasoning behind using a static type language is more fuzzy than usual.
But if you have even a loose criteria for why you pick static typing for a value versus doing the value's verification dynamically, what is that criteria?
The same as with the choice of anything: what feature to work on this week, whether to automate a process or keep it manual, whether to use JSON or BSON or Protocol Buffers ...
It's a judgement call and it's not really possible to give a good answer in a Hacker News comment.
So if what you're saying here is that in Haskell that this choice is mine, that I can always completely avoid having to choose static verification if I so choose (ie, I can get it a la carte), then that is just plain awesome. Is that what you are saying?
Well, yes, roughly, of course! You can always choose to use extremely broad types that give minimal guarantees, for example Scientific instead of Double or Int, String instead of MyPreciseErrorType, Map String Dynamic instead of MyPreciseRecordType ...
You'll find the Haskell ecosystem is not really designed around that kind of programming because Haskellers don't really like it but it can easily be done, semantically. It will also be a bit awkward syntactically, but it's certainly possible. And then you can opt in to types (a la carte) later by replacing broader types with narrower ones as your project manager refines his specification.
But that's not really the point. You can bolt on types to Clojure and you can bolt on dynamism to Haskell. My point is that I've almost always found it better to start in a strongly typed language, even when the requirements are changing rapidly.
What you're calling a reminder is not just a reminder; it's a requirement -- you are obligated to go update those places in your code before you can deploy/execute the code.
Which is the very definition of coupling.
This isn't just theoretical. I've encountered this pain again and again in my career. This kind of coupling is severe impedance. Even worse is when the coupling spans teams in an org. It is the difference between pushing a fix or business value out to production now versus having to coordinate across areas of your code base and/or architecture.
There is this feeling of control by enforcing every part of your code base play the same game. But when you break out of that, and realize it's a game. That you don't have to design your code such that it has to be updated altogether, then you realize that types are only encouraging you to do this unnecessary thing. You can design very powerful systems with complicated behavior with minimal coupling. Where you get to choose what parts of your code you update at any point in time.
It may well be that core.typed and clojure.spec get at least 80% of the benefits of Haskell's type system with no more than 20% of the cost, but in that case Clojurists need to spend their time explaining how rather than railing on Haskell's good parts. (Haskell has plenty of bad parts. The type system is not one of them!)
What I am after is this: Does mandated type verification yield higher overall throughput to the programmer trying to deliver business value?
It's clear to me that that having to pass a type checker before you can deliver business value is (at least) an upfront impedance/tax/cost.
So the burden is on the person (or PL) that insists on mandating type checking everywhere that it is somehow yielding overall higher throughput. (The usual line of argument I hear is that mandated type checking etc helps in maintenance cost. But this needs to be demonstrated.)
In my experience the coupling I mentioned just above is paralyzing to the team(s) trying to deliver business value. It is really the difference between an hour cost to delivery versus days.
I'll leave you with my parting thought: I've never used Clojure but I have used Python and Haskell. My experience is that Haskell's ("mandated") type checking allows me and the teams I've worked with to deliver far more business value than Python. If Clojure would allow me to deliver even more then that would be great, but given my experience with Python I can't see how a dynamic language would do that.
I guess my parting thought would be that this doesn't need to be that obscure. What seems to be implied in our conversation here is that the statically typed language is not introducing any extra immediate work for the programmer. But that is just false. I think it's arguable that over time that extra work may payoff, but we're not even at that conversation yet. You seem to be suggesting that because types can be inferred and not written down in many places, then the work has been removed. But the work is not in the typing, it's in the cost of making everything consistent wrt to the type checker.
I've noticed a common pattern amongst Clojure programmers that statically typed languages require "proving stuff to the compiler".
(defn add [x y] (+ x y))
(add (read-string) (read-string))
In Haskell, this isn't sufficient. I have to say something about types, and I have to compile first. That is what is meant by I have to "prove".
In at least this toy example, one of these workflows is orders of magnitude more work than the other.
Now what happens in that Clojure program if I enter junk inputs when I am prompted? Well, I get an Exception, or I get NaN, or junk. But you know what? I don't care. For this particular example, my product manager doesn't care. When he cares, I'll go add in some dynamic verification. The point is, my business priorities are my choice, not some academic proof system's. I like verification, though, so I can go add it in a la carte, i.e. per my discretion.
Prelude> add <$> readLn <*> readLn
3
40
43
> one of these workflows is orders of magnitude more work than the other.
"Order of magnitude" generally means "factor of ten". Are you really claiming that the Haskell code is at least one hundred times more work than what you wrote?
I have a question about "read-string". What sorts of objects can it return? Base numeric types I guess, plus atoms, and recursively, lists of the above. Anything else?
; -- the program --
(defn add* [x y] (+ x y 1))
(add* (read) (read))
; -- repl demo --
3
40.1
44.1(...friendly joke, of course.)
Prelude> add_ x y = x + y + 1
Prelude> add_ <$> readLn <*> readLn :: IO Float
3
40.1
44.1My Clojure program is valuable/effective/per-spec without the type burden. So the type burden has slowed my delivery.
And that "one single place" is for this trivial toy program. Now imagine the impedance across the delivery of a real business app.
And that "one single place" is for this trivial toy program. Now imagine the impedance across the delivery of a real business app.
This comes up in a concrete manner in your example. The add function is almost too small to be typed appropriately. There isn't enough information for GHC to constrain the choice of numeric representation so it picks one. If you were to embed that in a larger program with more specific operators no types are necessary.
Prelude> let add = (+) <$> readLn <*> readLn
Prelude> let foo = (/) <$> add <*> add
Prelude> foo
3
30.1
40
10.2
0.6593625498007968
Typically in the real world, the customer or product manager asks for the thing-of-value. The job is not find a `foo` that reduces the type annotations. The job is to add business value to your system, to your code.
The probability that the world asks for something that fits so nicely into your type taxonomy is low. The real world and the Future is often more creative than our invented taxonomies support. In these cases, what you need to do is go fix up your types/taxonomy so that consistency ensues again. Whether or not that results in less type annotations doesn't ultimately matter. It's the work you had to do (the game you had to play) to make the type checker happy.
Note: The implicit assumption behind what I'm saying is that we want to create less work for ourselves, not more. If we don't care about work/time/efficiency, then my arguments in this thread are all moot/baseless.
Please don't assume the motivations or intentions behind my actions and then attempt to use that to prove a point.
To address that point explicitly: In general, if requirements change then the code needs to change. Neither Clojure, nor Haskell will make that fundamental truth go away. You say you want to create less work for yourself when this happens. I'd like to propose that there is different types of work with differing qualities. When you receive a requirement change, the first step is to determine what that means for the system as it stands. This is by far the hardest step and is where the majority of the "hard" work lies. The next step is to change the system to fit the new requirement. This is primarily a mechanical task of following directions you laid out in the first step. I think it's preferable at this point to have some tool or process, even multiple, to make sure you do this part correctly. Tests, types, and code review are the three major tools I've seen aimed at this problem. Tests help ensure you've specified the changes correctly by forcing you to write them down precisely. Types help ensure you've implemented the changes correctly by forcing consistency throughout the system. Code review helps ensure you've implemented the changes in a manner that is understandable (maintainable) by the rest of your team. Note also that tests require an investment in writing and maintaining them, types (with global type inference) require no upfront investment but can require some maintenance, and code review requires participation of team members of similar skill level to you. They also all require some level of expertise to be effective. It seems shortsighted to throw away static types when they are, in my opinion, the cheapest method of helping correct implementation.
I did a job for a defense contractor once that brought the entire team of 10 into a room to code review page by page a printed out copy of the latest written code. Now whether this was rational or not, I'm not sure, but I will give it to them that in mission critical systems you don't want to take any chances and that you're willing to be way less efficient to make sure you don't deploy any bugs.
I've been at a few companies where one of the engineers discovers code coverage tools and proposes that the team maintain 100% coverage of their code. These were mainstream industry software businesses that could afford some minor bugs here and there, so no one thought this was a good idea. Most engineers I know doing industry programming think that trying to sustain some specific percentage is a bad idea. Most say that you have to write your tests with specific justification and reason.
So no reasonable person I knows would advocate some overall mandate to do Code Reviews like above, or to hit some specific metric on Automated Tests is a good idea. And yet the general tendency of statically typed programming languages is to enforce the usage of types through and through. This should be really interesting, considering that Code Review and Automated Tests are far more likely to root out important bugs than a type checker.
I'm not arguing against type verification. I agree with you that it is one tool among many. It's the weaker tool among the three tools that you mentioned but we are still somehow arguing whether it should be (effectively) mandated by the programming language or not.
Why mandate type verification and not unit test coverage? Why not mandate code review coverage? Because, when mandated, they cost us more time for the benefit they bring.
My main argument is that type verification is a tool that should be used judiciously not blindly across the board.
Not to bring up the tired argument again, but as far as I know there isn't proof for this. Nor is there proof that types are better at catching bugs than tests or code review. The best we can hope for is anecdata. I've got my fair share that shows types in a good light and I'm sure you've got your fair share that shows tests in a good light.
That being said, global type inference is in my opinion a fundamental game changer here. No longer are you required to put effort into your types up front. It is the only one of those three tools with that property. This makes it trivial to get "100% coverage" with types. That is why people argue for static type coverage.
Additionally, Haskell specifically has a switch to defer type errors to runtime, which means you can compile and test without 100% coverage.
I don't agree with this.
Static typing is the stronger sense (than C or C++) is mostly represented by:
- ML
- oCalm/F#
- Haskell
- ADA
Coupling is not idiomatic on them. This is mixed with the functional + inmutable aspect (not much on ADA, but as someone that used to work on pascal is not the mess of the C family...), but certainly coupling is WAY higer on JS/Python/Ruby.
By TONS. And certainly less skilled developers code on them. By orders of magnitude. Haskell scare people. Python not.
And that is despite the fact I totally love python. I don't say python is bad. Skilled developers totally love pytyhon too.
---
What I think is better to say, assuming always a capable programmer:
- A good programmer can program good.
- A good programmer prefer to use better tools, if posible
- A good programmer wanna do things faster (also, to make programs faster, but let's focus only in his own productivity)
But exist two ways! to do this:
- A good programmer love dynamic typing because he can manipulate the program in do things past what is obvious. He can do complex stuff easy.
But it miss the simple stuff
OR
- A good programmer love static typing because he can avoid to worry about trivial things, like always check if something is null, look at the documentation/code to see what is returning, etc. So he can focus in the complex stuff. However, do certains kinds of complex stuff make him wish to use something else.
However, I bet MILLON TIMES that truly everyone wanna:
- To have both static types for the code that is in the past/stable and dynamic for now. Static when things are settle and dynamic when not. And move between boths with fluidity so he can construct things on runtime and then get back on tracks for the stuff that not need to change!
I'd make that same bet, too.