(defn f [^String s] (.length s))
  (f 3)

  class X { public static int f(String s) { return s.length(); } }
  X.f(3)

Clojure functions are compiled into implementations of clojure.lang.IFn - you can see from https://clojure.github.io/clojure/javadoc/clojure/lang/IFn.h... that this interface simply has a number of overloads of an invoke method taking variable numbers of Object parameters. Since all values can be converted to Object, either directly for reference types or via a boxing conversion, no type checking is required to dispatch a call. With a form like

  (some-fn 1, "abc", (Object.))

Protocol methods just get compiled into an implementation of IFn which searches for the implementation to dispatch to based on the runtime type of the first argument, so it doesn't introduce static type checking in any way.

  (defprotocol P
    (method [this ^Integer i]))

  (extend-protocol P
    String
    (method [s i] (.substring s i)))

Of course there's no requirement for Clojure code to be AOT compiled anyway so in that case any name errors will still only be caught at runtime when the compilation happens.

Type hinted bindings are only converted into a cast and are not checked at compilation time either e.g.

  (defn hinted [^String s] (.length s))
  (hinted 3)

deftype is only used for Java interop an is also not a form of type checking. The methods will be compiled into Java classes and interfaces, but the implementations defer to regular Clojure functions which are not type checked. You can only make use of the type information by referencing the compiled class files in Java or another statically typed language, using them from Clojure will not perform type checking.

    Maybe foo = null;
    foo.map(s -> "bar");

    Optional foo = Optional.empty();
    String message = foo.map(s -> "Hello " + s).orElse("Fine, leave me hanging");

    validateEmail :: String -> IO ()

    validateEmail :: String -> Either EmailError ValidEmail

> But via an optional type you guarantee that it's handled

It's not 'handled', which is the point. There's no default value so you have no option but to propagate the missing value. Callers that establish the precondition still have to deal with an Optional value even though it can't be empty. Callers which establish the precondtion through the types receive a more precise type and don't have this problem. Callers that establish the precondition in the more simply-typed version (Int, Int) -> Int also receive an Int. Only your version imposes the imprecision on the return type.

> There is nothing wrong with using a Maybe monad here. There is zero reason why you need to throw an exception.

The Optional[Value] returned from a map lookup is used to incidicate the possibility of a missing key, which is an expected outcome of the operation itself. Passing a null map represents a structural error in the construction of the program at the point the call is made. If you represent both in the same type you can't distinguish these two cases.

> You now have a hole in subtraction as 3 - 3 would be a singularity.

There's no hole here, subtraction on NonZero just has to return Int instead.

> If it comes from IO anything goes, you have to be prepared for Anything

Yes, if it comes from user input you have to establish the property dynamically. Encoding the property in the argument type forces you to actually do it (whether statically or dynamically), and help you push the constraint to the highest level. Putting the optionality in the return type doesn't force you do do this, and imposes a cost on every call that actually does.

I've explained why it matters - the types are more precise in my version and if you start from that you can always throw away the extra precision if desired to get to your version. You can't go in the other direction, so starting from your version makes it impossible to safely recover an Int from the returned type of Optional[Int], even if you've already established the precondtion beforehand.

> There is 100% casting in your version

Creating an Optional[Int] from an Int is a conversion, not a cast. I thought it was obvious from the context but for the avoidance of any doubt, by 'casting' I mean an unsafe narrowing conversion. Optional[Int] is a larger type than Int, so it's trivial to create one from an Int:

    def pure(x: Int): Optional[Int] = Just(x)

    def fromOptional(o: Optional[Int]): Int =
        match o with
        | Some(i) => i
        | Nothing => ...

> Imagine a map with RGB colors as keys.

Your example doesn't make sense, what would you expect (lookup Map.empty Red) to return? The optional return value is used to represent the key being missing in the map. Nonetheless the point I was making is that you wouldn't return Nothing from such a function in the event of a precondition failure e.g.

    def lookup(m: Map[K, V], v: K): Optional[V] =
        if m is None return Nothing
        ...

> This prior point involves the creation of the type NonZero[Int] which involves: NonZero.fromInt

No, this is not necessarily the only way to create instances of NonZero. You could have a PosNat subtype with members one: PosNat and succ: PosNat -> PosNat. You could have a non-empty list type with a length member.

> Every other mathematical operation (+,-,x^y,/,) returns an Int not a NonZero[Int]

They don't return Optional[Int] either so I don't see how this is relevant. There's no reason the input has to come from some application of a different operator, it could come from configuration, user input, a property from some other type etc. The question is whether and how to model the constraints in the type. The constraint exists in the argument so it makes sense to constrain the input type, not widen the output.

> Notice how the above two sentences are the same?

Yes, if all you want to do is avoid establishing the property you care about and silently propagate some information-free 'failure' value to the top level, then you can do it either way. But the entire point of encoding properties in the types is to force you to establish them. These statements highlight the difference:

1. I've established the divisor is non-zero, called myDiv, received an Int and continue

2. I've established the divisor is non-zero, discarded that information to call yourDiv, recieved an Optional[Int] which cannot be empty, but which must be propagated. You could immediately unwrap the value but now you're just re-creating the dynamic behaviour of a function (Int, Int) -> Int which you've already rejected.

The reason you can't write my version using yours is that the types are less precise and you can't recover the imprecision in the output type after the fact. The only safe way to obtain an Int from an Optional[Int] is by providing a default value which doesn't exist in this case.

> The Optional[Int] doesn't exist so how do you create it?? You CAST

By casting I mean an unchecked narrowing conversion e.g. of the type Optional[Int] -> Int. There's no casting in my version.

> if you want to talk about "Well Established" then Optional is more well established

This is a false dichotomy, contracts are still used in static languages where you can't or don't want to try represent properties at the type level. You could for example define a function

    lookup: Map -> Key -> Optional[Value]

> The safe version suffers from your same problem just moved

It didn't 'just' move, it moved to the point in the program you actually need to deal with the possibility of a zero divisor i.e. before calling div. Where does the divisor come from in the first place? You seem to be assuming there is necessarily some call to NonZero.fromInt at each call site to div but this is wrong. The non-zeroness of the divisor could be established at some prior point in the program and used in multiple places. In contrast your version has to deal with the possibility of returning None everwhere even if you've already established the property of the divisor beforehand.

It's not arbitrary since it's possible to write your function using mine but not vice versa. If you disagree then please implementing the following function without casting:

    def convertDiv(f: (Int, Int) -> Optional[Int]): (Int, NonZero[Int]) -> Int

The convention that callers are responsible for upholding the preconditions of the functions they call is well established: https://en.wikipedia.org/wiki/Design_by_contract. You obviously can't fix precondition violations by checking the result after the fact.

> Also Your unsafe version is again worse because it will trigger an exception on zero

That is the point of the unsafe version, yes. Sometimes you will statically know the argument is non-zero e.g. NonZero(3). If you want to avoid an exception then use the safe version.