I have a previous post about static and dynamic types [1] and I think I still agree with everything my past self said. However, I think there’s a couple additional points that I can make now that I either couldn’t think of a good way to say previously or have come up with since my original post.
The typical discourse seems to be that those in favor of statically typed languages indicate that their programs ‘just work’ while those in favor of dynamically typed languages will say that static types get in their way and their programs totally just work as well.
I think the position of static type system proponents can be disingenuous. A static type system isn’t going to solve all of your problems; it’s just going to ensure that your “micro” interfaces line up correctly. This will keep you from using an integer instead of a list of integers, but it isn’t necessarily going to prevent you from building a program that violates the semantics of the problem you’re actually trying to solve with your program.
Consider if you had a Haskell like language, but you only used tuples and integers. It doesn’t seem like the type system is really going to be helping you very much with ensuring that your program solves the problem at hand correctly. However, on the other hand, if you had a Lua like language, but it was also equipped with algebraic data types and pattern matching. *That* language would probably help you encode and represent your problem and greatly assist you in coming to a correct solution even without static checks.
Additionally, learning a type system isn’t free. There’s a lot of potential work to do in order to be able to effectively handle a type checker. Some of that work is understanding the type theory that they were implementing (and there’s more than one possibility to choose from), and some of that work is understanding the implementation details that affect what you’re able to do. Sometimes the things that you want to do, which make perfect sense and are completely consistent and safe, are not allowed because of theoretical or implementation artifacts.
Finally, those who are really good at programming in dynamically typed languages are running a kind of a type checker in their minds. They understand the nature of what their functions accomplish and they’re able to ensure that they work correctly with the rest of the program. They don’t have to wait for anyone to figure out how to type check what they’re able to work out for themselves.
But that isn’t the final paragraph … is it? So far this post *sounds* like it’s in favor of dynamically typed languages, but this is really a pro-statically typed language post. However, before I went into how I feel about static typing, I really wanted to point out that dynamically typed proponents have legitimate view points and concerns.
My first point was that micro interface type checking (or perhaps I should say sub-semantic type checking) isn’t all that great. And I think before you get the hang of dealing with a type checker like what Haskell or ML provides this *is* a thing that is very frustrating. Mysterious “failed to unify” statements that you have no control over complaining about silly things that just work in other mediums really hurts and that’s not a problem you can just ignore. However, once you do get the hang of it … not understanding stupid things that don’t work really hurts, and the last thing I want to do is have my program produce incorrect output because I forgot that the function I’m calling returns a “List (Maybe Int)” and I’m mistakenly believing it returns a “Maybe (List Int)”. Having something sit there and tap me on the shoulder to help me with silly mistakes that don’t have anything to do with the actual problem I care about is actually really nice because it means I can put more of my effort into thinking about the problem I actually care about. If my program type checks and it still doesn’t work, I don’t have to worry about a lot of types of errors because the type checker already took care of those problems. I can devote all of my cognitive effort towards the problem that matters.
Additionally, I mentioned that a language with algebraic data types and pattern matching, but no static type checking might be just as good as a language with static type checking. However, advanced techniques allow you to push more and more of your real world problem’s semantics into the type system. Phantom types, general algebraic data types, dependent types, etc. If we can use advanced techniques to represent the problems we care about in the type system, then we can not only get automatic assistance in checking for stupid mistakes, but we can get similar assistance in checking for big relevant domain specific mistakes.
Finally, I’m not exactly sure where else dynamic typing has to go. It would be nice to be pleasantly surprised by new developments in what you can do with dynamic typing, but I suspect there’s not that much more you can do with it. On the other hand, the ultimate goal of static typing is to be nearly as permissive as a dynamically typed language, but also provide you with checks on low level mistakes, checks on semantic mistakes, and even suggestions for how you can proceed with a problem when you get stuck. Today I don’t think it’s fair to tell everyone that they need to switch to a statically typed language, but I believe that tomorrow it’s going to be more easy and also more compelling to be solving your problems with a static type checker.
No comments:
Post a Comment