Lambda the Ultimate

Hi. I'm new here.

I've dug up some old topics on the issue of the dynamic/static-typing cold-war/debate, and considering this to be a predominantly pro-static, all-determinism and pro-PF message-board, I would lay down this question as a test of either my misunderstanding, or as a fair argument for a particular point which I think hasn't been mentioned.

One claim that's been in many topics (especially on this forum) and recent papers on modern type theory (even though I have no idea about its origins) is the possibility to construct a 'Universal' type to capture the notion of run-time typing:

data Univ = Inte Int | Str String | ...

This has been used to justify the claim that, since such a hack can be used to bypass the type-checker, statically typed languages can directly express all programs in dynamically typed ones, but such a statement isn't true in the reverse.

One argument that has been thrown against this is that, currently, this isn't very convenient (especially in SML, Haskell and any other widely used language with type-inference). One would be forced to work with explicit type-constructors, functions would have to be 'lifted' (lift (+) :: (Int -> Int) -> (Univ -> Univ)) in order to operate on data of this sort, and would have to be 'flattened' again (Univ -> Int) to be of any use in order to interact with the outside program.
One rebuttal has been made is that the blame lies /not/ with type-systems in general, but how they are currently used and implemented.
And so I attempt to debunk this claim, by stating that the perceived shortcomings of latent typings lie not with the concept as a whole, but with how (the majority of) current languages (Ruby, Python, PHP) go about it. I should mention now that I am most familiar with Scheme (and Lisp in general) and intend to use this to put forward my arguments.

Static typing is essentially a method by which a program can be mechanically checked to guarantee that when two functions (f and g) are composed (f o g)( x ): x belongs to the domain of g; the codomain of g is the domain of f; and as such all functions and/or operators are consistent in this fashion. I know very well that static typing has a much greater potential than that (as evidenced in the possibilities of dependent types, GADTs, type/module hierarchies and so on). This checking is performed during program compilation (in other words, prior to the program actually being run) and does NOT add any capability or structure to the code, and has no effect upon the execution of the algorithm.

Many modern (mostly dynamically typed) functional languages are implementing a form of compile-time metaprogramming, and allow direct access to manipulate or query the source code of the surrounding program. My question is, isn't static type checking already possible to implement through that, and therefore a dynamically-typed programming language with metaprogramming features (like Lisp) is MORE expressive in the criteria of compile-time validation. PLT Scheme programmers will be aware of this if they've ever read up on or used MrSpider and/or MrFlow.

Of course, statically-typed languages with such features would be capable of doing the same. But I'd like to digress for a moment to say that the pain of Template Haskell, F# and integrating features like macros on them is plain hell.
Anyway, to deny the above the above statement (not about the criticism of Template Haskell which is sure to start a flame-war) is plain hypocritical for advocates of static-typing and the argument about its superiority previously mentioned. A programming language with features allowing compile-time reflection and processing would easily be capable of isolating a few-modules, marking them 'typed' and sweeping them with the Hindley–Milner magic.

Of course, this would all be quite impractical. Implementing / extending a type-system is a difficult task (even though so far I'm cool with the current and most popular soft-typing attempts) but the same could be set for the Universal type constructor and all the baggage that comes with it. Getting the two worlds to talk to each other is a pain.

Static typing is a limited form of compile-time sweeping. Q.E.D?

Once again, the playing field is level, and the choice between the two is almost entirely about preference.