0, null, unknown, invalid, (ad infinitum)

It very much depends on your problem domain. In many cases the functions to be computed are primitively recursive ones, in particular in databases. In those cases Rice's theorem is not applicable, and the type system can actually contain all necessary semantic information. Coq and by extension Lean are practical examples illustrating that point (not for databases, though).