let's talk about qi

https://en.wikipedia.org/wiki/Qi_(programming_language)

Copy pasted example of defining a type for a sorted list.

(12+) (datatype ordering

if (number? X)
if (number? Y)
let Z (* X 2)
if (= Y Z)
__________________
[X Y] : ordering;)
ordering : unit

(13+) [2 3] : ordering
error: type failure

(14+) [2 4] : ordering
[2 4] : ordering

>>50

Nobody cares about your individual case.

Of course people care. See any disaster caused by a logical error in software.

>>51

The purpose of a type system isn't to catch all your mistakes automatically.

These aren't worth much.

You can make mistakes while defining the types but the types are only a small part of the logic, and easier to get right. Doing this will allow the compiler to check important parts of the rest of your logic.

The types you are talking about have no logic to them at all. They're just names and maybe they have a partial order of subtypes.