[moxious]

I think of dynamic typing in a language as a big pro and a big con at the same time, but it's one of the things that makes a language like JavaScript or closure what it is.

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?

[mhluongo]

Spec (and more generally, contracts) aren't just about "making up" for the lack of static typing. They can encode a variety of invariants that a type-system can't, and are also useful for parsing (see coercion) and generative testing. Unlike most type systems, they also aren't required across the whole code base.

[nilved]

It depends on how you implement the gradual typing as well. Through contracts is one way (probably the bad way, since they still apply at runtime) and static analysis with type annotations is another way. There isn't any reason a sufficient static analyzer couldn't be as powerful as an inbuilt static type system.

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.

[tel]

Parsing and generative testing are well-covered by static types, but I'll give you that contracts can enforcing things static types cannot. That said, static types can enforce things that contracts cannot, too.

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.

[arohner]

> static types can enforce things that contracts cannot

Example, please?

[tel]

Sure. Consider the type

    forall a. a

With mild conditions on what the program fragment achieving this type can do I can be certain that this function does not return. It is an error, an infinite loop, or simply does not exist.

No contract can verify this because they inspect the value and thus get stuck by infinite loops.

I don't use that sort of thing often, but here's a simpler one:

    sort :: Ord a => [a] -> [a]

I know that `sort` only uses the ordering properties of the values within the list. It could be generalized to `forall a . (a -> a -> Ordering) -> [a] -> [a]` in which case it would be totally oblivious to the values inside of the list except in that it probably applies that function.

No contract system can examine functions. No contract system can prove universals. Types can do both (in certain, principled ways).

---

Another interesting example is handling something like a channel. In Haskell, we have the type `TChan a` which is a channel carrying values of type `a`. In Clojure, the best we can do for giving a contract to a core.async chan is to say it's a "chan containing something" or even "a dereffable thing returning something". To use a contract here we'd have to check every value that ever pops off the channel.

Contracts check shape, but cannot ensure usage.

[lorddoig]

Spec isn't a type system - it's an immensely powerful abstraction for describing your data that can be leveraged for validation, coercion, error reporting, and automated test generation. This, I think, is what many of us wish our type systems could do.

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?

[tel]

> Immensely powerful abstraction

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.

[akmiller]

I didn't see him claiming that spec is better than all type systems. Obviously, Haskell has one of the better type systems. Languages like C# and Java are not near as expressive so when he says most type systems, I'd agree...spec offers more expressivity than the type systems in these languages while remaining as an opt-in choice.

[throwbsidbdk]

I donno man, the longer I use typed languages the more I hate untyped ones, if only for the IDE help alone.

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.

[moxious]

People vote with their feet, and while I'm really sympathetic to everything you're saying about static typing, it's hard to argue that reality is producing a lot of really popular dynamically typed languages. JS being exhibit #1, but also python, ruby, clojure, and on and on.

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"

[throwbsidbdk]

I'm in the opposite camp, it feels like js is mutating quickly to try to fix the rediculous problems with the language because people are forced to use it.

You don't see such sweeping changes in other languages that have been around much longer and used more widely than js.

JavaScript just got a package manager, the module system was hacked on a few years ago and still isn't standardized, the build tools change every other year and still largely suck, it still doesn't support multithreading, the object system is super wonky, it doesn't support specific float/integers which seems to break math constantly. None of these things are an issue in any other language I can think of, these features are in language V1.0

I expect developers to jump ship immediately when a replacement without these core problems reaches critical mass.

Google has been looking into this for a while, and Dart was designed with the assumption that JavaScript fundamentally sucks and can't be fixed.

This has happened before... Look what happened the perl when Python started to gain steam. It used to be pretty much the #1 way to write websites, now you would be a fool to use perl over Python on almost anything.

[aikah]

> I think of dynamic typing in a language as a big pro and a big con at the same time, but it's one of the things that makes a language like JavaScript or closure what it is.

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.

[qudat]

Yes you are missing something.

We web developers are stuck with javascript in the browser. Any proposed solution would be "bolted on" to javascript.

[grzm]

Given the rise of transpilers targeting JavaScript, "stuck with javascript" doesn't mean quite as much as it may have in the past. You could argue that this is "bolted on", but given the current state of tooling and how quickly it's improving, I don't think it's a fair characterization. I suspect this trend will only continue.

[moxious]

Here here! This transpilation thing is something relatively unique about the JS world, namely that it mutates really fast with capabilities like transpilation. Yes, it's done in other languages in limited situations but JS is the only one I can think of where transpilation is normal and standard, i.e. writing in es6 and then babelizing it to es5 for legacy nodes.

Then you add things like flow, or TypeScript, and frankly I'm losing track of exactly what it means to write in JS anyway.

[moxious]

If it's as simple as "javascript because web" as you suggest, how does that jibe with things like Electron (js desktop apps) and back-end JS without a web facing component? None of those people had to pick JS.

[k_sh]

None of them _had_ to pick JS, but many of them prefer it because they already know JS from building web apps.

The projects are different, but there's a lot of crossover in terms of the people behind them.

[amelius]

WASM will be here soon, and from that point on we can elegantly compile from any language to the browser platform.