This is just an idea off the top of my head. Is it possible to mathematically prove that a type-heavy language can always express the same algorithm as a type-light or type-free (no type-tag) language with the same or less amount of code? Or vise-versa? If not a mathematical proof, then at least a compelling argument.

This is related to the continuing argument over whether heavy typing increases "code bloat" or not.
----
To start with, we need to clarify what is meant by type-heavy, type-light, and type-free.  Do you mean StaticTyping vs DynamicTyping, ManifestTyping vs ImplicitTyping (aka TypeInference), StronglyTyped vs WeaklyTyped, some specific combination of these, or something else?

'''Definitions to be Used On This Page'''

* '''Type-heavy''' -- place definition here, please.
* '''Type-light''' -- place definition here, please.
* '''Type-free''' -- Languages such as BCPL or ForthLanguage lack either static or dynamic types.  Only bytes or natural machine words (generically referred to as ''cells'' in Forth, ''words'' in BCPL) are available to program with.  The burgeoning thought is that ''types'' are semantic constructs to be built by the user, either enforced by the language's module system or encouraged by the language's (or project's, as the case may be) module ''convention.''

-------
See Also: LinesOfCode