It's useful for things that would be too painful to enforce via types. For example, "this list should be non-empty" is pretty easy to enforce via types (use a p

It's useful for things that would be too painful to enforce via types. For example, "this list should be non-empty" is pretty easy to enforce via types (use a pair of head element and possibly-empty tail list). On the other hand, something like "map of non-overlapping date ranges to counts, with automatic splitting on insertion" would be pretty tricky. It's easier to state the desired properties as universally-quantified functions rather than types, at which point we might as well throw them into a few property checkers to see if they find anything we didn't think of.