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.
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.