You can also further generalize this idea by noticing you can encode all kinds of life cycle information in your type system. As you transform some data in a sequence of steps, you can use types to document and enforce the steps are always executed in order.

In this example, the user input validation step is f(String) -> ValidatedEmail, then the process of verifying it is f(ValidatedEmail) -> VerifiedEmail. But the same principle can apply to e.g. append() operation being f(List[T], T) -> NonEmptyList[T], and you can write code accepting NonEmptyList to save yourself an emptiness check. Or, take a multi-step algorithm that gets a list of users, filters them by some criterion, sorts the list, and sends these users e-mails. Type-wise, it's a flow of Users -> EligibleUsers -> SortedEligibleUsers -> ContactedEligibleUsers.

And then, why should types be singular anyway? You should be able to tag data with properties, and then filter on or transform a subtag of them. This is the area of theory I'm not familiar with yet, but I imagine you should be able to do things like:

List[User] -> List[User, NonEmpty] -> List[User[Eligible], NonEmpty] -> List[User[Eligible], NonEmpty, Sorted[Asc]] -> List[User[Contacted], Sorted[Asc]].

Or,

Email -> Email[Validated] -> Email[Validated, Verified] -> Email[Validated, Verified, Trusted].

I'm sure there's a programming language that does that, and then there's probably lots of reasons that this doesn't work in practice. I'd love to know about them, as I haven't encountered anything like it in practice, except bits and pieces of compiler code that can sometimes propagate such information "in the background", for optimization and correctness checking.