Simon Peyton Jones

Something that's very monad-like has appeared lots elsewhere.

It's been a very unifying concept.

It lets you reject silly programs up front.

So if I have a function that adds one to things and I apply it to a character or to an IO computation, I'd like to, that's going to fail at runtime.

Because I can't add one to a character.

Or maybe you overload plus, maybe reverse a list or something.

If I've got a list reverse function and I give it something that just isn't a list, then it's a bit silly to allow that and only fail at runtime.

So fundamentally, type systems are about rejecting at compile time, programs that you do not want to run because they will fail at runtime.

Now, we've had static type systems for a long time, like going back to Pascal and earlier, but simple type systems are annoying because they get in the way.

Imagine a function that reverses a list.

In Pascal, you could write a function that reverses a list of integers, but if you wanted to reverse a list of characters, sorry, you can't.

That function that reverses a list of integers, it has type list of int to list of int, so you can't apply it to a list of characters.

Game over.

You have to write another copy of the code with a different type.

That's a bit annoying.

So what are we going to do?

We need polymorphism.

We need a more powerful type system.

We want to give reverse to type for all A, list of A to list of A. So that up front says I work for any type A. You give me a list of integers?

Fine.