Begin reading from "Through the years, there were some attempts to build type systems on top of Erlang..."
> And, actually, they added types into Erlang: dyalizer.
Yes, and they did it right: type-checking should be a task performed by a different tool.
> As for optionality of static types... What is your experience, precisely? My tells me that type systems are, actually, your partners in program development. Quite intelligent partners - Haskell type system, Agda2 type system...
I do agree that static type systems are very helpful. What I don't like about them is that most incarnations of them force your program to be type-correct all the time. This is not the case when you are sketching a solution, or sometimes while fixing/improving code. Sometimes I was working on some part of a software, breaking the static typing of the program as a whole along the way, and the compiler kept complaining until I had fixed or commented out some other (currently not impacted) part of code. I've found that to be very annoying. I would have very much preferred such type errors to be just warnings until I was ready to finalize my fixes.
> I think that they require your program to be correct at the time of checking.
I don't understand: static typing requires all the source code - and I stress "all the source code" here, which encompasses code not reachable too, rather than the just the code you are working on - to be type correct, otherwise your program will neither compile nor run.
> Looks much like Visual Studio. Am I right?
Yes, but aren't all static typed languages the same? I've found that to be the case with C++, Java, Haskell.
I know a different story.
http://learnyousomeerlang.com/types-or-lack-thereof
Begin reading from "Through the years, there were some attempts to build type systems on top of Erlang..."
> And, actually, they added types into Erlang: dyalizer.
Yes, and they did it right: type-checking should be a task performed by a different tool.
> As for optionality of static types... What is your experience, precisely? My tells me that type systems are, actually, your partners in program development. Quite intelligent partners - Haskell type system, Agda2 type system...
I do agree that static type systems are very helpful. What I don't like about them is that most incarnations of them force your program to be type-correct all the time. This is not the case when you are sketching a solution, or sometimes while fixing/improving code. Sometimes I was working on some part of a software, breaking the static typing of the program as a whole along the way, and the compiler kept complaining until I had fixed or commented out some other (currently not impacted) part of code. I've found that to be very annoying. I would have very much preferred such type errors to be just warnings until I was ready to finalize my fixes.