But what about then gradual typing in core.typed? Will it make core.typed more useful? Or is problem not just in gradual typing but more in type oriented system vs data oriented system?
The issue I have with gradual typing in most languages is that it's added after the fact and not native. As a result, the integration isn't native and you start seeing issues like this.
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")
(Yes, that's compile time instead of run time)
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
Interestingly, the Perl 6 core team could allow for powerful type inference with this, but one of the core issues has always been that many languages using type inference have rather opaque error messages because they essentially dump a "proof" of type failure and many struggle to understand them. Thus, the the Perl 6 devs are taking more careful approach, though they know they can do more. For example, this falls back to a runtime failure instead of a compile time failure:
$ 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
In other words, because it's not sure of the type of $name at compile time, it falls back to run time (though in the simplistic example above, that's clearly not the case). Annotate the $name variable and you get a compile time failure again:
$ 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)
With this, third-party libraries which don't declare types work just fine, but you get type-safe run time failures. If they do declare types, you often get compile time failures (though it will still fall back to run time, and won't check at run time if it knows at compile time that it works).
There are also tentative plans to integrate core.typed with the Clojure compiler so type annotations can be used during compilation (e.g., type hints through inference).
Interesting to compare with TypeScript, which runs into similar issues.
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.
> TypeScript's types are not amazingly flexible, so it encourages writing less magical code (...)
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.
That... is pretty much exactly the list of problems I've expected out of optional typing.
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.
> 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.
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.
Often the point is that it mostly doesn't, and then in a few rare cases (hot inner loops at scale discovered via profiling) it suddenly does. You can rewrite the inner loop in a different language and call it via FFI... or you can type-annotate it. Which is simpler?
When it's native to the language, it's awesome. When it's bolted on as an afterthought, you get articles like this.
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.
I can't say, but I love what Perl 6 has done. For example, here's a Point class, with read/write, mandatory attributes:
class Point {
has $.x is rw is required;
has $.y is rw is required;
}
Like many dynamic languages, there's nothing to stop you from assigning the string "foo" to one of those attributes, so let's fix that, but go even further and constrain the X and Y coordinates from -10.0 to 10.0. (Note that a "Rat" is a rational number, so it's perfectly precise and doesn't suffer from floating points imprecision):
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;
}
So what that's done is allowed the dev to declare a new type, PointLimit, on the fly. It must be a number from -10 to 10. And then we have our X and Y attributes:
my $point = Point.new( x => -1.2, y => 7.3 );
$point.x = 3.14;
$point.y = -22.0; # Boom! Constraint violation
It would certainly be better if it were in there from the beginning.
There'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.
Not at all. This is the list of problems that exist with an overly slow, early and incomplete type checker.
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.
No. It has a sparse (and I'm being extremely generous with sparse) standard library. Almost everything you do is FFI, which if you want to type, is a PITA.
I disagree. Typescript is an excellent example of an optional static type system that works great. It has none of the 3 problems the OP describes: it's fast, it nicely encompasses the whole language and the Definitely Typed repository includes a TON of 3rd party library type definitions.
It's competitor from facebook (http://flowtype.org/) is also really fast during development as well, even for sweeping changes across big sections of the code base.
agreed on TS, we're using it extensively in production to great effect.
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.
The article's code base is also ~100K lines (of clojure) and the type checker runs for 2 mins, so it feels safe to say that Typescript's checking is an order of magnitude faster, right?
A lot of the bottleneck is the header structure: the size of the translation units (.c files with headers expanded transitively) is often quadratic with respect to overall codebase size.
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.)
That also depends massively on the used libraries and the structure of the code. A 100kloc c file could build superfast. Whereas multiple c++ totalling about 10kloc that include use use lots of Boost stuff can take ages compared to that.
That's a ton, you're probably not using typescript incremental compilation feature but recompiling your whole codebase instead. Even in that case, 7 seconds for compiling a 100k LOC code base is not even close to what I call "slow".
First of all, adding optional static typing is not "trying to stay current". You may be surprised (I certainly was), but at the last ECOOP it was very clear that the typed/untyped/optionally-typed debate is very much alive and well. Second, optional typing in itself is a hot topic (regardless of the merits of static typing), with some very interesting work. See, e.g. the extremely-powerful-but-not-yet-production-ready pluggable type systems supported by Java 8: http://types.cs.washington.edu/checker-framework/current/che..., or Gilad Bracha's optional types in Dart.
I'm generally underwhelmed with the whole idea of optional typing in general, because it seems like a solution to the problem of sucky static type systems. The solution is, static type systems that don't suck. If you have that, optional typing seems a lot less interesting.
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.
The search for type-systems-that-don't-suck is very much ongoing and there's no solution in sight. You need to find one that is 1/ understandable and palatable to the human mind, 2/ powerful enough to specify properties of interest and 3/ can be inferred as much as possible to reduce effort.
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.
> I think Haskell's type system satisfies your list of requirements.
:) 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...
I think the very most common property of programs I or anyone ever deals with is handily covered by Haskell's type system: "do these two (often complex) things fit together?"
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.
> I think the very most common property of programs I or anyone ever deals with is handily covered by Haskell's type system: "do these two (often complex) things fit together?"
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).
Isabelle is definitely type-based by any definition I could think of. Really it's more of a logic and TLA+ is model checker. If we want to do model checking then SMT solvers are in every half-sane dependency manager on the planet verifying build sets.
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.
> Isabelle is definitely type-based by any definition I could think of.
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.
Model checkers, OTOH, are limited in scope, and can only work with finite domains, and, furthermore, is usually restricted to first-order reasoning on them.
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.
Oh, certainly! But I still see little chance of proof assistants being used in the industry for anything but the most exotic niches. They're just too hard and time-consuming to use. Academics might certainly use them to prove algorithms as they prove algorithms now (although, at present, I also don't see too much realistic chance of algorithms requiring proof-assistants for their proof being implemented in the industry; as it is, even informally-proven algorithms that are complex enough and hard-enough to implement are avoided, and very few niches can afford translation validation for their implementation[1])
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.
«few niches can afford translation validation»: So, as long as you can avoid it, don't translate. Perform your proofs in the same term language in which your program is written.
«other than by the graph of foreign keys»: That's, like, the whole point to using relational databases.
> Perform your proofs in the same term language in which your program is written.
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!
Like I said above, Haskell/ML's type systems don't even come close to verifying most interesting program properties. They can't even verify a monad, let alone the simplest sorting (or selection) algorithm. All those software verification tools most certainly can, and even much more interesting properties/algorithms than that.
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.
«can't verify a monad» (probably you meant «that the monad laws hold»)
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+)?
> result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem
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 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.
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.
> proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell
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).
I've only dipped very shallowly into TLA+ and haven't had time to investigate, but I have been wondering if we can leverage Haskell's type system to make sure we're matching the abstractions we've assumed for TLA+ at a low cognitive overhead.
> And that's exactly what can be said about the difference between Haskell's and Java's type systems.
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.
> Only at the last step do we need a check that two Haskell terms are syntactically equal
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 ...
Many things I could respond to, but out of convenience I'll just note that there's a reason why nobody programs in Haskell in the Cont monad unless they really can't avoid it!
Sure, just as there are reasons people write simple pure functions in Java when that's the best approach, and they generally try to keep things simple and tractable. Obviously, there's plenty of terrible Java code out there, but there would be plenty of terrible Haskell code out there too if Haskell had similar levels of usage. In any case, I was responding to the general statement that Haskell's purity makes reasoning easy by mere virtue of being pure. Well, LC is pure and it can be just as messy as Turing machines. Haskell code -- like Java, C, and Python code -- is simple to reason about when it is written with care (yes, I know that there are differences, but as a general rule).
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.
That's one nice thing provable in Haskell's type/effect system, though, that the ambient effects available are no stronger than X for various descriptions of X. I know you dislike that whole regime, but it at least in this specific case explicitly circumscribes situations where, e.g., Cont is too strong.
> 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.
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-linguisti...
> In those cases, one possible strategy is to take a detour via auxiliary data types...
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/distribut...
> 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
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...
> 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... If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools.
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 totally ridiculous to need an automated theorem prover to verify a sorting algorithm.
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?
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.
Sorry, but I don't really get why you are comparing Haskell and the model checkers you listed. Haskell is a programming language and is not meant to be a formal verification tool.
Because Haskell's design has always placed verification as a top priority. Indeed, Haskell tries (IMO, unsuccessfully so far) to combine programming and verification in a single language. In fact, for some time, Haskell's colloquial tag line was "if it compiles it works" -- what is that if not verification?
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.
> "if it compiles it works"
I think this wasn't meant literally. I think it rather means that a program that type-checks is at least more likely to work than a dynamically typed one. I think this is far from verification.
> 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).
You know what? I'd like to ask you a personal question.
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?
Ah right. It's you who gets to define the word "verification" and Haskell is aiming to do it, yet failing to do it, whether its creators and proponents like it or not.
> Because Haskell's design has always placed verification as a top priority. Indeed, Haskell tries (IMO, unsuccessfully so far) to combine programming and verification in a single language.
Could you point to me to Esterel's formal semantics? Last time we discussed, you also mentioned Esterel, so I was a little bit curious, but, after 30 minutes of frantic DuckDuckGoing, ultimately could find nothing.
#1 I might be completely wrong, but I think this might be doable in Haskell with a monad that tracks total time + maybe STM would help for the rest of the requirements (for a subset of the problems)
#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
> #1 I might be completely wrong, but I think this might be doable in Haskell with a monad that tracks total time + maybe STM would help for the rest of the requirements (for a subset of the problems)
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.
You're right. I didn't mean full formal verification, I just meant controlling the amount of code you do need to verify. There will be axioms of course i.e.
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.
That's assuming that exceptions show up in type signatures. (Which they do in Java, granted.) And it's still incredibly noisy compared to pattern matching on Options/Eithers or, even better, chaining them Kleisli Option/Either arrows.
Its not the same at all - for one, in Java null can be assigned to any type. There is a difference between the inability to prove certain things and having giant holes in the type systems that nullify most guarantees.
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.
> Additionally, I believe that the effort required to write Haskell code is vastly over-estimated.
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.
> 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.
The distinction isn't too hard to make: a type system's "goodness" is:
* 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)
I'd like to expand on #3 via examples:
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.
I don't think that optional typing is in general an attempt to solve sucky static type systems -- instead, many researchers and organizations view it as a way of converting programmers who have only seen Java into developers that willingly use the type checker. It's a great motivator when you experience a bug in production that the runtime helpfully reminds you could've been caught if only you'd turned on types in that code :).
> don't bolt less-than-half-assed static typing on to the side.
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 gave up on core.typed because I've found adding type annotations to most of the forms is significantly harder compared to a statically typed language. (In hindsight this is obvious, I know.)
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.
Over and over I see reports of iteration speed being critical to real-world projects, and that's certainly my experience.
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 problems I've seen with tools that try to load everything once and monitor for incremental changes -- is it's hard to get RIGHT. These tools tend to be buggy, or worse tell you it's not them that's buggy, it's you that's "doing it wrong" somehow, trying to work the way you want.
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.
The problem is that our editors are at the core still "text" editors. That forces the tools (IDEs) to continuously synchronize the text with the parsed AST.
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 :(
I think we wouldn't even have to give up whitespace, comments, and other things that get left out of ASTs. I think the problem there is that ASTs are normally thought of a one-way, compiler-friendly representation. But if we start thinking of them as a round-trip representation that is also friendly to programmers, it doesn't seem impossible to include comments and formatting as hints in the AST that compilers and interpreters ignore. Sort of the same way that many HTML and XML parsers keep track of comments and whitespace even though that generally gets ignored by code that uses the parse trees.
The counterpoint to this is that if you're not using text editors then you lose the universal property that most source code is plain text which can be edited with your preferred text editor. Plain text seems to be the most tool-agnostic representation, which for many people is a big plus. Notice that in this day and age there are still people complaining about "bloated" IDEs...
I think there's a useful distinction between serialization format and working format (that is, what it looks like in RAM). For a plain text editor, they're the same. But that's pretty unusual.
There's reason we couldn't have an editor that works with the AST while saving everything out in plain text for interchange purposes.
True. But the property you mention -- that for plain text editors the serialization and working formats are the same -- is actually a pretty useful and convenient property! I think this is why it's extremely unlikely there will ever be widespread adoption of a different format for source code. Niche tools will remain niche forever, in my opinion.
Sure, simple tools are great when simple is what you need. But here they took a simple approach to a problem that's essentially complex, which means they lost a user.
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.
I'm not very familiar with Go, but from what I understand Go is the antithesis of this feature in many ways. AFAIK the tools are all stand-alone command line applications which you have to run every time you want to check whether you're on the right track. Go tools which generate code are an even worse example. If your language good abstraction capabilities your development environment could understand your intentions much better than with generated code.
> AFAIK the tools are all stand-alone command line applications which you have to run every time you want to check whether you're on the right track.
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.
We've been using Flow at Streak. Compared to my last experience with TypeScript, it's been really great for how easy it is to add into an existing codebase. Nothing about our build process had to change because we were already using Babel (which by default strips out Flow types and supports JSX) with Browserify. Flow understands node-isms and follows how commonjs and es6 modules include each other, and only enforces its type checking on files that have opted in with the magic /* @flow */ comment, so we didn't have to stop the world and make everything play nice with it in one go. We're gradually opting in more of our codebase over time. Its type system maps to javascript really well, supporting things like optional types, disjoint unions, intersection types, and polymorphic functions and classes.
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.
An IDE's a good start. But IDEs tend towards monolithic, which can mean relatively low adoption. I'd much rather see independent tools that can be plugged into IDEs. E.g., in this case, I'd rather that the type checker ran as a daemon. In its base mode, it would just produce text output. But it would also have some IDE-friendly protocol so that it could be easily bundled.
Yeah some tools are kind of like what you describe... for example, FindBugs is a great lint-type tool for Java, that you can run standalone from command line (ie as a part of a build, or CI), but also has plugins for all major Java IDEs. I have it set to run every time I save a file (on that file only) and here is a kick, it does not run the command-line version, it just runs within the IDE so it is fast enough to be imperceptible.
I guess they do? Eclipse itself is many millions of lines of code, and far as I can tell, it seems that the prescribed way to develop for it, is to use Eclipse itself.
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 feel like I can somewhat relate, I've been adding flowtype [0] annotations to my JS code, which is transpiled with babel. However, since I'm using unsupported ES2015 features and experimental ES2016+ features, it fails to run over my code (which is completely understandable).
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.
Not the OP, but I use flow because (1) it's easy to integrate into an existing project without having to define and rewrite everything with types and (2) I've found myself using other Facebook tools anyway (mostly in the React ecosystem) and Flow tends to be better supported in that world. But I hear the IDE support for TypeScript is first-class, something I haven't found to be the case with Flow, which interests me.
Mainly because I was already using babel (which was 6to5 at the time). Typescript didn't support JSX at that time either. I don't know if TypeScript has full ES6 support yet? (And async/await!)
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.
One particularly relevant feature of Flow is that it does its type checking in a server. It watches the file system and incrementally rechecks automatically when files change. With this setup, "running" the type checker is actually just querying the server, which returns very quickly.
"You should support this" is not the same as "we're using this". Typed Clojure was a neat research project (disclaimer: I supported it) but it seemed not to work for their actual needs.
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.
I wrote that post, and it was very much about why you should support Typed Clojure, not why you should use it. You should support it for the potential, you should decide whether to use it on practical concerns.
Typed Racket (due to different integration into the compiler) is much more incremental -- the speed issues in the blog post would be much reduced. The typechecker still isn't as fast as we would like, though, although we have plans to improve it.
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.
This bit raises the question, is #1 being caused by #2 and #3?
--------------------------------------------
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?
I don't have nearly the breadth of experience in Clojure as the circleci guys, but I found that Prismatic's Schema [0] works well for me vs. core.typed. I can selectively annotate functions with their return types, and test runs will validate that they are returning as expected. It's runtime evaluated, so you lose a lot of static analysis benefits that type checking gives you, but it still provides some good code coverage, forces you to think about types a bit, and (the biggest benefit for me) it serves as documentation for functions that might return somewhat complex types. I can return to code months later and have a good idea of what's going on.
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.
I introduced core.typed to Circle, and I was responsible for most of the early type annotations in the Circle codebase. Because of me, Circle was also the first large contributor to core.typed's kickstarter campaign.
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.
> 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.
It seems like something like the dependency tracking and selective reloading in Stuart Sierra's tools.namespace could be used to mitigate their first problem.
147 comments
[ 3.9 ms ] story [ 183 ms ] threadThis, 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:
(Yes, that's compile time instead of run time)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:
Interestingly, the Perl 6 core team could allow for powerful type inference with this, but one of the core issues has always been that many languages using type inference have rather opaque error messages because they essentially dump a "proof" of type failure and many struggle to understand them. Thus, the the Perl 6 devs are taking more careful approach, though they know they can do more. For example, this falls back to a runtime failure instead of a compile time failure: In other words, because it's not sure of the type of $name at compile time, it falls back to run time (though in the simplistic example above, that's clearly not the case). Annotate the $name variable and you get a compile time failure again: With this, third-party libraries which don't declare types work just fine, but you get type-safe run time failures. If they do declare types, you often get compile time failures (though it will still fall back to run time, and won't check at run time if it knows at compile time that it works).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
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.
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.
There'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?
http://www.shenlanguage.org
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.)
[1]: http://linux.die.net/man/1/watch
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.
[1]: http://www.cl.cam.ac.uk/~mom22/pldi13.pdf
«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 ...
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-linguisti...
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/distribut...
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
[1]: http://elm-lang.org/docs/records
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.
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.
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.
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)
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.
[0] https://github.com/gcanti/tcomb
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.
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.
--------------------------------------------
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?
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.
[0] https://github.com/Prismatic/schema
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.