Why we’re no longer using Core.typed
blog.circleci.com
blog.circleci.com
Other commenters are speculating that this kind of tool needs to be built into the language, and planned ahead of time. IMO, this is completely wrong. core.typed fits surprisingly well into the language, and there are no fundamental reasons in Clojure or core.typed preventing it from working well.
I largely agree with the criticisms raised in the post, but it's worth pointing out that core.typed is developed by one guy, part-time while working on his phd. The problems are all related to maturity of the project, and bandwidth. core.typed's version number is currently 0.3.11, which gives you an idea of its state.
Ambrose has shown what is possible; I'm confident that with more help, core.typed can become an amazing tool for finding bugs in production code.
This is true but I wonder how much Clojurists care about what core.typed offers. If not enough do then many there will never be enough contributors to really make it work. LightTable is a project that seems to have had something similar happen.
But it's something I rarely see featured in tool design. So many of our tools are still batch oriented: they start from scratch, read everything, process everything, and then exit. That made sense in an era where RAM and CPU were expensive. But now that they're cheap, I want tools that I start when I arrive in the morning and kill when I go home. In between, they should work hard to make my life easy.
If I'm going to use a type checker, I want it to load the AST once, continuously monitor for changes, and be optimized for incremental changes. Ditto compilers, syntax checkers, linters, test runners, debugging tools. Everything that matters to me in my core feedback loop of writing a bit of code and seeing that it works.
For 4% of my annual salary, I can get a machine with 128GB of RAM and 8 3.1 GHz cores. Please god somebody build tools that take advantage of that.
The beauty of simple tools is it's easier to make simple tools that work really really well. From loading everything at once, to considering text editors vs "IDE", which is really part of what you're talking about too. When we have new languages and platforms all the time these days... it's important to be able to get high-quality tools that don't take forever to develop.
It's trivial to get an editor right if it edits the AST directly. You skip the whole tokenization/parsing step which is where most complexity is. However, such an editor will need specific plugins for each language, and these plugins will be easier to write for languages which have a standardized AST (Haskell comes to mind). Also, users would have to give up part of the formatting (whitespace etc), and some people are very religious about that :(
There's reason we couldn't have an editor that works with the AST while saving everything out in plain text for interchange purposes.
This is an important point for tools, like type checkers, that are supposed to help deal with complexity. Type checking doesn't really matter in a small code base. The bigger you get, the more it pays off. But their type checking tool gets worse with the code base size. This is self-limiting in a way that can be fatal. If your tool doesn't matter for small code bases and it can't be used on large ones, that's a problem. It's very hard to know in advance that one's project will grow to a medium size and then stick there.
Go? They've always had this as a top level goal.
I really don't understand this distinction. My tools run those commands for me. I type in my editor, and it tells me if the compilation fails. My editor is also far more responsive and uses far less ram than the typical java IDE, so it feels faster to me, not slower.
The annoying things with Flow: No Windows support yet which is the one thing holding me back from transitioning some personal projects over, but it sounds like progress is coming there[1]. There doesn't yet seem to be any real plans for letting 3rd party NPM modules bundle their own type definitions and have them be automatically used[2]. (Flow doesn't have issues with untyped imports at least. They're just treated as the any type.) Editor integration is pretty bad still. There's an Atom plugin, but it's buggy. This doesn't affect me too much as the "flow" command for type checking is quick to use (on the first run, it starts a long-running daemon in the background which watches your whole project for changes and keeps their type information cached) in the terminal I already always have open for interacting with git.
[1]: https://github.com/facebook/flow/issues/6 [2]: https://github.com/facebook/flow/issues/593
Like, an IDE?
I mean, if you search for a string, Eclipse comes back quick because it indexed all your files. Run a grep? It comes back 6X slower (on my adhoc test)
I think other dynamic-type language communities should read this and think really hard. I've said before, I'd rather see a language become the best $LANGUAGE it can possibly be, for whatever that $LANGUAGE is, than try to bolt things on that pull it away from its core focus. Dynamically-typed languages are dynamically typed. Become the best dynamically-typed language you can be, don't bolt less-than-half-assed static typing on to the side. The sum ends up being less than the parts.
And if that means the next ten years is the language slowly fading into history... that is the destiny for all of us anyhow. Let it be with a fantastic dynamic language that was the best it could be, let it be a language that people speak wistfully of twenty years later. Don't make it be remembered as a Frankensteinien monstrosity as it tried to stay current.
On the other hand, there are instances where types are useful, even in dynamically typed languages. One of them is optimizations. The job of a compiler gets much easier if it can assume that a given variable will always be, say, an integer and nothing else.
Don't use a dynamic language when that sort of thing makes a real difference.
Native gradual typing can be much faster and assuming the language has a decent test suite, cases can quickly be added to uncover those troublesome spots.
Aftermarket gradual typing leads to a lot of information that you could use to significantly improve the performance of the language (hey, we have an int, so let's use native types instead of our language's version), but because they're not native, that typically doesn't happen.
class Point {
has $.x is rw is required;
has $.y is rw is required;
}
class Point {
subset PointLimit of Rat where -10.0 .. 10.0;
has PointLimit $.x is rw is required;
has PointLimit $.y is rw is required;
}
my $point = Point.new( x => -1.2, y => 7.3 );
$point.x = 3.14;
$point.y = -22.0; # Boom! Constraint violationThere's a set of things that are very hard to bolt on after-the-fact that aren't necessarily that expensive if you start with them. This seems to be one of them.
This has nothing to do with optional typing at all. It's just the expected problems with an early and slow (2min!) implementation of core.typed.
Other type checkers and inferencers in gradually typed languages don't have these problems, so you cannot generalize.
E.g. Optional types in Common LISP on which Clojure is based on doesn't have these problems. Scala has similar problems, but most other non-JVM based gradually typed languages not.
What about Shen on Clojure?
There are tons of papers with type checkers in the exact same early state, and how they made it fast and more reliable.
I think TypeScript is an extremely impressive tool, and a great example of considering the current environment when designing. The type system can effectively capture pretty much all API designs that see use.
We have a medium sized Typescript app (~100k lines), and it takes 7-10 seconds to transpile to JS.
Whenever a change is made, that is 7-10 seconds the watch command is running and I'm not testing my changes in the webapp.
In fact, a slow running grunt watch is why I'm on HN right now in the first place.
The who who recommended Webpack, I can't reply to you for some reason, though I will try it.
Compared with C and C++ build times which are measured in minutes or even hours, 10s is nothing.
If you fix that, then linking can take a long time too. (Not sure on the details, but it's a "global" algorithm to fix up all the pointer offsets)
Incremental builds will be slow if you structure your code in such a way that you often have to touch a header file, and that header file requires recompiling all translation units.
In short, you have to be super careful about structuring your code in C/C++ if you want fast build times, and approximately zero of the industrial codebases I've seen do this. (Well there was one, but it was all written by a single person, which is not surprising.)
Wait, is that 7-10 sec with "tsc --watch"? Or like, the whole shebang for the production build?
Programming in 2015 seems to be in this really weirdly reactionary mode to the problems of the 1990s in so many places. ("Event-based programming" as an escape from 1990s-styles threading is another one.) Umm, well, it's great that we learn from the 1990s as much as we learn from any other decade, but I'm not convinced optional typing solves the problems of 2015.
Even deciding what those "properties of interest" alone may be is very much an open question. Right now, some advanced type systems simply specify those properties that happen to be easy to infer rather than those properties that would be most valuable (i.e. cause the most expensive bugs). And, of course, you still have the halting problem fighting you at some of those most painful points.
For an interesting (though very partial) discussion of the difficulties, see Lamport's Should Your Specification Language Be Typed?[1] It speaks about specification rather than programming language, but once you decide to introduce rich type systems to programming languages (which was not so much in fashion among PL researchers when that paper was written) the problems become similar (and when he says "statically typed programming languages" he means C or Java -- not Haskell). In the conclusion he even hints at optional types:
But typed formalisms that permit automatic type checking are less flexible than set theory. The best way to catch errors may be to treat type declarations as annotations that do not affect the meaning of the specification. If the type system proved to be too inflexible, one could replace it by a different one or simply ignore certain type errors.
[1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
:) Haskell doesn't even come close. Haskell's type system is pretty much defined to be any property that happens to be inferrable by the (extended) HM algorithm. It's like: "we'll prove what we easily can" rather than "let's prove what's most useful". Sure, it may be useful in some (or perhaps many) circumstances, but it's far from the set of properties I think anyone would list when asked "what properties would you most like to verify about your program?"
For example, the two most basic tests for any formal verification system is verifying a sorting algorithm (like, say, QuickSort) and verifying a distributed algorithm (like, say, Paxos). Haskell's type-system fails to do both. Again: it cannot verify the two most common examples that people want automatic verification for. In fact, it is even too weak to verify that the monads it so depends on are actually monads. Still, it places a non-negligible burden on the developer that many would deem substantial or even onerous. And because types place some burden on the developer, you can then ask whether the set of verifiable properties is worth it or not (BTW, that any form of formal verification requires effort is pretty much a given; if it didn't, that would be a violation of the halting theorem).
OTOH, richer type systems (that include dependent types) can no longer infer everything, and they become (much) harder-yet to use.
Here are some examples of properties of interest:
1. When a request arrives at my server, a response (either a result or an error), is always produced within a given time frame. There can never be deadlocks, livelocks or starvation.
2. X and Y are two columns in my data table that must always satisfy certain invariants, and must never be observed to violate those variants.
3. My O(n) selection algorithm is correct.
4. My (sorting) algorithm requires O(1) space.
5. When a user inputs "X" the system will (or will-never) output "Y" within 5 seconds.
There are many, many more. I picked those because there are formal verification tools today that can verify all those properties (or at least many interesting instances of them). Of course, some proofs would require your computational model to be non-Turing complete, because the halting problem is real...
The other properties you mention are great! I'd love to verify them too. We'd be better off if those tools were widely used. But that's far from staying that what we have today isn't fantastic.
That is indeed very common, but it is neither the most important (it might be, but that requires evidence) nor is Haskell's particular blend of proof vs. burden necessarily the best. You could have said the same about Java, C#, Go or C, each with their own limited type "richness".
> We'd be better off if those tools were widely used
Formal verification tools that are able to prove many of the example I listed (or interesting-enough special cases) are far from being in wide use in the industry in absolute terms, but they are certainly in wider use than Haskell (in spite of the latter's popularity among bloggers), at least when it comes to large, complex software, which is where verification is most valuable anyway. Fujitsu have used JPF to verify a 1MLOC Java program[1], Amazon use TLA+ to verify/specify most (all?) of their AWS services (written in Java), some are quite complex[2], Esterel (or, rather, its descendants) is used by various realtime systems[3], and Intel uses TLA+ and/or internal verification tools to verify components in its processors. Each of those alone has seen more real-world "tough" industry usage than Haskell.
AFAICT, those tools are in wider use than Haskell in academia, too (aside from PL research, obviously), where they're sometimes used to verify concurrent/distributed algorithms (and in at least one famous case, prove the incorrectness of a much-lauded algorithm[4][5]).
It is, however, true that type-based verification tools (like Coq) have seen even less use than Haskell (they're basically unused in the industry) and other proof assistants are rarely used (a notable example is Isabelle, which has been used to verify the seL4 kernel, but AFAIK Isabelle isn't type-based, but, like TLA+, uses set-theory). Even in academia, use of type-based proofs is very rare (virtually nonexistent outside PL).
[1]: http://javapathfinder.sourceforge.net/events/JPF-workshop-05...
[2]: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s...
[3]: http://www.esterel-technologies.com/industries/
[4]: http://www2.research.att.com/~pamela/chord-ccr.pdf
[5]: http://brooker.co.za/blog/2014/03/08/model-checking.html
I still stand by the idea that these tools should be more widely used. I also don't understand a position where they're in opposition to type theoretic approaches. Liquid Haskell extends Haskell types with an SMT silver and, frankly, most logics can import a proof with ease if you're willing to trust an external party.
It certainly has types, but I don't think it bases its proofs on type theory in the same way Coq/Agda do (but I really know nothing about it, so you may be absolutely right).
> I still stand by the idea that these tools should be more widely used.
I agree. But it's important to remember that correctness is often not boolean, and is often yet another requirement, which varies across domains and projects, and with it the effort to provide it.
> I also don't understand a position where they're in opposition to type theoretic approaches.
They're not. I simply stated that type-theoretic approaches (including Haskell) have so far gained little traction, that's all. If they one day become more popular -- I'm all for it.
The problem is that proof assistants -- be they type-based or set based -- are rarely used, and the reason is that they are notoriously hard to use, and hardly ever justify the effort. That kind of effort for correctness is only justifiable in niche applications, so those tools will always be niche tools. There's just no-way, no-how you can realistically expect large swaths of the industry to adopt them (and I'm trying to be optimistically realistic rather than a wishful-thinker). Model checkers, OTOH, are qualitatively different, and are much closer to writing tests. If the industry could be trained to write automated tests (and that has contributed greatly to the rise in software quality we've seen since the nineties, when we had a "correctness crisis"), then it can be trained to write a formal spec (a "lightweight model" as Pamela Zave calls it, or an "exhaustively-testable pseudocode" as Leslie Lamport calls it) and run a model checker. It is both more applicable, much cheaper, and much more familiar than formal proofs, and so it has a real chance at adoption. Dropping costs of computation have made it far more practical, too, for ever larger models.
As soon as you want to prove anything slightly more interesting (e.g., «this nontrivial program transformation preserves the meaning of programs», or «this implementation of serializable database transactions protects the data integrity invariants of any relational database schema»), you're completely out of luck.
But, "this implementation of serializable database transactions protects the data integrity invariants of any relational database schema" can very well be verified by model checker on a finite model for some schemas (there's little reason to believe that serializability would be affected too much by schema, other than by the graph of foreign keys), and that may be enough to gain the necessary amount of confidence in the algorithm. I can certainly see distributed-database designers using model checkers for that.
«other than by the graph of foreign keys»: That's, like, the whole point to using relational databases.
We don't have such (real) languages yet[1]. Idris is far from being production ready and or demonstrating it can be effectively used for real-workd programs. Even then, it still remains to be shown that such languages will be cheaper to use than validating the translation and still be performant enough for the purpose they're used for (and, BTW, systems that require this level of correctness usually require proofs of timing and memory use -- including stack use).
[1] There is actually one such language -- Esterel. It (and its descendants) have been used to write safety-critical software successfully. It's an incredible language, but it doesn't translate well to other domains as it's not Turing complete.
We do. Because Haskell and ML are ultimately just fancy term rewriting systems, you can do equational reasoning on their terms by hand just fine. It's even easy enough for non-[computer scientists/mathematicians] (such as yours truly) to do it casually!
Esterel can't verify a sorting algorithm (as it can't even express it), but it can verify most properties that interest developers of safety-critical control systems, including timing and memory use.
More often than not, either the monad laws are easy to verify by hand (exceptions, state, nondeterminism, etc.) or the verification can be borrowed from nLab. It's a nonproblem.
As I said in another comment, there's no general technique or tool for proving arbitrary theorems, and we have to live with that. Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
And that's exactly what can be said about the difference between Haskell's and Java's type systems. It hasn't been shown that the additional provable properties -- that are not too powerful -- do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence.
> Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer.
> But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
On the face of it, proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell (or other language). There may, on the other hand, be additional tooling advantages around TLA+.
I think he was talking in monetary terms. And this is a useful point of view. While Haskell's beauty makes writing Haskell its own reward for some (at least me), from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business...
I think so too, but even then there are a lot of unanswered questions.
> from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business...
I do run a business and do believe that Haskell gives me a competitive advantage, of a sort. The interesting question is not whether this is true, but in what precise sense it is true.
Wow, nice! :-)
Yes, but you don't prove the same properties with Haskell as with TLA+ (in fact, I think that there is little overlap if any in practice). Most properties proven (well, maybe not proven but satisfactorily verified) with TLA+ (or any other sophisticated verification tool) just can't be proven in Haskell. And, again, I even prefer TLA+ to JPF (which is the tool I've had most experience with) which verifies Java bytecode directly because so far I find it more effective to verify only the core components of the algorithm. Verifying the details is usually a waste of effort (they both make the verification harder -- either harder to prove if you're doing a formal proof, or much longer to run in a model checker -- and they are easy to verify by other, informal means).
This is a little bit disingenuous, for reasons exposed below.
> do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence.
No disagreement here. I don't recall ever making any statements myself to the tone of «Haskell makes writing correct programs cheaper». But if someone else told you that, you're right - it requires empirical evidence.
> But you said "perform your proofs in the same term language in which your program is written".
And it is. Equational reasoning about Haskell programs is just using Haskell's existing reduction relation, extended with additional assumed identifications that can be used as reductions in either direction (given `a = b`, replacing either `a` for `b` or vice versa, though more often than not, only one direction is needed).
Only at the last step do we need a check that two Haskell terms are syntactically equal, which, as you say, is not doable in Haskell itself (since judgmental term equality isn't first-class), although it is trivial to do by visual inspection. The fact remains that the bulk of the work of verifying non-IO Haskell code is really just evaluating Haskell code.
> If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
I can't comment on what's best for Amazon's needs, since I've never worked there. And, obviously, there's a lot more software engineering talent working for Amazon than sitting in front of my keyboard.
That being said, I think the amount of effort required to evaluate Haskell[0] by hand is significantly less than the amount of effort required to translate back and forth between Java and TLA+.
And, for my needs (mainly implementing compilers and libraries of data structures and algorithms), Haskell is a significantly better language than Java (or Lisp, Python, C++, what have you). Precisely because I can reason about Haskell programs by just evaluating Haskell[0] by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic.
---
[0] Plus propositional equalities.
I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. For example, if you pick a recursive QuickSort implementation (just picked sorting because that's a classical verification example) and wanted to verify it in Haskell, you'll need to prove much more than equality at each recursive step (or unwind the entire computation and then prove equality, but that's not a very convenient proof). Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach).
Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell, and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java.
There are some interesting uses of Haskell's logic, such as session types (also possible in Java, BTW), but they are too underpowered to prove any distributed algorithm of interest (AFAICT, they are exactly as powerful as regular expressions).
What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. So it is the features of a certain algorithm which determines the language's semantics rather than an analysis of what's helpful. Good examples of the latter approach would be Java, Erlang and Clojure. (BTW, a good explanation of Java's design decision is in the first 17 minutes or so of this talk: https://www.youtube.com/watch?v=Dq2WQuWVrgQ)
That is somehow (if you squint) similar to Prolog, whose utility was determined by the quality of it search algorithms. Such approach makes for great research, but its industrial applicability is very brittle.
> Haskell is a significantly better language than Java ... Precisely because I can reason about Haskell programs by just evaluating Haskell by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic.
Even if I were to accept that premise, that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features).
EDIT:
Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; lambda substitution is a very mathematical concept).
To make this more concrete, recursion is limited assignment, and recursion combined with a continuation (or, in Haskell, a continuation monad) is imperative assignment (imperative state can be fully implemented in a pure language with continuations and recursion). So substituting across the cont monads is directly more complicated (computationally -- it requires lots of reductions) than state simulation of the very same computation.
[1]: But, forgive me, so is Java.
Now, don't get me wrong: I'm all for Clojure-style, ML-style or Rust-style immutability-by-default (each, of course, is different as they all have different tradeoffs), but that's completely separate from purity.
In those cases, one possible strategy is to take a detour via auxiliary data types, which aren't declared in the program, but are isomorphic to types that do. For example, lately I've been working quite a lot with data structures based on skew-binomial numbers (zippers, lenses and traversals for skew-binomial trees and heaps). Their usual implementation is as linked lists of increasingly weighted trees, except for the first two ones, which may have the same weight. In my proofs, however, I work with an isomorphic type with two constructors: one for the case where the weights are all strictly increasing, another for the case where the first two trees have equal weights. This is no different from performing mathematical induction on Peano naturals, but using machine integers or big integers for actually performing arithmetic operations.
> Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach).
Most algorithms that interest me are data transformations - some sequential, some parallel, but almost never concurrent. And, even in those few cases where the interleaving of concurrent computations actually matters to me (e.g., implementing serializable transaction support in a RDBMS that works for any valid schema), I highly doubt that the tools you mention have anything useful to offer, although I would love to be wrong here.
> Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java.
For things like protocol verification, I'll take a substructural type system, like those of Rust and ATS, where non-forgeable, non-duplicable tokens are used to reify the states and transitions concurrent computations may undergo. This still offers an easier, more integrated workflow than translating between two different languages.
> What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience.
My analysis of what strength is needed is very simple: If the computer can do something perfectly, let it do it. If the computer can't do it perfectly, I'll do it myself. I have no taste for automated mistakes that have to be manually rolled back, such as program analyses whose results I can't fully trust. HM-style (or, more generally, ML^F-style) type reconstruction just happens to be something that a computer can do perfectly.
> Even if I were to accept that premise, [that equational reasoning about Haskell programs is just normal Haskell term reduction]
What part is hard to accept?
> that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]).
Yep, only some aspects. Exactly the ones I happen to need to write correct programs - and prove them so.
> A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions.
Perhaps I'm just too noob, but I'm really happy that I don't need to care about tuning the behavior of a managed language's runtime system. It's too much of a black art for me to want to have anything to do with it. If performance ever becomes that much of a problem, I'll just call Rust or C++.
> But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features).
I find my productivity when using Java even lower than when using C++, which is a really impressive achievement, considering that C++ is such an unproductive language. C++ supports (to a limited extent) and encourages (to an even more limited extent) a programming style where variables actually stand for legitimate values inhabiting your problem domain (varying between assignments or member function calls, of course). These values can be manipulated using equational reasoning. In Java, every non-primitively-typed variable stands for an object reference, which is effectively a reification of the time and circumstances in which the object was created, and most certainly not something I care about. So, when it comes to actually producing proofs of correctness of Java programs, I need to jump this additional layer of indirection between variables and the values I care about. Back and forth. Over and over.
> Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine.
Of course term rewriting is computation - if it weren't, it would be useless as a theoretical basis for programming languages! But «equivalent in raw power» doesn't imply «equally convenient to use». Models of computation based on term rewriting happen to be easy to reason about in a compartmentalized, divide-and-conquer manner than Turing machines.
> So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers).
I've burned way too much time in debugger sessions that could've been usefully spent doing anything else, like writing programs that don't need to be debugged, or simply enjoying life. I don't think the value I got from them justifies the cost of opportunity. Never did a debugger session give me full confidence that the program I've written is correct. Even worse, debugger sessions seldom told me where exactly my program (as in, the code, not the running process) is wrong.
> I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time;
Speak for yourself.
> lambda substitution is a very mathematical concept).
What do you mean by «lambda substitution»? A bound variable (by any binder, such as lambda, mu, forall and exists) cannot be substituted - you need to extract the term under the binder first. If you mean «variable substitution», yes, of course it's a mathematical concept.
If you're interested in formal proofs, I suggest you read the discussion Should Your Specification Language Be Typed?[1] by Leslie Lamport (Paxos, TLA+) and Lawrence Paulson (ML, Isabelle). It is very balanced and discusses the relative pros and cons of typed and untyped proofs for formal verification (the closest they come to making a specific recommendation is exploring pluggable optional types).
> If the computer can't do it perfectly, I'll do it myself. I have no taste for automated mistakes...
You're talking about false positives, while a better approach might be to allow false negatives (as Idris does), i.e. a program doesn't typecheck without additional proof.
Alternatively, if you want the computer to do its work automatically, why stop at a simple type-checker that runs for a few seconds? Why not let the computer run a model checker for a few hours and verify some much more interesting properties? It doesn't deductively prove correctness, but it certainly increases confidence much more than testing, and it's orders-of-magnitude easier to use than any proof assistant (the authors of the seL4 kernel spent 30 man years proving 7500LOC with a theorem prover!); it's probably as easy or easier than coming up with your auxillary types.
> What part is hard to accept?
That equational reasoning is always more convenient for people than state simulation.
> Exactly the ones I happen to need to write correct programs - and prove them so.
I do that in Java. Haskell only brings you marginally closer to the correctness of a sorting algorithm than Java does (if at all) anyway. If I need more formal verification, I use a model checker (JPF in the past, now I'm about to switch to TLA+). It feels more natural for me than using types for proofs. I've found that using a model-checker that works directly on the Java code (like JPF) is not an advantage in terms of total effort over one that uses a separate specification language, especially one that's as (relatively) simple as TLA+/+Cal. I haven't tried KeY, though (also works on Java code, but uses symbolic execution; gained some publicity recently when it found a bug in a complex sorting algorithm -- in fact, possibly the world's most used sorting algorithm).
> but I'm really happy that I don't need to care about tuning the behavior of a managed language's runtime system... If performance ever becomes that much of a problem, I'll just call Rust or C++.
That's more myth than reality. HotSpot without any tuning whatsoever performs better than pretty much all managed languages. Tuning is required if you need to really come close to C-speeds, and in those cases it still requires far less work than C. But that's a whole other discussion.
> I find my productivity when using Java even lower than when using C++
I can believe that, but I was a C++ programmer for a decade before switching (primarily) to Java -- at first quite reluctantly -- and my productivity soared. However, I wasn't talking about anecdotes or personal experience. It is a proven fact that the productivity of the industry at large jumped considerably (estimates are 2x-3x on average) when it switched from C++ to Java.
> But «equivalent in raw power» doesn't imply «equally convenient to use».
Exactly.
> Models of computation based on term rewriting happen to be easy to reason about in a compartmentalized, divide-and-conquer manner than Turing machines.
True, but no one programs Turing machines. Whether term-rewriting is more convenient than mainstream imperative or imperative-functional (i.e. Clojure, ML, Erlang) requires empirical evidence which is so far sorely lacking.
> Most algorithms that interest me are data transformations - some sequential, some parallel, but almost never concurrent.
Ah, that explains it. I mostly do concurrent/distributed algorithms (I build concurrent, distributed in-memory databases).
> I highly doubt that the tools you mention have anything useful to offer, although I would love to be wrong here.
So you'll be happy to learn that you are wrong! TLA+ and friends have been used to verify lots and lots of concurrent and distributed algorithms (as well as hardware cache-coherence protocols) like Paxos, Raft,(fixed) Chord, and many, many others. See [2] and Lamport's Checking a Multithreaded Algorithm with +CAL[3]
[1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
[2]: http://brooker.co.za/blog/2014/03/08/model-checking.html
I'm not interested in «balance», because this isn't a political debate, and my formal system choices don't affect anyone but me. What I do care about is convenience: not having to translate between formal systems, ruling out as many unwanted behaviors making as little effort as possible.
And the arguments in the paper in favor of the «flexibility» of untyped systems are really arguments for sloppiness. To see why a more constructive approach is better, using an example from the article, instead of saying `i - j >= 0`, I would just say `exists k. i = j + k`. This means that the witness that `i - j >= 0`, namely, their difference `k`, can be used throughout the rest of the proof without recomputing it over and over.
> (the closest they come to making a specific recommendation is exploring pluggable optional types).
I've never found optional types worth the trouble, precisely because they run into the same issues as CircleCI has experienced with core.typed: they greatly constrain typeless exploratory programming, and bring in few of the benefits of typeful exploratory programming.
> I do that in Java. Haskell only brings you marginally closer to the correctness of a sorting algorithm than Java does (if at all) anyway.
For something like a sorting algorithm, I'd just carry out the proof by hand.
> If I need more formal verification, I use a model checker (JPF in the past, now I'm about to switch to TLA+). (...) I've found that using a model-checker that works directly on the Java code (like JPF) is not an advantage in terms of total effort over one that uses a separate specification language, especially one that's as (relatively) simple as TLA+/+Cal.
I'm not going to question your experience. But all of this still seems like a lot effort to me.
> That's more myth than reality. HotSpot without any tuning whatsoever performs better than pretty much all managed languages.
I never compared HotSpot's performance with any other managed runtime. Mostly because it never gets to the point where a performance comparison matters - I don't care how fast a runtime system is if it's too hard to write correct programs that run on it.
> Tuning is required if you need to really come close to C-speeds, and in those cases it still requires far less work than C. But that's a whole other discussion.
I never said C. I'm not willing to give up the ability to define my own abstractions in a statically verifiable and enforceable manner.
> True, but no one programs Turing machines. Whether term-rewriting is more convenient than mainstream imperative or imperative-functional (i.e. Clojure, ML, Erlang) requires empirical evidence which is so far sorely lacking.
Standard ML, with a subset of its reduction relation, is a perfectly usable term rewriting system. One just needs to be aware that, while types as collections of values are sets, types as collections of terms are just presets - not all terms are equal to themselves.
> So you'll be happy to learn that you are wrong! TLA+ and friends have been used to verify lots and lots of concurrent and distributed algorithms (as well as hardware cache-coherence protocols) like Paxos, Raft,(fixed) Chord, and many, many others. See [2] and Lamport's Checking a Multithreaded Algorithm with +CAL[3]
I've never seen a convincing demonstration of how those algorithms (or anything in the distributed computing literature) can handle concurrent data structures with interesting invariants. All I see when I read those protocols is how to synchronize a single integer or something equally meaningless.
The model checker verifies this for you whether you're "sloppy" (most mathematicians wouldn't call it sloppy; just those that work in typed logic systems) or not.
> I'd just carry out the proof by hand.
Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand (see http://www.envisage-project.eu/proving-android-java-and-pyth...). And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong. Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord). Those algorithms had proofs, but the proofs were wrong: http://brooker.co.za/blog/2014/03/08/model-checking.html
If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. Lamport has written quite a bit about the difficulty of proofs for modern algorithms.
We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand.
> But all of this still seems like a lot effort to me.
It took 30 man years to deductively prove 7500 LOC with a theorem prover! It takes a few days to spec and verify Paxos or fixed Chord.
> if it's too hard to write correct programs that run on it.
There's a Haskell dialect on the JVM and a good (multithreaded!) OCaml implementation.
> All I see when I read those protocols is how to synchronize a single integer or something equally meaningless.
That's because those are the examples that fit in a tutorial. Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol: http://research.microsoft.com/en-us/um/people/lamport/tla/wi...
And here are all the verification annotations used to find and fix the TimSort bug: http://www.envisage-project.eu/proving-android-java-and-pyth...
So I just stick to simple data structures and algorithms for the most part. I don't see a real need for something as complex as TimSort, when quicksort and mergesort (or even insertion sort!) are perfectly good algorithms that any high-schooler with a modicum of mathematical talent can understand. It's totally ridiculous to need an automated theorem prover to verify a sorting algorithm.
> And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong... Lamport has written quite a bit about the difficulty of proofs for modern algorithms.
How often were these proofs formal proofs? By which I mean that the definitions and theorem statements are just pieces of syntax in a formal system, and that the associated proofs are just calculations driven by the formal system's rules?
> Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord).
I would never assume an algorithm is correct just because it appears on a paper authored by famous people, or because it's widely used in industry. (You wouldn't do drugs just because famous and rich celebrities do, right?) So, unless the proof of correctness of an algorithm is so trivial that I can find the proof on my own given a couple of hints, I will demand fully formal proof. (Yes, this means that the typical CS paper, especially the typical concurrent/distributed computing paper, doesn't convince me of its thesis.)
> We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages.
They're typically that long because they're written in a mix of natural language and mathematical notation, where the former attempts to convey intuition in order to make up for the latter failing to provide rigor.
> There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand.
Agreed. Once we have accepted complexity in our designs, nowhere can salvation be found. So just say no to gratuitous complexity.
> There's a Haskell dialect on the JVM
Nice. Will check.
> and a good (multithreaded!) OCaml implementation.
I don't care. OCaml is an ugly language.
> Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol
Any examples that a non-hardware person can appreciate? (Preferably databases, but operating systems would also be okay.)
It's not ridiculous when billions of dollars pass through programs using your sorting algorithm, and any improvement can matter (and there can be big differences).
> How often were these proofs formal proofs?
Do you know what percentage of algorithms have formal proofs? About 0.
> Agreed. Once we have accepted complexity in our designs, nowhere can salvation be found. So just say no to gratuitous complexity.
I've been in this industry for 20 years now, and I started out saying this, and now I hear this from others. That is obvious. Sometimes you deal with inherently complex problems. I was in the defense industry for a long time, and air-traffic control is a complex problem.
> Any examples that a non-hardware person can appreciate?
Sure. Follow the links here: http://brooker.co.za/blog/2014/03/08/model-checking.html
Also, Amazon specified Dynamo (939 lines in TLA+) and their internal distributed lock manager (mentioned in this report, with the number of lines and the kinds of bugs found: http://glat.info/pdf/formal-methods-amazon-2014-11.pdf) but I don't think they've made the actual specs available.
There are more popular languages that are faster than Haskell, languages with better tooling, and languages that are easier to learn and faster to write and read code. Haskell's claim to fame and the justification for its learning curve is verification (both formal and informal). Therefore, I think it's reasonable to compare it with verification tools.
> Haskell's claim to fame and the justification for its learning curve is verification (both formal and informal).
I think Haskell's claim to fame is being a pure language (and maybe its laziness). I don't know what languages you had in mind, but Haskell's learning curve is usually also related to people not being familiar with functional programming as a paradigm.
How would you characterize verification, then? (and remember, most verification methods aren't proofs)
> I think Haskell's claim to fame is being a pure language
Sure, but why would you want to use a pure language? I mean, you could say that any programming paradigm is intellectually interesting, but some people seem to think that using Haskell actually has some real advantages. What are those advantages? Performance? Readability? Sure, some believe it results in more maintainable code, but I think that the most common praises are "helps to reason about code equationally" -- which is informal verification -- or "helps write more correct code faster due to the rich type-system" -- which is formal verification (BTW, I say "believe" and "claim" because unfortunately we don't yet have any significant evidence to speak with confidence regarding Haskell's benefits in large, challenging real-world software because it has hardly been used in any yet).
> Haskell's learning curve is usually also related to people not being familiar with functional programming as a paradigm.
Partly, but I was quite familiar with FP (Scheme, ML) when I started learning Haskell, and there's a very steep curve (steeper than going from Java to OCaml).
No it's not. It's an informal probabilistic statement based on induction, not formal reasoning based on deduction. Stop trolling.
Formal verification is not the same as deductive proof. Some formal methods produce "probabilistic statements based on induction".
What is it that motivates you, at the same time as introducing interesting and pertinent details to a discussion, to be so negative and condescending about other people's choice of technologies?
You are clearly very intelligent and well educated. Why do you feel the need to do this? I can't for the life of me understand where this is coming from. Do you not realise how aggravating it is for the other parties in the discussion?
You have plenty to contribute by mentioning interesting technologies like TLA+ and your threading implementation. Why do you have to dump on other people at the same time?
An easy way to both start and win an argument!
No it doesn't. Troll.
Oof, that hurts. You hit us right in our sensitive areas.
* The Constructive Semantics of Pure Esterel (1999): http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2...
Both by Gérard Berry (https://en.wikipedia.org/wiki/G%C3%A9rard_Berry)
#2 can also be done by writing a custom type for the table row e.g. MyType and a function mkMyType :: columns -> Maybe MyType that never produces a result if the invariants are not satisfied, then updating your data access layer to only allow MyType to be used in insert/update commands. Or is that not sufficient?
#5 is similar to #1 but easier because of the missing deadlock/starvation requirements
Don't know about #3 and #4
edit: What I'd really like in Haskell are Elm style extensible records [1] to replace the glorified product types with auto-generated functions. Everything else seems really great to me
I don't think you can have a monad that tracks total time at compile time without dependent types (you might be able to do something like what I think you're suggesting with C++ templates, but even that would be rather limited), and STM is neither a verification mechanism nor an artifact of the type system -- it's an algorithm providing a useful abstraction, not unlike a GC (don't get me wrong, it's a great solution in some cases -- Clojure has it, too -- but it's orthogonal to Haskell's other abilities).
> #2 ... then updating your data access layer to only allow...
That's architecture -- not verification -- and no different from saying we'll keep X and Y as private members of a Java class, and only allow modification through a single public method which we mentally "prove" to preserve the invariant.
Obviously, people write software that fulfills similar specifications all the time and those systems work, so we know how to write them (using architecture, care and appropriate algorithms). Formally verifying them is a different story.
given the axiom "mkEmail :: String -> Maybe Email` always produces Nothing when the email is not correct, and given that other Email constructors are not available"
then the `Email` type is guaranteed to contain a valid email address anywhere in the code.
At least that is where the value is for me - the type system freeing me from reasoning about the same preconditions everywhere, over and over again - as well as warning me when I violate them while changing the code. Is that not enough? :)
Enough for what? Proving the correctness of a sorting algorithm, a distributed algorithm or pretty much any algorithm? Or proving that your request scheduling is fair and free from various failures? No, I'm afraid it isn't. :)
Enough for preventing the most expensive bugs? Well, that requires evidence, but I have the feeling that the answer to that is also no.
It's certainly good for many, more modest things, but the guarantees you happened to mention are as easily achievable with much cruder type systems in much more popular and better-supported languages, too (your own example is the same as having the Email class's constructor throw an exception in Java/C++/C# for invalid emails; that would guarantee that all Email instances are valid).
The question is, is the extra type-expressivity afforded by Haskell -- which is richer than cruder type systems but falls short of other, more popular verification approaches -- worth the extra effort? Unfortunately, at this point in time we can only answer this question based on personal preference and anecdotes.
Runtime is too late to find bugs.
Additionally, I believe that the effort required to write Haskell code is vastly over-estimated. Its not harder than other languages - just different enough that a lot of knowledge doesn't transfer.
Perhaps, but so is the ability of Haskell to produce more correct program more cheaply.
The Haskell type system is really not powerful enough to verify even the basic monad properties, let alone a simple sorting algorithm. OTOH, you can eliminate null-pointer errors with much simpler type type systems than Haskell's (e.g. Kotlin's). Haskell's type system exists at one point on a spectrum, Java's at another and Kotlin at yet another (but close to Java). It has not been shown which point results in less total development cost, nor that there aren't any other points with better results. Also, none of those was contrasted with a hybrid approach that has proven useful at Amazon (write code in Java, verify in TLA+).
> for one, in Java null can be assigned to any type.
Not with Java 8's pluggable type systems (which are quite advanced, BTW): http://types.cs.washington.edu/checker-framework/current/che...
> There is a difference between the inability to prove certain things and having giant holes in the type systems that nullify most guarantees.
I don't know if the distinction is so clear. Type systems aren't axiomatically "good". They exist to serve a purpose, and they come at a cost. Both purpose and costs are points on a scale, so one cannot simply make the general statement that a "sound type system is better than an unsound type system". All you can say about it is that it's sound. Whether it's "better" or not requires some empirical study.
* proportional to the number of constraints you can express with it (that you're interested in)
* inversely proportional the effort necessary to express those constraints
* inversely proportional to the number of lies it tells (times probability to encounter a lie)
Assignable nulls is an example of a type system lying. It lowers the guarantees without reducing the burden. The more you rely on that lie being the truth in your code, the less useful the type system is in preventing bugs in your code.
`null` is a pervasive hole as every time you invoke a method on any object, you may actually be throwing a null pointer exception
Checking for null every time will help - now we have the guarantee back. However then we get to another hole which is caused by shared mutable state: if you check for nulls by the time you get to executing the method inside the block the reference may become null.
Luckily, this doesn't pertain to code that doesn't deal with shared mutable state, so this "unsoundness" is less "bad" i.e. more avoidable than the previous one. However in the presence of concurrency, immutability or the inability to share mutable state become another useful constraint.
So its simply a question of how much potential certain lie has to cause problems in your particular code or domain. For example, the answer for `null` is pretty much "most code". The answer for "bivariant function types in TypeScript" is "a lot less, but here are cases X Y and Z and they are common in our code, and here is how to avoid it.."
But yes, I agree that its not a binary unsound vs sound. And I do prefer type systems where I can say "trust me, this results with the type I say it will" when its not possible to express it otherwise. I'm okay with lying to the type system: just not okay with it lying to me.
While your points may be valid, this may not be a great example.
To be fair, core.typed is a completely independent, optional library- It does in no way detract from the dynamic nature of the language or affect you in any way if you simply refrain from including it in your project.
I've found the syntax a little arcane, particularly for coercion (which is a secondary function of Schema) but the documentation benefits have been worth the effort of learning it.
A nice middle ground between nothing, and full-blown type annotations.
Before TypeScript 1.1, the intelligence was quite slow, but is now fine even for large projects. Third party libraries often have type definitions in the DefinityTyped collection.
That just leaves constructs that work in JavaScript, but which can't be type checked in TypeScript. This is often double-edged. TypeScript's types are not amazingly flexible, so it encourages writing less magical code, improving readability, but it also discourages some patterns that are quite useful, such as passing references to properties using string key names, which are hard to type-check.
you can "cast" anywhere so it's not really an issue :
(<(string)=>string>baz['baz'])('foo')
Otherwise typescript support union types and such ... Even without .d.ts headers everywhere it is still useful. I prefer it to babel and co as it is easier to track ES6/7 integration. Never used typed clojure though ,but I don't know any example of a language that didn't have types before and retrofitted type safety without any issue and breaking backward compatibility.
Not having type-checking doesn't necessarily make Clojure any less awesome for me though. I write unit tests, add (some form of) contracts at least to the public functions and pay attention to documenting public stuff. And not doing excessively clever things like having unnecessary mini-DSL's within the code also help.
The workaround I've found is to use a plugin [1], which converts the type annotations into runtime checks. It's not perfect, but I've found it helps catch some bugs quickly. It's also really helpful for documentation purposes: you know that this function param takes a number param, if you're not passing in a number you've made a mistake. Also, having the inline type is nicer than having it in a jsdoc-style comment above.
I think there's diminishing returns as you add more annotations to your code and you make them stricter, but having basic sanity checks has been helpful in catching stupid mistakes quickly.
[0] http://flowtype.org/ [1] https://github.com/codemix/babel-plugin-typecheck
Overall babel seems to be moving in a direction which I'd consider really interesting. With babel 6 you'll be able to write a plugin to add runtime checks that aren't limited to module boundaries.
I wonder how many other premature "you should too"s have been issued over the years. At least they had the guts to retract theirs.
Even though I no longer use Clojure much and prefer to work in languages designed for static typing (e.g. Haskell) I don't regret my donation. It is an ambitious project and I'm glad someone had the courage to take it on.
--------------------------------------------
The problems that we have hit with using Typed Closure are
1.) slower iteration time when programming,
2.) core.typed not supporting the entire Clojure programming language
3.) using third-party libraries that have not been annotated with core.typed annotations
--------------------------------------------
If #1 is caused by #2 and #3 then presumably #1 will get better with time. But if #1 is caused only by typing itself, then it sounds like, for them, using types was a bit of premature optimization.
It does raise the question, is it possible to create a type system that does not slow a project down?
This, incidentally, is one of the reasons I like Perl 6 (http://perl6.org/). It also has gradual typing, but if a third-party library doesn't have a type annotation, that's OK: it will simply fail at run time instead of compile time.
Another reason to like native gradual typing instead of third party gradual typing is that it can be integrated natively into the system instead of being used as an afterthought. Perl 6 has native type infererence to allow for compile time failures:
$ perl6 -e 'sub foo(Int $x) { say $x }; foo("bob")'
===SORRY!=== Error while compiling -e
Calling foo(str) will never work with declared signature (Int $x)
at -e:1
------> sub foo(Int $x) { say $x }; ⏏foo("bob")
What happened above is that the optimizer saw that the call to foo() requires an Int and checks the argument type to see if the call is allowed.
And here's the untyped version:
$ perl6 -e 'sub foo($x) { say $x }; foo("bob"); foo(3)'
bob
3
$ perl6 -e 'sub foo(Int $x) { say $x }; my $name = "Bob"; foo($name)'
Type check failed in binding $x; expected 'Int' but got 'Str'
in sub foo at -e:1
in block <unit> at -e:1
$ perl6 -e 'sub foo(Int $x) { say $x }; my Str $name = "Bob"; foo($name)'
===SORRY!=== Error while compiling -e
Calling foo(Str) will never work with declared signature (Int $x)
at -e:1
------> t $x) { say $x }; my Str $name = "Bob"; ⏏foo($name)
Typed and untyped code must (and will soon) be able to cooperate in providing compile-time and run-time type checking in Clojure.
There was a post about it, but the best I could find is a recent paper: http://frenchy64.github.io/papers/typed-clojure-draft.pdf
I think the tooling integration is better in Typed Racket, although Ambrose has made some improvements in Typed Clojure as well. As for typed versions of existing libraries, I think that things are bit better in Typed Racket, but also Racket has many fewer libraries than Clojure at the moment, so the scale of the problem is smaller.