Yes - I understand why some people are keen on static types, but type inference is a powerful way to create funcetionality and I believe that the separation of concerns between the dispatcher and the programming code (removing the logic of decisioning from the code and using type inference instead) leads to clearer programs. I can't think how you can have that and have static checking as well (although I know that there are some compilers for some Julia code as mentioned in this thread)

Lots of languages with static typing use type inference. Haskell, OCaml, Go, Rust, Nim, etc. Even C++ has auto these days which I think when combined with templates gives you what you're talking about though it is a bit clunky.

EDIT. For instance in Haskell I can just declar a function to sum the things in a container by saying

  summer a = folder (+) 0 a

And the compiler will figure out that the function accepts a Foldable container of some sort full of things that are Nums without ever having to tell the compiler that (though it's a good idea for maintainability. And then I can just pass in a list of floats and the compiler will Do The Right Thing. And if I pass in a list of booleans instead the compiler will yell at me at compile time because there's no (+) operation for booleans.

I think he possibly phrased it wrong. Dynamic languages don't do type inference, they carry type with each value at runtime.

Dynamic and statically typed languages each have their own wonderful advantages. There is just no way of replicating all the advantages of dynamic typing in a statically typed language.

It is hard to sum up why in a short sentence but I have tried to articulate it in a longer article here:

https://medium.com/@Jernfrost/the-many-advantages-of-dynamic...

Keep in mind this focuses only on advantages of dynamic languages. It does not mean I don't consider that static languages don't have their own unique advantages, but that was not the topic of my article.

The primary problem with static typing as I see it is the complexity and mental overhead it adds. It is not just the complexity in the type system and the language itself, but also in the tooling surrounding it: build system, dependency management, binary interface definitions, debuggers, REPL etc.

The complexity makes meta programming very hard to do for a software developer of average intelligence.

Where I see a use for advance static languages is for very specialized systems which need a high level of correctness and where a company is able to do the job with a small team of very bright people.

For me static typing removes mental overhead. I have fewer things to keep in my head, I can trust the tools to have my back and point me to where I did stupid mistakes. It makes reasoning about the code more local.

Also you can have static typing in an interpreted, interactive setting, with any language that has a REPL. That's even how the ML family started.

Peace of mind is not quite the same as what I meant with mental overhead. What I am referring to is that static type systems have far more complex type systems and semantics, which occupy more brain real estate.

And complexity tends to explode because it carries over to the tools. Static languages require far more complex tools to work with.

I did not mean static languages cannot have REPLs but my experience with them have not been great. They seem hamstrung in a way I cannot articulate well.

Reading through that Medium post makes me think that maybe the author has never worked with a large code base written in a dynamic language and is attributing the difficulties of large projects to them being written in static languages? My day job involves a large amount of Python and we certainly use CMake to bundle it up for deployment, use YAML configuration files, worry about library version compatibility, and all of the other problems the author ascribes to static typing.

Dynamic languages do do type inference. Or at least they can.

Julia does type inference at compile time. The difference is that it doesn't have to succeed.

If you write type unstable code then it won't.

Yes... but I feel that is more like an implementation detail. Semantically speaking you don't think of Julia as doing type inference.

Semantically speaking expressions don't have types and the type of expressions are never inferred (however they are inferred at compile time as an implementation thing for the JIT).

My point is that you can make an alternative Julia implementation that did absolutely no type inference and everything would work just fine apart from possibly bad performance.

However you could not make a compiler for a statically typed language such as Haskell which did not do type inference. If you did programs would no longer compile.

At least that is how I interpret the difference. I could be wrong. You probably know this better than me.

Surely Haskell and Rust would be fantastic examples of languages that have static typing and excellent type inference?

Presumably this means that no one has implemented a suitable static type checker or its type annotations don't provide sufficient information for a static type checker to work in principle?

The problem is more the former (nobody has gotten around to it yet), but also a bit of the opposite of the latter, i.e. the type system is so rich, type-checking may be undecidable in too many contexts.

Julia's parametric types are incredibly rich. You can look up 'dependant types' which are similar in the static world and see the sorts of hoops static language designers jump through to have dependant types and still be able to reliably prove theorems.

What you can do with Julia types is far more advance than I think you can do with any statically typed language.

I can add a type annotation in Julia which is a function call which returns a type e.g. This function can be of any complexity.

I think a better approach is simply a Linter. You report type problems you can find and ignore the rest. Not point trying to figure out the more advance Julia cases.

I would assume 90% of Julia code will use types in a pretty straightforward manner and thus would be able to be analyzed by some sort of Linter. Lint.jl e.g.

You're describing optional type systems; in this regard, Julia is on par with Python or TypeScript. The linter you're describing is also a type checker (like Python's Mypy). That said, it would be really interesting if someone would make a type checker that would evaluate/resolve those more complex types, at least those that can be guaranteed to terminate.

Optional typing and what Julia does is quite different. Julia type system is nothing like Python or TypeScript.

In Julia type annotations are not just a sprinkle of sugar. It has a very concrete use beyond asserting type consistency.

Julia types are used to decide what code gets run and memory layout of data.

I wrote an article showing a (probably naive) way how it could be done, but also discussing some of the limitations. At the end I think it would be better to think about these kind of tool as partial, automated tests rather than full-blown static type checkers.

https://nextjournal.com/jbieler/adding-static-type-checking-...

You can do some form of type checking with stuff like Lint.jl. I mean since Julia uses a bunch of type information and Julia parses code into data structures which are easy to process, you can to a lot of your own type verification before running a program.

However I see Julia not being a statically typed language as a feature. If Julia was statically typed you would pretty much have lost everything that makes Julia a great language.

You cannot do multiple dispatch with a statically typed language efficiently.