The Ergonomics of Type Checking (2016) (michaelfeathers.silvrback.com)

We still use Grails at work. Kill it. Kill it with fire.

Apache Groovy's worked quite well as the "Bash of the JVM", though other JVM languages have been moving into that space lately. Clojure's also quite good for running tests -- its macros can easily eliminate clutter in repetitive tests. Kotlin's been chosen by Gradleware as their preferred language for writing Gradle plugins and build scripts. And Scala doesn't really need glue code for tying its classes together because it can do that itself. Virtually no-one's ugraded Grails to version 3 since it came out over 2 years ago, or starting new projects with it. Groovy's adoption is dropping fast, e.g. it slipped out of Tiobe's top 50 a few months ago, and some robot running in Germany is responsible for most of its downloads.

Not sure if this is exactly what you're asking but one can reassign variables to change their types in Python:

    >>> x = 1
    >>> type(x)
    <class 'int'>
    >>> x = 'foo'
    >>> type(x)
    <class 'str'>

It depends on the type system, but often all usages are taken into account during type inference.

That would still fall under the umbrella of "type inference"

If you want to learn more about this, the Damas Milner unification-based algorithm used in ML, Haskell and others is a must-read starting point. It does global type inference of all types in the program without requiring any annotations, by analyzing how the types are used. It also can detect when a variable is only passed around, without being used in primitive operations, in which case it infers a generic/parametric type for it.

Coming from C++, take a look at OCaml, and specifically it's object-oriented facilities. It does exactly what you want, but in an usual (for a C++ coder) way - by making objects structurally typed. Suppose you write a function like this:

   let f(x, y) = x#foo(y#bar(x))

`#` is the member access operator. So this is a function that takes two objects (strictly speaking, it takes a single tuple of two objects), calls the method `bar` on `y` passing `x` as argument, then calls the method `foo` on `x` passing the result of the previous call as argument, and finally returns the result of that. Nowhere are the types declared, but they are fully inferred and statically checked. The actual type of `f` is rather convoluted when written out fully:

   (<foo: 'b -> 'c; ..> as 'a) * (<bar: 'a -> 'b; ..>) -> 'c

The `<>` notation means "object", with members listed inside delimited by semicolons. `foo: 'b -> 'c` means that there must be a member named "foo", which is a function that takes a single argument of some type 'b, and returns a value of some other type 'c - these are like template type parameters in C++, except you don't have to declare them. Finally, `..` means "and any other members" - without it, our function would only accept objects that have only the member named "foo" with the designated signature. So, `<foo: 'b -> 'c; ..>` means "any object that has method "foo" that takes a value and returns a value, and also possibly some other members". The `as 'a` part then assigns another type parameter to describe that object for reference later.

Then we see the object type for the second function argument, which is `<bar: 'a -> 'b; ..>`. This is structured in the same way, but note that it uses type parameters with the same names as before - this indicates that they must be the same type. This makes it possible to make the definitions recursive; the entire bit before `-> 'c` at the end can be described in a more verbose fashion like so:

"A tuple, the first element of which is an object, with method "foo", taking an argument of the same type that is returned by method "bar" of the second element of the tuple, and returning a value of any type, and possibly some other members; and the second element of which is an object, with method "bar", taking an argument of the same type as the first element, and returning a value of the same type that method "foo" takes as an argument, and possibly some other members."

Note that you don't actually need to write any of this. You can explicitly declare the type of "f" if you want to, but the compiler can figure it all out by itself, just by looking at the body, and will print out the type for you. It will also statically verify how the function is used. So, this is okay:

   let a_foo = object
      method foo y = y + 1
   end;;
   let a_bar = object
      method bar x = x#foo 0
   end;;
   f(a_foo, a_bar)

But on the other hand, this:

   f(a_bar, a_foo)

gives a compile-time error for the first argument:

   This expression has type < bar : < foo : int -> 'a; .. > -> 'a >
   but an expression was expected of type < foo : 'b -> 'c; .. >
   The first object type has no method foo

And this:

   f(a_foo, a_foo)

gives an error for the second:

   This expression has type < foo : int -> int >
   but an expression was expected of type < bar : < foo : int -> int > -> int; .. >
   The first object type has no method bar

(OCaml also has classes, but their sole purpose is to provide a common implementation for objects, and to allow code reuse and extensibility via inhe...

Check out the hindley milner type system [1]. It's used by haskell and some other languages, and allows for a very extensive amount of type inference. You can often write large sections of code with no type annotations and the compiler can figure out the most general type based on the type of some function called somewhere, which means the thing you did with that result must be of a certain class of types, which makes the surrounding expressions' types have to be a certain class of types, etc etc.

[1] https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...

This is a well explored area. Wikipedia article is short but has some good references [0].

Languages like Haskell, OCaml, F#, and Elm use global type inference.

Languages like Scala and TypeScript use local type inference. TypeScript in particular uses flowed type inference (there might be a more formal name for this). For example:

  let a = document.querySelector('#a') // typeof a is Element | null
  
  if (a == null) throw 'not found'     // typeof a is now Element

[0] https://en.wikipedia.org/wiki/Type_inference

So no two classes anywhere in the entire project can have a method with the same signature?

I should have qualified that with the presence of type parameters (nominal subtypes without type parameters are still easy to deal with). Without subtypes, you only unify X and Y (so X = Y), where X and Y are trees with open variables. It turns out X < Y is much harder (semi unification rather than unification).

It is basically equivalent to an alias analysis with imperative assignments (subtypes) and fields (type parameters).

A `String` in Java has a `.length()`, not a `.size()`.

Apologies! I meant to include a comment pointing out the error (as Thiez writes, it should be length, not size), but that somehow didn't make it into the comment as published. I blame my sub-editors, can't find the staff these days.

Do they really insert extra dynamic checks?

Is Sound Gradual Typing Dead? https://news.ycombinator.com/item?id=11041272

http://prl.ccs.neu.edu/gtp/research.html

It was my understanding that MyPy was purely compile time with no runtime checks. But I could be wrong. Gradual Typing as implemented in the original paper would lead to much much slower code. The weight of a static language bolted onto a dynamic runtime for the worst of both possible worlds. Sufficiently abstract Python code is almost un-typable.

I think eventually we will get there, where one can explore a program in a dynamic language and ship a correctly statically typed one. Types are only the beginning.

What prevents you from writing the exact same exceptional code in a static system? I'm not sure I understand your point.