Dynamic vs static typing

(This is a response to a post "Dynamic Languages are Static Languages". I tried to post a comment, but Wordpress told me it couldn't send it, probably because the post in question is too old. So I'm putting it here.)

Your thesis sounds wrong to me. My experience is that strong typing simply disallows some perfectly normal easy programs to be written. And that shouldn't be true if dynamically typed languages are just a special case of statically typed ones.

A few months ago, in order to learn Haskell (in an academic setting), I tried to write a Haskell function to test if a Boolean function was valid (always true). The literature I was using (The Haskell Road to Logic, Math and Programming, by Doets and van Eijck) did that in stages, valid1 for unary functions, valid2 for binary ones... I, as a diligent professional programmer, saw a common bit of code in those, and naively thought I could use recursion (and currying) to make a function valid, so that valid 1 was valid1, valid 2 was valid2, and so on. That way, my code would be much more general, _and_ easier to write.

Imagine my shock when I got an occurs check error. Of course, the problem is that valid1 had type (Bool->Bool)->Bool, but valid2 had type (Bool->Bool->Bool)->Bool, so there simply was no way for valid to have a type, and the GHC told me so. In fact, to be completely honest, valid _has_ a type: a dependent product type, n:Integer->(Bool->...->Bool)->Bool, where there are n arrows inside parentheses. But Haskell can't represent such types, at least as far as I learned (please correct me if I'm wrong).

So, you'll probably tell me I was simply using too weak a type system. But Haskell is the poster child for functional programming. If I can't use that, then what? Miranda is even weaker. Standard ML is not pure, it seems. Coq is not even Turing complete. _Where_ do you find that ideal typing engine you're constantly talking about? Or is it just a platonic ideal, with no implementations in the real world?

Or you're going to tell me that valid function is simply not a function. It is a nonsensical notion, since in a well-typed language you could only have valid1, valid2 and so on. To that I'll tell you it's nonsense. I have perfectly well represented valid in Coq, and Coq surely knows its type theory (however, as I said, it has other problems).

Or you're going to tell me that it's no better in the world of dynamically typed languages. That's simply not true. I can write valid in Python in a few minutes. (Thanks to Python's introspection capabilities, I can even drop the first parameter, and ask my argument function how many bools it would like to receive. But I know static typing fans would probably scream at such an idea.:)

Or you're going to tell me to shut up and simply use lists. Integer->([Bool]->Bool)->Bool is a good approximation, and I did use that variation in the end. But it feels like a horrible kludge. I don't want lists, at least I surely don't want Haskell's interpretation of them as codata. It makes no sense to ask if a Boolean function receiving an infinite list of arguments is valid. And even if it did, I have no way to put something in the "Integer" place. Yes, I can get rid of it, and get it from the length of the list. But the situation is even worse than that: I seem to have no way of restricting the argument to only receive lists with _same_ length. Boolean function that knows how to handle both 2-element and 3-element lists is simply not a valid argument for the function valid I was intended to write.

I don't think I can change your opinion, you obviously know a lot about those things. But maybe you can change mine, by communicating your idea better. What am I missing?