This is a good point. The poster then proposes being able to nail down your types progressively -- which I think is fine as a long as you don't let the iteration cycle get too long.

Optionally typed languages are one way we approach this ideal. Another way is linters that are stricter than the compiler itself. You must run the compiler to have testable code, but you can run the linter later, perhaps only as part of CI.

It is possible that in future, both of these approaches will look like primitive exteremes of some richer process progressively nailing down the static safety of a program.

An incremental Java compiler. Implemented as an Eclipse builder, it is based on technology evolved from VisualAge for Java compiler. In particular, it allows to run and debug code which still contains unresolved errors.

That means that you can write something like:

    private void describe(String string) {
        if (string.isEmpty()) empty();
        else nonempty(string);
    }
    
    private void empty() {
        System.out.println("empty");
    }
    
    private void nonempty(String string) {
        System.out.println("contains " + string.size() + " characters");
    }

It's one of the few things from Eclipse i miss when using IntelliJ.

[1] http://www.eclipse.org/jdt/core/

Bingo. I love this idea. I haven't tried it yet myself, but I think mypy [1] from Dropbox makes this a reality today in the Python world.

[1]: http://mypy-lang.org/

Live the dream :P

http://mypy-lang.org/about.html

Dropbox employs the creator of MyPy but it isn't a creation of dropbox.

Type Systems as Macros http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf

Pluggable Type Systems http://bracha.org/pluggableTypesPosition.pdf

Propositions as Types http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...

https://www.youtube.com/watch?v=IOiZatlZtGU

Are you sure that gradual typing is different than what Mypy supports?

The Wikipedia page for gradual typing cites mypy as an example.

https://en.wikipedia.org/wiki/Gradual_typing

The Mypy docstrings specifically state:

> Mypy has a powerful type system with features such as type inference, gradual typing, generics and union types.

https://github.com/python/mypy/blob/272d0c4c50918a36b57e7c0c...

The section on gradual typing in PEP 483 seems consistent with this as well.

https://www.python.org/dev/peps/pep-0483/#summary-of-gradual...

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.

It looks like there are some active projects for runtime type checking in Python and while I don't believe Mypy is related to any of them, enforce [1] looks to also use the same standard type hinting syntax from PEP 484.

[1]: https://github.com/RussBaz/enforce

To provide some context: my first experience with static (or rather explicit?) typing was TypeScript, and I really liked what I saw.

declare(strict_types=1);

is checking and throwing type errors at runtime, not compile time.

Edit: example to further clarify what I meant (it's a bit more than type inference at initial assignment)

    var x = readUserInput(); // narrow down: string, int, double
    x += y; // if y is also a user input, no change
    x += 1; // narrow down to int, double
    p = x % 2; // narrow down to int

An example is Crystal; [edited] example from the website:

  if rand(2) > 0
    my_string = "hello world"
  end
  puts my_string.upcase

  Execution:

  $ crystal hello_world.cr
  Error in hello_world.cr:4: undefined method 'upcase' for Nil (compile-time type is (String | Nil))

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

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

But gradual typing means avoiding typing alltogether in some parts of the program and in some sense going against the inferred type. This is probably most relevant in Haskell where IO is typed, and less so in others, e.g Clojure.

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.

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

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

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)

   f(a_bar, a_foo)

   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

   f(a_foo, a_foo)

   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

Effectively, this is static duck typing. This all looks a great deal like C++ templates, in that you can "just do" things, and the validity is effectively determined at the point of use. However, because it is captured at the type system level, the point of use doesn't have to see the implementation of your "template" to typecheck it - it just checks the arguments against the type signature that it computed when the "template" was defined. This also means that `f` is an actual function - not really a template - and so it can be passed around, stored in a variable etc (which in C++ is only possible for specific instantiations of a template).

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

Also, I believe the work you are citing above explores structural subtypes, not nominal ones.

    pair x y = (x, y)

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

Also, I'm not sure how a union type could be distinguished from an error during type inference. Maybe a nullable, but otherwise it'd be very tricky.

Even languages with overloading dont allow them in the same namespace if they also have the same signature.

It is also possible for the compiler to use type information to attempt to disambiguate. Especially because this would normally happen across module boundaries, a hypothetical compiler could:

1) Infer types based on all non-ambiguous references (or all references within the compilation unit that contains the definition)

2) Disambiguate all ambiguous reference using type information.

I suppose a sufficiently smart compiler could attempt to do type inference and disambiguation at the same time; but that sounds like introducing NP hard problems to the compiler for the sole purpose of allowing confusing code.

I quite like the pattern of having fully typed interfaces and type signatures while letting the body of a function be dynamic where it makes a big difference to expressiveness. Like a hard shell with a soft inside.

Nowadays if it wasn't for Gradle, I bet it would have been gone by now.

For the other part of your question, it depends a bit what you mean by "without the need for object orientation". Groovy definitely relaxes a lot of the strict object orientation of Java. However, since it is based on the JVM it doesn't have platform support for core functional features like tail recursion and immutability. Groovy adds a number of features to add support for these, but as with all such features added after the fact, they aren't as good or reliable as if it was built into the core platform.

Groovy's forte is really in how it makes Java massively more developer friendly while staying within the original philosophy and maintaining full compatibility with Java. This is where I think it wins over Scala and other JVM languages which introduce their own types and radically different design philosophies. The integration of Groovy with Java is nearly completely seamless, and that's where I think it's actually really awesome for enterprise systems.

I still use Groovy to write quick scripts or cron jobs that need to use Java libraries. Basically the Bash or Python of the JVM. Otherwise there are much better choices.

I've never worked on an "enterprise system, not web based," so I'm not sure what it is, but it sounds important and large. I wouldn't write such a thing in Groovy, or any other dynamically typed language: one misspelled variable and you have a runtime error waiting for you. (I wouldn't write such things in Java either: one missing null check and you have a runtime NPE waiting for you. But alas, the industry thinks otherwise.)

PS. Whatever you do, stay away from Grails. I've never seen such a bug-ridden, slow and crappy piece of junk in my entire career. And when I say bug, I mean a running production system suddenly starting to omit all WHERE clauses from all SQL queries, out of the blue. The app still working properly, but customers seeing the data of all other customers. I'm not joking.

That’s a shame because typescript is basically this. Typing is optional, and you can become more granular as you want.

Perl 6 does this.

Granted, (almost) nobody is using it, but it does exist (finally!).

Back in like 2006 they were estimating that all of the stuff they wanted to put in 6 would require until 2016 or 2017 to complete. I figured that was a comment meant to negotiate down the scope to something reasonable.

Turns out, no...

[0] https://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typin... [1] https://github.com/samth/gradual-typing-bib

C++ 'auto' type. Workflow:

1. Write 'auto =', see what the compiler picks up (iterator of a vector of a set of classes that points to a list of structs, etc).

2. Potentially copy/paste that (unless the line is bigger than 350 characters :) )

> they exist, but I don't use them.

:/

The author's thoughts (I want to write dynamically to get the code working, but then make it static afterwards) are nearly the exact thing I've heard from Matthias Felleisen when he talks about the motivation behind Typed Racket.

http://mypy-lang.org/index.html