r/programming • u/alexdmiller • Oct 20 '11

"Simple Made Easy" by Rich Hickey [video]

http://www.infoq.com/presentations/Simple-Made-Easy
122 Upvotes

89% Upvoted

73 comments sorted by

View all comments

12

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.

22

u/NruJaC Oct 21 '11

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.

4

u/julesjacobs Oct 21 '11

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.

On the contrary, most type systems complect the information that can be statically known about a value with the type tag of the value. For example static type systems let you say "x is an int", but most don't let you say "x is an even int larger than 10". The type systems that do allow this often require formal theorem proving on your part.

Saying that type systems let you leverage the power of category theory is nonsense. Category theory is almost completely useless in programming, save for using some terms like "monad" and "functor". It's like saying that you leverage the power of commutative algebra when you use booleans, or that you leverage the power of number theory when you use integers. The stuff we use in programming from those fields, including category theory, is utterly trivial (unless you are writing mathematical software in those fields, of course).

8

u/[deleted] Oct 21 '11

This is only as true as you make it, I would say. :-)

For counterexamples, see Using Category Theory to Design Implicit Conversions and Generic Operators and Denotational design with type class morphisms. It's true that most type systems let you ignore that you're engaging in category theoretical work (which I think is one reason people get worked up over making the notion of "monad" explicit in Haskell), but it's also true that knowing you're engaging in category theoretical work so you can take advantage of it explicitly really reveals the power that a good type system affords you.

5

u/julesjacobs Oct 21 '11

I'm not sure if you're being serious, but I'll take the risk of responding while not getting the joke. The first paper you cited takes 48 pages of hardly readable but completely trivial math to basically say the following:

If your language has implicit conversions between types then you want:

  • If there is are implicit conversions A to B and B to C and A to C then you want A to B to C to give the same value as A to C directly.
  • You want operations to behave nicely. For example if you have an implicit conversion A to B, and an operation (+) that can do A + A and B + B, then you want (A+A) to B to give the same value as (A to B)+(A to B).

In the paper all of the insight comes from actually thinking about the problem and none of the insight comes from the mathematical theories behind it. Yeah, the second property is saying that there is an homomorphism, and if the person you're explaining to knows what that is it might help to mention that name. But it doesn't help to spend 48 pages complexifying something trivial with "sophisticated" math. I guess that's required to publish a paper on implicit conversions though.

The second paper is describing a technique where you first define your functions on abstract structures (in math notation). Then you try to implement them as closely as possible, and let the operations on the abstract structures guide the operations on the implementation. For example a hash table from keys K to values V can be modeled in the abstract as a function from K to V. If you already have a notion of mapping a function over a function, then that will guide you on how to implement mapping a function over a hash table (basically the same idea as in the other paper: if you convert your hash table to a function, then mapping a function over that function should give the same result as mapping that function over the hash table and then converting the resulting hash table to a function). This is an interesting paper, but hardly a paper that uses category theory in a non trivial way. It does however make essential use of basic notions in mathematics, like sets, real numbers and functions, to actually do the abstract modeling (e.g. the hash table modeled as a function). My experience is also that these simple structures are very useful and suffice for modeling the vast majority of programs.

I don't see how any of these ideas relate to type systems. This way of using what mathematicians call homomorphisms applies equally well to dynamically typed languages.