As a Haskell programmer I never feel the need to add any form of dynamic typing. In practice dynamic typing makes it harder to build programs, not easier.
I'm the first one to admit that Haskell's type system has a somewhat steep learning curve. But after a while, when you internalize it and learn to pattern match on GHC's type errors, day-to-day programming will become easier.
> In practice dynamic typing makes it harder to build programs, not easier.
OTOH, static typing could make writing some kinds of programs impossible. In an interview, Joe Armstrong of Erlang fame said that they tried hard to put a type-system on top of Erlang, but they have not been able to.
IMO, static-typing should be optional, that is: you should be able to run a static-typing checker on your programs, without being constrained by it at every step.
No, JA told that they planned to add type system, but their users didn't feel they need it.
And, actually, they added types into Erlang: dyalizer.
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...
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.
> OTOH, static typing could make writing some kinds of programs impossible.
Often, these turn out to be incorrect programs or programs without a good structure/architecture. It is my experience that static typing makes it slightly harder to write the first version of a program, but subsequent alterations become an order of magnitude easier. For me, this is worth it, since alteration and maintenance are the largest part of most program's life cycles.
There are times when you wish you had dynamic typing, but this is usually a fault of the type system and there are better answers than ripping the type system out entirely, once you ascend to a mathematical way of looking at it.
Suppose for example, that you wanted an existentially qualified list, something like forall a. Ord a => [a], and to be able to mix variables of different concrete types in that list. Well it's a slight pain to do that right now.
This goes back to the classic adage, the answer to broken maths is... MOAR MATHS!
Anyway, I would like a switch that would let you do that, even if it means adding a type sig. A better switch might be a LANGUAGE pragma, because this is one of those things you either really don't want at all, or you want it really badly.
> There are times when you wish you had dynamic typing, but this is usually a fault of the type system and there are better answers than ripping the type system out entirely, once you ascend to a mathematical way of looking at it.
Indeed. Having a static typed language means that you are tied to a single static-typing system. OTOH, I guess you could apply different type checkers to the same dynamically-typed program.
I'm the first one to admit that Haskell's type system has a somewhat steep learning curve. But after a while, when you internalize it and learn to pattern match on GHC's type errors, day-to-day programming will become easier.