I love typing systems too, there are compelling advantages...and disadvantages.
I guess sometimes what seems strange is attempts to bolt type systems on to fundamentally dynamic languages, like adding two extra wheels to a motorcycle, extra fairing, and then calling it a car.
I don't fault anyone for wanting a car. But if you wanted a car, why not start off with a statically typed language? Why bolt this stuff on really in contravention to what the dynamic languages are trying to be?
Perhaps this is JavaScript fatigue in a new guise? If everything has to be JavaScript (for whatever reason) then having no static typing ever may be hard to live with?
Am I missing something or does the motorcycle with two extra wheels seem destined to be clunkier and less flexible than a proper car?
This is effectively dragging some of the benefits of static typing to dynamic typing. I wonder why you'd pay the cost of dynamic types though, instead of going the other direction. With type inference you don't need to explicitly write types the entire codebase, and you can opt-in to dynamic types in controlled, explicit scenarios.
Furthermore, in my experience I find use of the things that static types can catch and contracts cannot on a nearly hourly basis while I rarely to never use things that contracts can check but static types cannot.
I think the thing you're missing is that dynamism is not about avoiding types, it's about having the flexibility to define your own type system. Clojure actually has real static typing - not quite complete, but it's there - and it's a library(!) Not a single change was required in the compiler. That's kind of mind blowing, no?
Let's take a look.
> Validation
Validation typically means that given a set of shapes of data from a large class we should determine whether a certain instance fits within a smaller class. For instance, parsing selects out valid strings amongst all strings.
Haskell has a number of libraries like this. Let's use JSON for example. We create instances of the typeclass
class FromJSON a where
parseJSON :: JSON -> Maybe a -- simlplified
and now each type which instantiates that class gets an automatic validation as a JSON-like type. Similar patterns are available for any other kind of "validation".> Coercion
Coercion in the core.spec sense is a similar game to the kind of enhanced validation I used above. If validation picks out a subset of valid instances, coercion, conformance, lets more than just the subset stand for itself—other instances can "conform" to the same thing.
Again, type systems are very handy for this. The JSON example above is already taking care of this in a way more robust than core.spec. The desired result type `a` drives all possible "parses" and conforms them all to its value.
> Error reporting
Let's take a closer look at a more real type of the method within FromJSON
class FromJSON a where
fromJSON :: JSON -> Validation ParseError a
what a `Validation` does is collect errors which occur in the parsing of a value `a`. All of the errors which arise throughout parsing are collected.Now, core.spec takes advantage of Clojure's core data language (EDN or whatever) which has the property of having concrete "paths" from the root of any value down to any sub-value within it. This is a nice property in that core.spec can pinpoint the location of an error within a type.
But it's a property of the shapes of Clojure data, not a property of Spec. We can write a type in, e.g., Haskell, which has the same properties. If we replaced JSON with that type then we'd have the exact same property.
> Automated test generation
This one makes me laugh a little bit. Automatic test generation was invented for use in Haskell's type system. For this we have the typeclass
class Arbitrary a where
arbitrary :: Gen a
where `Gen` denotes a randomly chosen value which can be "shrunk" to find a more minimal example. Create a collection of Arbitrary instances for the data of your system and you'll immediately be able to generate "property tests".Reid Draper, original author of test.check, actually was cribbing the design precisely from Haskell's QuickCheck library.
---
So we might wish our types did these things... But we'd be mistaken to do so. Our types already do these things and have for longer than Clojure has been around!
Furthermore, I really can't let it pass that Clojure's core.spec is not a form of static typing at all. It enables no guarantees at compile time, only at runtime.
Core.typed is a static type system and is outside of the compiler as you note, but there's nothing special here. People put type systems in their compilers for (a) convenience and (b) to guarantee the things fed to the compiler are well-typed so that the compiler can generate more efficient artifacts. Both of those reasons are auxiliary, optional. There has never been a reason why a language couldn't just build an external type-checker. Hell, Flow and TypeScript are more or less exactly that.
Sorry to come on strong, but I think it's quite far from the truth to take these things as benefits of dynamism. They have always been there. Dynamic languages just make them a little harder to access.
All the newer static languages use type inference anyways so its not that common to need to specify explicitly.
Besides, if you want to turn off the type system you can just cast to object or use "any" in the case of typescript.
JavaScript's untyped insanity is also the main reason it's around 10x slower than c# or Java.
Again js is a familiar example, but untyped "numbers" are HELL if you're trying to do any real math or implement a mathematical algorithm. I decided against porting one of my libs to JS for that reason alone.
A lot to lose and nothing to gain with dynamic typing.
Take a look at how fast javascript mutates, I'd argue that rate of mutation is one of the things you can do in a dynamically typed language. Java doesn't mutate like that, despite having many of the same ecosystem pressures, such as the pressure to "be good at everything" because it's so widely used.
That mutation often comes with unneeded parts and kludges, but the rate of mutation and change in the JS ecosystem has also been a huge positive. Still, TANSTAAFL and all that, I'm certainly not saying it's all good -- but I think you overstate it considerably when you say "A lot to lose and nothing to gain with dynamic typing"
Well JavaScript weak type system allows it to be shaped basically however the user want, so to an extent it's a language that make it easy to build something upon, like another languages or adapt any library from any other language.
JavaScript however definitely introduced functional programming to a generation of developers, no question.
But it was designed for extremely sloppy ones too. JS tries hard not to throw a type error.
> I don't fault anyone for wanting a car. But if you wanted a car, why not start off with a statically typed language
When I started programming I thought type declarations were getting in my way ... now I'm using Go which has one of the most rigid type system of all.
When I was using node I was like writing 10 000 lines of code a day ... now I have hard time making sense of what I wrote 3 years ago, let alone understanding someone else's JS codebase.
We web developers are stuck with javascript in the browser. Any proposed solution would be "bolted on" to javascript.
Also worth checking out: tcomb[0] which can let you use your Flow types at runtime for eg; pattern matching.
I know that flow has prevented me from checking in bugs, because I've tried to push up code with e.g. misspelled property names and the pre-push hook stopped me.
EDIT: You can see schema in action in https://github.com/cardforcoin/shale. In fact, the latest build surfaced a bug via schema- https://circleci.com/gh/cardforcoin/shale/379. Next version we're planning to migrate to spec.
Not yet, but I have some use cases (mostly validation).