Pozorvlak's Conjectures

[pozorvlak]

For the past couple of years (longer, actually), I've been thinking a lot about this business of static and dynamic typing in programming languages. Here's my current position on the matter.

Static and dynamic typing encourage and reward quite remarkably different approaches to the creation of software: everything from the nitty-gritty, (sit and think?)-edit-(compile?)-run-(test?)-(debug?)-(repeat?) cycle to the design (at all levels) of the software to be created, taking in every aspect of the tools and process used to support this design and implementation. Also, the choice of static or dynamic typing is best understood as part of a larger attitude towards development. Unfortunately, the use of a dynamic mindset with a static language not only means that you can't take advantage of the tools available (or even see why they'd be useful), it actively hinders success. The same is true for approaching a dynamic language with a static mindset.

I would therefore like to propose Pozorvlak's Conjectures:

1. If you find that a modern dynamic type system causes more problems than it solves, you're probably doing it wrong.
2. If you find that a modern static type system causes more problems than it solves, you're probably doing it wrong.

For instance, I find Haskell's type system causes me many more problems than it solves. Discussions with more expert Haskell users suggest that I am indeed doing it wrong. This guy, on the other hand, finds that "the dynamic languages stick out like sore thumbs because of the whole class of dynamic run time errors that show up that don't even appear in the statically typed languages". If you find this, I claim that it's because your code is not polymorphic enough¹. You can get away with having code which only accepts data of very restricted types when the compiler does all the checks for you statically. When it doesn't, you're better off writing code that behaves well for a wider class of inputs, and dynamic languages give you much more facility to do this. Once you learn to code like this, your problems largely go away. As a bonus, your code becomes more flexible, and whole classes of techniques become possible that would have been literally unthinkable before. Similar claims, it appears, can be made for static languages: at the higher levels of mastery, one can use a static type system as a theorem-prover to establish some quite nontrivial properties of your program automatically and across the entire codebase. This allows for some excitingly different approaches to program development.

A corollary is that if you ever finding yourself saying that your port of Feature X to Language Y is better than the original Feature X solely because it's (statically|dynamically) typed and the original Feature X was the other one, you should probably save your breath. It will probably also be worth your while to go back and determine what advantages the opposite choice of typing regimen gave to Feature X's users.

¹ A less interesting, but probably valid conjecture is that you're also not testing enough, or at least testing the wrong things. But this can't be the only answer. Dynamic programmers, in general, are not idiots; they are usually also Lazy, in the good sense. They're smart enough to work out that writing the equivalent isa_ok() test every time they would have written a type declaration in Java or whatever is no time-saver at all. Hence, they must need less type information overall for their code to be correct.

Comments

[totherme.livejournal.com]

All sounds pretty sensible to me :)

Further to you corollary, I'd note that making something (statically|dynamically) typed is a huge advantage if everything else in your system is going to be (statically|dynamically) typed. This is automatable going in the static->dynamic direction (just insert a bunch of runtime checks at the interfaces), but not necessarily the other way around (possible if the dynamic code happens to have been written in a pretty typey way to begin with - but if it was, then the author should probably have been using a static system in the first place. This is the subject of ongoing research by Smart People).

So, some obvious questions include "Is one style better for any clearly definable problem domain?" and the related "Why do people favour one style over the other?"

I think the first question is much harder to answer, and the second one potentially more interesting :)

[pozorvlak.livejournal.com]

Corollary: that's a really good point. Yes, library authors should be entitled to put as a bullet point "Library X' is a good citizen of $type_discipline", but that doesn't automatically make Library X' better than the original Library X, which was presumably a good citizen of its own language and type discipline :-)

I agree that it would be possible to automate static->dynamic library conversion, but you're unlikely to end up with a very natural-feeling library like that. I'm thinking about the Ruby DOM libraries there - weren't they later supplanted by more native-feeling interfaces?

I suspect a lot of the answer to your second question is "experience and training", but no doubt a component is "temperament" - and that's the interesting bit.

[pozorvlak.livejournal.com]

Related to the library porting issue, it's interesting to compare Lisp macros with Template Haskell. Lisp macros can be explained in a sentence: "they output a sexpr which is spliced into your code and then executed", whereas TH introduces a complex API for describing the structure of Haskell code. Macros in TH are more complex than their Lisp equivalents, but can be typechecked; they can only be run at compile-time, but provide stronger guarantees. Lispers get simplicity and power, and Haskellers get static checks and guarantees: everybody feels like they've got the better half of the bargain :-)

I don't know about that

[(Anonymous)]

In this case, you're right, but TH does syntactic transformations just like lisp macros, and there's no guarantee that TH's transformations are type-preserving. If there were, then you'd _really_ be in static land. But the reason that lisp macros are simple is because lisp's syntax is simple; the reason TH is complicated is because Haskell's syntax is (comparatively) complicated. If you gave lisp a polymorphic lambda calculus type system, I'm pretty sure macros would carry over almost unscathed. That is, if there weren't a whole culture of lisp idioms that are not well-typed.

I certainly agree, though, that there is no answer to whether static or dynamic typing is better. Or no, I should revise that statement. I agree that currently there is no answer. But I believe in the future static could be better; never dynamic. If someone invents a type system which can support almost all dynamic idioms, still catch errors, and perform inference, then I will leave all my dynamics behind. From my experience with studying type systems, this is highly unlikely :-)

-Luke (http://luqui.org/blog)

Re: I don't know about that

[pozorvlak.livejournal.com]

Well, TH does all its transformation at compile-time, and the output is fed to the type-checker then and there: if your macro produces ill-typed code, you learn about it quickly. Whereas in Lisp, as I understand it, macros can be invoked at runtime, causing type errors while the program's actually running.

I remember reading somewhere that some well-known theorem, possibly Rice's Theorem (http://en.wikipedia.org/wiki/Rice's_Theorem), implies that

• it's impossible to write a static type system that catches all bugs;
• the stronger you make your type system, the more valid code will be rejected.

. Hence the perfect static type system you want is actually impossible. It also seems to be the case that inference imposes a large cost on a type system: if you want your compiler to infer types, you're greatly limited in the features your type system can offer.

Limits of type systems

[(Anonymous)]

I think you have those points backwards!

1. Rejecting all buggy programs, for some class of bugs, at the cost of also rejecting some valid programs is precisely what most (published) type do. "soft type systems" are the ones that let you run any valid program you want, and only catch some bugs. A type system should

• Reject all buggy programs
• Accept all bug-free programs (an untyped program is "accepted" if there is any way of assigning types to get a well-typed program)
• Have decidable type inference (starting from a completely untyped program)

The full theorem says you get two. It's actually possible to get two. Say you start with the untyped lambda calculus, and want to avoid expressions that don't terminate.

• The untyped lambda calculus already trivially accepts all terminating expressions and has decidable type inference (but also accepts all diverging expressions).
• The simply typed lambda calculus rejects all non-terminating expressions and has decidable type inference (but rejects plenty of good programs too).
• System F accepts all terminating expressions and rejects all nonterminating expressions (but inference is undecidable).

2 "Stronger" doesn't always mean the same thing, but lots of the work on already-sound type systems are about accepting more valid programs while still completely excluding some class of bugs. If you are just worried about keeping the wrong primitive types aways from case statements then simple types, Hindley-Milner and MLF are all safe, but the stronger ones accept more programs.

There's a "full-employment" theorem here, saying you can improve a type system on one of the axes above without making it worse on the other two. Trivially, just hardcode some program mishandled by the existing system - maybe there's a more interesting result? (You can quantify decidability by looking at how much type information you have to add for your algorithm to infer the rest).

A perfect type system (scratch the static!) is impossible, but that means any type system can be improved.

-Brandon (brandon_m_moore on Yahoo)