It would be great to have a notion of type that would actually pay for itself in real clarity. For example, what would be really useful in many dimensions is "semantic types" rather than value oriented types (which I don't think are particularly valuable enough).