Lambda the Ultimate

I don't remember seeing this before, Frank. It was an interesting read, thanks.

A good interview, better than average. The best question was, essentially, "in your experience, how much time is needed to learn [C/C++/Java] ?". Stroustrup and Gosling both give long-winded answers, but Dennis Ritchie just says 'I don't know the answer to this question either--my stock joke on similar ones is, "Well, I never had to learn C...."'

Multiple return values in Java would have been a great alternative to exceptions, for those guys who hate exceptions. I like how Gosling regrets not having it.

Kent Pitman covers multiple return values used this way, in an old paper.

I don't have a problem with exceptions. Checked exceptions, however, are a chore. They cause me great pain when I need to program in Java.

Sorry for not being clear. I'm talking about those guys who prefer returning error values to exceptions, in languages like C#. (They actually seem to prefer checked exceptions. I say "seem" because I haven't yet seen one of them give a proper engineering defense.)

The C# guys are very proud of this feature. Maybe it solves the problem (pun intended).

But surely every programmer knows this principle?

The PP articles/book are supposed to be about common sense programming practices (i.e. things that every programmer should know). But just because every programmer should know this stuff, doesn't mean that they do.

When it comes to general programming techniques things become a bit more problematic. I once wrote a couple of tips to help new programmers get up to speed on various useful techniques (e.g., how to make code easier to debug and instrument, how to design in-memory data blocks, that sort of thing). I still think its a valuable exercise.

Having said that, let me add that I haven't read the PP book, so this wasn't meant as a recommendation of that specific book.

So why do pundits, webloggers and authors like this get so much credibility and respect in the programmer community and in the industry?

The reasons you give are part of the answer. Here are some others:

...the type-theory crowd has not done a very good job promoting their ideas in terms that resonate with 'pragmatic' programmers.

The problem is that 'pragmatic' programmers usually disregard claims that any type system may offer flexibility on the base that Java's type-system doesn't. IME it's very common to have discussions like this.

A sample:
He's also correct that dynamic typing is more powerful, statically typed programs are a subset of dynamically typed programs. Dynamic typing is also more flexible, you can program while working one the problem, rather than programming to please the compiler. His final statement is also correct, many of the top professionals are starting to prefer dynamic type systems now that computers are fast enough to make them feasable. Static type systems only advantage over dynamic systems are speed, and some assistance from making typo's.

Usually such discussions follow this pattern:

DT: Static typing doesn't allow you to do X

ST: We can do X like this

DT: Also they don't let you do Y

ST: We can do Y in this way

DT: BTW gurus like A, B and C are singing songs about how DT is better than ST.

ST: Actually they're talking about Java there are better ST systems

DT: Moore's law is on our side.

ST: Moore's law works both ways.

DT: ST get's in the way.

ST: Hey, are you even listening to me?

DT: We won you lose. Hurray!

Argh, now I'm feeling really bitter.

So what exactly are the practical advantages of using statically typed languages such as Haskell and ML?

• They allow you to encode important and useful information about your program in the source code.
• They automatically check that you've encoded that information correctly, and cross-check that the encoded information is compatible with the underlying program.
• They prevent you from running long procedures only to discover a problem that would have been caught before runtime with a checked type annotation. Note that test suites are only a partial solution to this issue, and don't work well for all types of applications.
• They make the code more statically tractable, supporting various kinds of analyses and transformations which, with dynamically-typed code, range from more difficult to effectively or actually impossible (depending on the language it's written in).

Programs have types, whether they want them or not. Keeping all the types in the programmer's head - and not supporting their representation in a mechanically tractable form - is hard to defend, except on the grounds that currently, most languages that do otherwise force you to the other end of an entire spectrum of behaviors, with all advantages and disadvantages which that entails. But that's a function of where the low-hanging fruit in language design is - we're messing around in the shallow end on both ends of the static/dynamic spectrum, and mostly avoiding the deep waters in the middle.

Discussing whether we should always statically know the type of every term, vs. disallowing their being specified statically even though they're often statically known or knowable, is an artificial dichotomy that says more about the state of the PL art than anything else.

Instead of ST fans arguing with DT fans, both should be educating themselves (as necessary) and bugging language designers to do a better job of allowing programs to evolve along the type spectrum. Given languages that can do that well, I can't imagine that many people would be arguing that all programs should be written either entirely avoiding type annotations, or requiring that every term in all programs be statically typeable. There may be specialized cases where one or the other extreme is desirable for some reason, but these should be relatively exceptional cases.

BTW, in a scenario with optional ST, ST "wins" because there are good reasons in terms of verifiability etc. to want a fully ST program, but no good reason I can think of to ever want an entirely DT program. Any real program has many terms whose type is obvious and statically inferrable. This is a kind of "proof" that DT is not the be-all and end-all of programming systems.

Discussing whether we should always statically know the type of every term, vs. disallowing their being specified statically even though they're often statically known or knowable, is an artificial dichotomy that says more about the state of the PL art than anything else.

Now you're talking as a Lisp programmer!

Common Lisp supports optional static type declarations, and a good compiler like CMUCL does extensive type inference from the declarations you provide. Any type errors that can be determined statically are reported by the compiler, and any type declaration that could possibly be incorrect at runtime is dynamically checked. Lovely!

Lisp and CMUCL have the right idea. I'd personally pick Scheme and a soft typing system, although unfortunately the latter systems perhaps aren't as mature as CMUCL, but that's because they're more ambitious.

But I don't think this is a single-language issue. I'm sure there'll always be fully ST languages, because relaxing the type system introduces undecidability, and there are times you don't want that; but nearly all the DT languages could benefit from some optional type discipline. (There are a few that are so dynamic it may not be worth trying.)

Being able to optionally provide type annotations for values seems like a good idea. There are parts of code I write in which I can nail down the types definitely, and so it would be useful to have static checking for this stuff (core algorithms mostly). However, there are always bits of my programs that I am less sure about, and it would be useful to leave out type declarations for the initial development work, and then fill them in when I know what I'm doing a bit more; when I've explored the problem more thoroughly.

This was what I was trying to get at in my post about whether type is a fundamental property of values. If you can take an untyped value and annotate it with a type declaration (deriving a new value), then code which uses the new value could be statically checked (I assume). But you could still get at the untyped value if you wanted to, and the compiler could then leave that code unchecked. Something like (pseudo-code):

foo = getValue() // Untyped value returned
bar = [Integer: foo] // New value with type "Integer"
somefunc(bar)   // Can be type-checked
somefunc(foo)   // Cannot be type-checked
somefunc(bar.raw()) // accesses untyped value, disables checking

Would this sort of thing be feasible in practice? Do any languages have this sort of feature?

;; add1 :: number -> number
(declaim (ftype (function (number) number) add1))
(defun add1 (x)
  (+ x 1))

(defun test (x y z)
  (declare (type integer x)
           (type string y)
           (type (or integer string) z))
  (list (add1 x)
        (add1 y)
        (add1 z)))

If you compile this with CMUCL it will warn you that y is a string and should be a number. It won't warn you about x (known to be right) or z (not known to be wrong).

For fun, the warnings can even be annotated directly onto the expression in Emacs.

Just to show that some inferencing is going on, here's a
slight variation in which z will also be recognised as a string.

More information in CMUCL's excellent manual. (Don't be confused by the fact that CMUCL's compiler is called Python.)

For me such languages allow to discard whole classes of errors that used to bug me on large Java programs (e.g. NullPointerException, ClassCastException). While rigorous unit-testing may help in finding such errors they have two problems:

1. They can't prove that the errors won't occur.
2. Other "team members" can ignore unit-tests (either writing or running) completely.

I'm a big fan of TDD and use it whenever I can but it doesn't help if I have to use other people's code.

In the end of the day if I'm working with Haskell I can sleep without worrying if the server will go down because some race condition uncovered a NullPointerException bug in the code.

For my part, I sleep safe at night knowing that my servers are written in Erlang, and that for any error that can occur there is a simple and reliable recovery procedure that will log the fault and recover. I can then fix the faulty code without restarting the server.

For server applications I think the Erlang philosophy stands up extremely well:

In programming large systems, many small programming errors will be made - we view this as inevitable. Formal systems and exhaustive test procedures are currently not capable of ensuring fault free software for systems of the size and complexity of modern telecomms applications. Given that errors will be made, we are interested in the problem of detecting and handling those errors in such a manner that the system as a whole exhibits satisfactory behaviour in the presence of errors.

Programming in Haskell doesn't prove the absence of these errors either though, as we see from Fergus's post to the haskell list. I think that static-typing fans sometimes give the impression that their type systems prove much more than they really do.

This sounds like a straw man argument to me. What any static type system can prove is usually very well defined, and they do indeed prove the things they claim to prove. It's not as though there's some fuzzy area in which the type system is supposed to be able to prove something but can't really.

In fact, it's precisely the well-definedness of what static type systems prove that make them attractive. "Proof" is used in the mathematical sense, and it provides guarantees of a sort that can't otherwise be made. One way to describe the practical benefit of static type systems is that they make certain kinds of proofs about programs possible and even easy, which is quite impressive if you think about it.

I think the main argument against these sorts of points is to claim that these proofs come at too high a price. That's subjective, and application-dependent.

The problem is that these ST vs. DT debates are rarely precise, and almost never talk specifics. So it's easy for ST fans to sound as if they claim more than the type system they champion can actually do. Some are tempted, and in fact claim exactly this sort of thing.

Same goes for discussion about the benefits of TDD, by the way...

The problem is that these ST vs. DT debates are rarely precise, and almost never talk specifics. So it's easy for ST fans to sound as if they claim more than the type system they champion can actually do. Some are tempted, and in fact claim exactly this sort of thing.

In that case, the DT fans ought to have an easy time refuting what the ST fan is saying.

In the meantime, I've just added a "Halts" type annotation to functions in my toy language, which I'm finding quite useful for statically checking that any given function will indeed terminate. I can't understand why more languages don't have this sort of thing.

Amusingly, that's exactly what they think they are doing. That's why these arguments are so helpful in moving the state of the art forward...

I believe you guys are onto something and I don't want to refute anything. I'm fishing for some discussion of why the particular properties being proved are so important. After all, Haskell programs have bugs too, so what makes the class of errors eliminated by the type checker so important in practice?

I don't think that Joe Programmer is enthusiastic about proving properties of programs for its own sake. We want to know how this will improve our programs.

The problem is we leave CS, into the world of engineering. And I don't think the static/dynamic debaters are truly suited to engineering debates, because their points are invariably general and full of anecdotal evidence.

Engineeringwise, I would definitely like a phase where I can lock down on some code and prove properties about it. Crystalizing it. In the same way code hardens when you optimize or get serious about handling situations like disk-full.

I like CS for proving facts about emergent properties. The darkside is when I must program in a style which only admits easily-provable emergence.

And I don't even know what static means. I find Common Lisp rather static actually, because I can't just go around evaluating a form in an arbitrary environment. There are Schemes which do this; CL doesn't. And after compiletime, CL is effectively static since code-is-data goes away. This is a tradeoff, and while it may be more dynamic than 99% of languages, it's important to mind as a lisp programmer.

I find Common Lisp rather static actually, because I can't just go around evaluating a form in an arbitrary environment.

Sure you can. Just lookup how the debugger does it.

In the sense that an implementation provides such a way, then definitely. I was being imprecise, talking about only the spec.

Incidentally I edited out when I called the debaters "childish." It's not my place, and I didn't mean to be such a critic. (And is being childish bad?) I just wish people realized when they're crossing over into engineering discussions, which is a messy can of worms.

I'm a messy engineering kind of guy and that can of worms is exactly what I'm interested in, i.e. writing software as a whole. As a clarifying example, I think that Emacs is more important than higher-order functions.

If one doesn't relate these languages features directly to software development then it won't be a surprise if software developers don't pay much attention.

I believe we may be missing the point here by treating static typing and TDD simply as 'bug avoiding' techniques. They're much more than that.

I concordance with what a previous poster said, type systems help me to understand the problem better. It's a pitty, though, that current mainstream type systems are so primitive.

Tests can help to define interfaces and contracts. They tend to expose corner cases early. They make me think "how am I going to use this code?", but they don't help much in defining the inner structure.

No single technique known in our days can avoid 100% of bugs, nor they claim to. It's not the point of a type system to eliminate all bugs.

These issues, of course, tend to make the debate even more complex, since it often becomes a debate about programming methodologies - another thorny issue.

Perhaps the thorny part is framing this as a debate in the first place. If the great thing about ML'ish type systems is the overall programming discipline that goes with them, and the only way to understand that is to do serious ML programming, then I can readily accept that. This is certainly the case with the "dynamic languages."

If that's the case then perhaps we could better employ our time by sharing ancedotes :-). I'm quite curious to see some interesting or surprising properties encoded into types, who's got some?

Programming in Haskell doesn't prove the absence of these errors either though, as we see from Fergus's post to the haskell list. I think that static-typing fans sometimes give the impression that their type systems prove much more than they really do.

Of course it does!! It's the whole point of the type system. If you don't understand how the Haskell type-system can prove that something like NullPointerException or ClassCastException won't happen then you don't understand how it works. I can't write:

x :: Int
x = Nothing

in Haskell and I can trust the type-system to rule out any kind of code like this as incorrect. End of story.

Sure enough, when a thread get's this long it must have transformed into a static/dynamtic typing discussion...

I'm enthusiastic about Haskell, but I don't think you've addressed Luke's point. The sort of errors being discussed in the referenced post are function domain errors: calling head on an empty list, division by zero etc.

Sure it may be _possible_ to capture non-empty lists and non-zero integers in your types (actually, I doubt the latter), but it's neither easy nor convenient in haskell as it stands. Assuming you don't, you always have the potential for lurking bugs of this type, despite the fancy type system.

For server applications I think the Erlang philosophy stands up extremely well

The difference between "philosophy" and type-system is that a type-system is enforced by the compiler while a "philosophy" isn't (and can't). I like the idea that the type-system can help me formalize my ideas and give me some properties for free.

Static type systems are still interesting if they can reduce the number of errors. But they don't seem to me like the key to making such software seriously robust, if you accept the premise above. I also find that type errors are the easier to recover from, diagnose, and fix -- I'm much more concerned about logic errors.

A type-system only helps if you encode the semantics of your problem in the types you define. In simplistic type-systems you can encode almost nothing in the types, therefore the type-system doesn't help much and you have the feeling that "it just gets in the way". Many logic errors can be transformed into type errors, so there's no clear line between them. Also if a program has a type error, no matter how many times you crash and restart it still will be logically incoherent.


A simple example. If I want to work with a simple server that should respond to commands I can write it in a way where I can be sure that no unknown commands are going to get through the first layer of the application:

data Command = Deposit Int | Withdraw Int | Close | GetBalance deriving (Show, Read, Eq)
data Result = Error message | Success | Balance [String] deriving (Show, Read, Eq)
serve socket = do s <- readLine socket
                  mc <- tryRead  s
                  writeLine socket $ case ms of
                      Nothing -> Error "Unknown command [" ++ show s ++ "]."
                      Just c -> handle c
tryRead :: (Read a) => String -> Maybe a
handle :: Command -> Result

I can be sure that handle will never get something that isn't a valid command, not null, not a plain string, not a bitmap file, nothing. That makes the software more robust, because if someday a new kind of command is introduced I can be sure that there's no need to check the "serve" function to see if it handles all the possible cases. No "philosophy" can ensure the same thing.

I have found that in most cases if I write down or make up my mind on the type of a function I am conceiving, it is easier to implement --- in a few extreme cases the implementations are almost dictated. Thus I have adopted the habit of writing in Haskell

unit :: a -> [a]
unit x = [x]

and in Scheme

; unit :: a -> [a]
(define (unit x) (list x))

i.e., if the language is not statically typed, I manually type it anyway.

Generally I am for any discipline of annotating as many aspects of a function's specification as possible; and if the annotations are checked against implementation as early as possible, all the better --- it's only ethical.

This is also the standard practice in Erlang. Non-trivial functions are preceded by a comment giving the type signature, and the manuals include type signatures. The notation is informal but quite uniform. Of course it's crucial to understand what your types are whether or not you're running a static type checker.

In my experience there's a certain type-complexity threshold beyond which I get into trouble without static type checking, but in the programs that I write the best solution is usually to simplify the types.
If I were writing programs that fundamentally deal with complex data types, like compilers, then I might very well switch over to ML or Haskell. But I'd say it's less than 10% of my code that uses non-trivial types in practice, so I'm not so motivated.

This is also the standard practice in Erlang. Non-trivial functions are preceded by a comment giving the type signature, and the manuals include type signatures. The notation is informal but quite uniform.

So, are there any typecheckers for Erlang which analyze these comments and statically check the code for compliance, where possible? If not, do you feel that this situation is satisfactory?

For a long time, Philip Wadler has had the statement, "With Simon Marlow, I developed a type tool for Erlang," on his web page. The papers are here; I haven't read them.

I am a fan of both myself, so you shouldn't really see this as a challenge against TDD or static typing. It was just meant as a warning against fluffy debates...