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
See Also: LinesOfCode