[rraval]

> What statically typed language lets me define a type as “number between -180 and +180”, or “string which contains only alphanumeric chars”?

Pretty much all of them. Any simple predicate like this can be encoded with witness types.

Here's an example in Java, which is hardly the paragon of static typing (i.e. it's no Haskell/Idris/Agda/Rust/Typescript):

    class AlphaNumericString {
        private final String str;

        // use a fallible factory with a `private` constructor if you're
        // morally opposed to exceptions
        public AlphaNumericString(String str) throws AlphaNumericException {
            if (!str.matches("^[a-zA-Z0-9]*$")) {
                throw new AlphaNumericException();
            }

            this.str = str;
        }

        private static class AlphaNumericException extends Exception {
        }
    }

Now code can freely use `AlphaNumericString` and be guaranteed that it has been validated.

You may object and say that newtype wrapping is cumbersome but:

1. That's an argument about sugar and ergonomics, not about the semantics that the static type system enforces

2. Some languages make it easier to generate forwarding methods to the underlying type (a la https://kotlinlang.org/docs/reference/delegation.html)

3. The `AlphaNumericString` is describing a smaller set of values than `String`. In general, you should be strongly considering the methods you allow and make sure that all paths continue to enforce the semantics you intend.