There are, likewise, functions and tools that can't be built in statically-typed languages. For example, a general "compose" function (or macro, if you're so inclined)-- one that takes a list of functions and produces their composition-- can't be built in a language like Ocaml. (The best you can do is ('a -> 'a) list -> ('a -> 'a) ; e.g. it has the additional requirement that each function have the same return type as its input.)
As well as the ones you mention - would you include IDEs etc ? or is that more an issue of not doing the "smalltalk way" of editing running code?
For example, let's say you change the output type of a function deep in the trunk-- instead of returning a 'a or throwing an exception, it returns a 'a option, e.g. a discriminated union between None or Some x, where x is a 'a, using the None value to represent failure, in lieu of the exception-- and want to find all the places where things break in the leaf code, so you can adapt them to the changes. What tool do you use: grep? Nope. You attempt to compile the tree, and all the code-breaks are caught and displayed by the compiler.
I know the "typed lambda calculus" is the super set of the lambda calculus, but that's about it for me (or rather the "commonly known" lambda calc. is really a special case of the more general typed lambda calculus) - now if that translates into static typing being more mathematically pure/complete, I don't know (and even if it did - what does that mean in practice??).
I think nice languages with decent type systems kind of make static typed languages look nice - so the aesthetic argument (which is what most people refer to when they bring up the debate) mostly goes away (eg haskell, scala to some extent - although it can get gnarly).
I like using both - however from what little experience I have had I haven't enjoyed dynamic languages with optional type annotations (but it is limited experience).
I am interested in Brendan Eich's suggestion for ECMA script 4 (!) to have typed interfaces for the edges of a system....