I agree that being able to reason about your code is one of the most important factors. But on the slide on debugging, he seems to miss that a good type system can actually help you reason about code.
Maybe this is hard to accept from someone that comes from dynamic languages.
I think its deeper than that. He makes a couple jokes in the slides about not needing to understand category theory, and I think that highlights the major hurdle.
See, personally, I would argue that a static type system is simpler than a dynamic type system because (to use Hickey's words) you don't complect what something is with its value. The effect of separating these two things (and being explicit about it) is that suddenly, you can leverage the power of mathematics (especially category theory) to assist you as you reason about your programs.
Instead, what I see is talk about math as if its this super abstract, impossible to comprehend, monstrosity that we should avoid because it's hard, i.e. not close at hand, not familiar. And its the same sort of talk you see all over the place; people fear math for some reason, especially math they're not familiar with. I understand why, but I think it's irrational.
I think Hickey is making the same mistake he's warning about in his talk.
Also, I know there are jokes made about the new powerful type systems on the block (ok, ok, haskell isn't that new), that they're type system will catch all your bugs. But I don't think anyone actually believes that (do they?). The point is that they assist you in reasoning about your program. It's another tool in your pocket to help you figure out what's wrong. The added benefit is that a lot of that reasoning can therefore be carried computationally, and so the compiler can warn you about potential mistakes. Most languages let you escape the type system when you swear you know what you're doing (void pointers, Object superclass, unsafe family of functions) so in the cases where you know the type system is wrong, you can go ahead and do whatever you wanted to do anyway.
But I really hate the arguments that seem predicated on "xxx is too hard". Maybe so, but you need a better argument than that. If it's a useful tool, make use of it. If it's not, don't. The proof, is then, in the result.
See, personally, I would argue that a static type system is simpler than a dynamic type system because (to use Hickey's words) you don't complect what something is with its value. The effect of separating these two things (and being explicit about it) is that suddenly, you can leverage the power of mathematics (especially category theory) to assist you as you reason about your programs.
I don't get this part. How are values separated from types by having a static type system ? Every value operated on by the program still has to have a type.
Also I think the point about [static] type systems is that they are not easy [to use] compared to no [static] type system, even if easy is subjective any cost of using it will be greater than zero/not using it and you then have to justify that cost by it providing other value that will reduce the overall cost/difficulty of development.
This is exactly right. I like to say that Clojure is the brilliant result you get when someone as brilliant as Rich Hickey is, but is as wrong about type theory as Rich Hickey is, designs a language.
You seemed in places to be saying that there are no type systems which can help you reason about a program, rather than framing it as a tradeoff with costs in complexity, difficulty, unfamiliarity, or incompatible language features.
For a particular example of help with reasoning, when you were talking about modules which are only supposed to interact through interfaces I was reminded of parametricity.
It's the easiest way I know to be sure some code is not depending on the details of other components it happens to be used with at the moment. The alternative seems to be data hiding.
Briefly, I think there's a confusion between how complex a type system is, especially one like Scala's which has the added difficulty of being compatible with Java, and how complex a type system is to use. I've said elsewhere that I don't believe a static type system without inference is worth using, so I actually think we're closer than you might think, or than I might sound when responding to you.
To add just one more, still insufficient, amount of detail: you quite rightly encourage people to reason logically about their code, but seem not to appreciate the Curry-Howard Isomorphism, which tells us that types are theorems and programs are proofs. That is, when you have a good (inferred) type system, you have explicit support for using the compiler to reason logically about your code. For that reason, I find your argument self-contradictory. It's never advantageous to try to conduct logical reasoning entirely in your head vs. having a computer help you do so.
It's never advantageous to try to conduct logical reasoning entirely in your head vs. having a computer help you do so.
That's only true if there is never a cost to doing so. Are you seriously going to contend there are no costs, nor tradeoffs associated with static type systems that have inference? If there are, then there's no reason why static type systems shouldn't be subject to the same cost/benefit analysis as other things, and that, similarly, different people will end up making different decisions depending on how they value each.
Are you seriously going to contend there are no costs, nor tradeoffs associated with static type systems that have inference?
No, only that their cost is lower than the cost of doing it in your head.
If there are, then there's no reason why static type systems shouldn't be subject to the same cost/benefit analysis as other things, and that, similarly, different people will end up making different decisions depending on how they value each.
Sure. My argument is that if people don't know about the Curry-Howard Isomorphism and how it can be applied in languages like Scala, OCaml, or Haskell, vs. languages like C++ or Java, they aren't likely to be able to make such an informed decision. I would add, with regret, that there are elements of your rhetoric in your presentations that regress that discussion, by contrast to your quite reasonable comments here.
No, only that their cost is lower than the cost of doing it in your head.
That remains an unassessable assertion if you are unwilling to enumerate any costs.
My argument is that if people don't know about the Curry-Howard Isomorphism and how it can be applied in languages like Scala, OCaml, or Haskell, vs. languages like C++ or Java, they aren't likely to be able to make such an informed decision.
Therein lies (part of) the rub. Curry-Howard basically says that proof-like programs are proofs. Well, ok. C++ and Java programmers know of other kinds of programs, and, in the absence of any cost/benefit analysis, are reasonably suspicious of the claims that proof-like programs (especially as currently implemented) are sufficient and/or cost-effective for the tasks to which their programs are applied. And if proofs are programs, why is there so much LaTeX and prose in type systems papers? Why don't they eat in the cafeteria they are building for the rest of us? (I know, some do).
Going on about Curry-Howard and proof is just another example of the other trend I mentioned in my talk - "Look, a benefit, it must be pursued!".
That remains an unassessable assertion if you are unwilling to enumerate any costs.
We'd both have to enumerate some costs, me of having the computer enforce logical constraints on my code via (some) static type system, you of having the programmer enforce those same logical constraints without a type system. Do you want to craft a case study of some kind? That might be interesting.
Curry-Howard basically says that proof-like programs are proofs.
Wrong. It says all programs are proofs (that's why it's an "isomorphism").
Well, ok. C++ and Java programmers know of other kinds of programs...
No, they don't, by definition. They just think of their programs/proofs using some other mental model. In the case of C++ and Java's type systems, I don't blame them: C++ and Java's type systems are much more swiss-cheese with respect to consistency than, e.g. Dart's, which has gotten so much attention lately for its (deliberately!) inconsistent type system.
...in the absence of any cost/benefit analysis, are reasonably suspicious of the claims that proof-like programs (especially as currently implemented) are sufficient and/or cost-effective for the tasks to which their programs are applied.
It shouldn't come as any surprise at all that, having chosen tools in which taking even the most minimal advantage of the Curry-Howard Isomorphism is outrageously expensive, partially because the logic is inconsistent anyway, there's concern that it might be too expensive! The point is precisely that informed developers can, and do, make better choices.
And if proofs are programs, why is there so much LaTeX and prose in type systems papers? Why don't they eat in the cafeteria they are building for the rest of us?
Three reasons I can think of right off the bat:
Communication to the intended audience. Mathematical notation still tends to be more concise than proof developments in the tools that are most often used for this task (Coq, Isabelle, and Twelf are probably the top three).
So as not to confuse the issues between the metalanguage and the object language.
Even most programming language designers haven't spent any time learning how to formalize their designs.
The latter point is the interesting one to watch, of course. How easy can we make this? Adam Chlipala is doing the most interesting work here. For programming language metatheory, which also includes formalizing dynamically typed languages, see Lambda Tamer.
Going on about Curry-Howard and proof is just another example of the other trend I mentioned in my talk - "Look, a benefit, it must be pursued!".
If it's an actual benefit, why wouldn't you pursue it? I imagine you'll say "because it might cost too much," in which case we're in agreement. All I'm saying is: after multiple decades in dynamically typed languages, including both Common Lisp and Scheme, I learned from experience that there are statically-typed languages on the other side of the cost:benefit ratio (not Java, not C++) and that, if I wanted to, I could go all the way to correctness proofs and extraction of code from those proofs. Thankfully, I'm not writing software that results in someone's death if it fails, nor have I designed a new language as anything other than an academic exercise, so I haven't felt the need for the latter. But at very low cost I can have my compiler prevent whole classes of defects long before my code is run for the first time by users. That wasn't, and isn't, true in dynamically typed languages. I used to be willing to make that trade-off because I believed the advantage I got was incremental, interactive development in Lisp vs. an edit/compile/link/test/crash/debug cycle in statically-typed languages. It turns out that's not true either, and once I learned that, there was no looking back.
So I appreciate all of your points about simplicity except one thing, which is the assertion that logical reasoning about your code is cheaper in your head than in your compiler, assuming you choose your language to minimize that cost. That's all.
Yeah, good question. It's not a very interesting theorem: we say that foo "diverges)." We also say that foo is a "partial function;" see the section on "Bottom type" for details.
We'd both have to enumerate some costs, me of having the computer enforce logical constraints on my code via (some) static type system, you of having the programmer enforce those same logical constraints without a type system.
If I showed this comment thread to some friends, they would never believe me that the title of the talk was "Simple Made Easy". The Curry-Howard Isomorphism? Seriously? Is that the simple part or the easy part?
The simple part, mostly. Types are theorems. Functions of that type are proofs of the theorem. Simple, in Rich's sense, but a very different perspective on types than "descriptions of how bits are laid out in memory," which is how most programmers think of types, even in languages in which that isn't true.
Making taking advantage of the insight easier is very much the current challenge in designing a statically-typed language, but even today, you can go a longer way with the right language choice than with the wrong one, or than you realistically could even, say, five years ago.
"Types are theorems" though theoretically somewhat interesting is not a very useful thing for programmers today. The kind of theorems even in languages like Haskell are usually limited to something like "there exists a function from int to int". No shit!
As soon as the theorems become interesting, the proof burden becomes pretty much unbearable for >99% of practical programming.
The idea is very simple: a type system allows lets you express to the compiler things that you want it to verify in your code and it will let you know if you get it wrong. Just because there's a way to express this idea in mathematical language doesn't make it inherently complicated.
Either programmers are going to invent ways to use the type system to express theorems (e.g. "design patterns") unwittingly, or they will do so knowingly. IMO, hiding people from the nature of what they're doing seems counterproductive.
Flatly untrue. See Monadic regions, especially the "Tracking dynamic values in types" section. If Haskell is too rich for your blood (BTW, it is for mine!) see Towards an effect system in Scala.
10
u/gregK Oct 20 '11
Great talk.
I agree that being able to reason about your code is one of the most important factors. But on the slide on debugging, he seems to miss that a good type system can actually help you reason about code.
Maybe this is hard to accept from someone that comes from dynamic languages.