* Javascript has Flow/TypeScript
* Python has PEP 484
* Perl6 has some sort of types
* Clojure/Script has core.typed, schema and now clojure.spec
* Don't know about Ruby, but I've seen articles on type checking/annotations
* Erland has Dialyzer (although this is not a recent development)
1) could actually be any language that doesn't fit the mainstream mold
He acknowledged the deficiency, but worked through it to understand what the problem actually is. Then he created a solution that solves the real problem, in a way that avoids diminishing the character of the language.
Have a read through the rationale on the design of clojure.spec to see what I mean.
- lexical closures
- common set of base types (lists; dicts; sets)
- literals for said types
- immutability
- generators
- asynchrony
So yes, types do get in the way while prototyping but it's great to have them available when refining code.
And types can also help you prototype and then polish rough ideas. For example, I'm exploring a programming style where no unreachable code paths are allowed: in a circumstance where you'd throw an exception or return an error sentinel, I'd refactor the code to eliminate the unreachable branch. This means that abstractions must have the “right shape” (that is, not leak), and types are fundamental to make this work.
When I start adding type annotations, I'm usually aiming for a speed-up but more often it leads to reorganization and rationalization of the code. The code becomes more streamlined and beautiful.
The post below resonates with me. He calls it 'programming by teaching', where you gradually shape a program to solve your problem. I think of it as 'programming by learning', where the Lisp way of developing helps me learn about my problem. It's only when you have the final version of your code that you fully understand the problem by seeing its solution in front of you.
(0) Nominal types correspond to primitive domain entities.
(1) Structural types correspond to compound entities, built from simpler ones.
(2) Abstract types regulate the interaction between different subdomains of a larger domain.
The net result is that the REPL's feedback helps me identify those parts of the problem domain where my understanding is weak. Not only the REPL's feedback, of course. For instance, if my program contains unreachable code paths, it means that I haven't yet found the right abstractions.
The philosophy behind this methodology is that:
(0) The cost of having a wrong program is actually larger than that of having no program, because it takes too much effort to identify the wrong parts so that one can fix them.
(1) When the size a program exceeds a certain threshold, it becomes impossible for ordinary human reasoning to determine with full certainty that a program contains no errors. Only formal logic can help, and only machines can do formal logic at a large scale.
(2) It isn't practical to tackle large problems without a properly enforced separation of concerns.
---
By the way, ironically, I never make an explicit type annotation, except perhaps, perhaaaps, at module boundaries. Figuring out the boring details of how to connect the pieces of a puzzle is a job for computers (type inference), not humans.
This is not an example of language moving to gradual typing. Typescript is an entirely new language.
The good: it uses a structural type system. For someone who got the good old 'JavaScript is a toy language you should try Java or C#' at university, this feels really refreshing. It mostly works as JS and you get some nice auto complete. So it feels dynamic and not clunky, like the aforementioned 2 'true' languages.
The bad: the tools seem to work random. Sometimes they pick up the definitions, next time you open a file, 'cannot find module 'react'' or numbers in import paths break the auto complete etc. also often you don't find type definitions for you libs and as a type-n00b you often lack the skills to create good ones yourself.
Anyway, I hope with TS 2.0 things will get better. Especially with strict null checks, which hopefully will be a giant win.