[rer]

> the programmer ends up with less to specify

I don't see how this can be true. Wouldn't there be less to specify if the programmer didn't have to specify types at all?

[dllthomas]

Sometimes behavior follows from the types. Combined with inference you sometimes wind up writing substantially less code (because it's basically being generated for you by a prolog program).