Not Lisp again . . .

I’m always searching for a good way to explain what you can do with Lisp that you can’t do with most other languages. Joe Marshall has a compelling story, from a skeptic’s point of view, for what makes functional programming different. There are multiple parts that trace his way through a course at MIT and toward a love of lisp.

From the post:

I was floored. Here we take the simple, straightforward definition of the derivative of a function. Type it in with essentially no modification (we’re a little cavalier about dropping the limit and just defining dx to be a ‘reasonably small number’) and suddenly the computer knew how to do calculus! This was serious magic. I had never seen anything like it before.

Good stuff. It made me revisit Structure and Interpretation of Computer Programs, an all-time classic.

Type systems are right because they impose a rigid view of a domain (otherwise known as a model) that can then be reasoned about in a structured and reliable way. Well defined types define an ordered space in which the programmer can solve a problem. Outside of that space lies chaos.

C’s type system has been criticized for being flawed. It certainly is not as logical as Haskell’s. I am not going to argue with that. But C’s type system has (at least) one redeeming quality: an escape hatch.

When the Creators brought C into existence, they endowed it with a few datatypes and a way to make some new ones. But by letting any pointer be cast to (void *), they blessed C with the unifying principle that makes it so useful*. That principle is eloquently stated in three words:

Bits is bits.

And its universality brings beauty to the language.

Brittle class hierarchies serve a purpose. They let you model your domain. In a sense, you are creating a language about the problem. It is brittle because you want to know when it breaks so you can fix the problem. But sometimes, if you are adding and adding classes, legitimate stuff stops fitting in so neatly. You kind of have to force it, because the model you chose did not accomodate everything*.

There are many work-arounds. They will work in the short run. Eventually, you will have to rewrite. Reorganize your class tree to be more elegant. Because problems are best solved through grace, simplicity, and order. Every time you fudge in a new type, it will come back to haunt you. So take the time to find an elegant solution.

In short, you should keep your program brief and to the point. And rewrite it often.

Haskell’s type system disallows two broad classes of typing problems. It does not allow what it can prove to be incorrect (for example assigning a String value to a Number variable). That makes sense. It also does not allow anything that it cannot prove correct. That also makes sense, though it is somewhat annoying when you can see that it could be correct. This problem comes down to the issue of provability.

Haskell has a restricted inference engine to deduce the type of values. It is restricted to reasoning somewhere below first order logic. There are definitely things you cannot prove without at least first order logic*. So Haskell’s type engine cannot prove every type inference I can know is correct. So it just blatantly limits what you can say.

If it had a more powerful inference engine, one that was at least as powerful as first order logic, it would not even know what it could not prove. Such is the problem with powerful logics*. That means that there are typed expressions you could state that Haskell would not be able to prove correct (or incorrect). And what is worse, Haskell would not even know that it could not prove them. So Haskell must be restricted to a lower-order logic.

At least, that’s what the type theorists say. Haskell will do lots of type inference work for you, as long as you restrict your type usage to a very limited range. And I choose not to live with that restriction.