I think I am in general agreement with the viewpoint that typing should be optional not mandatory (see Is Static Typing a Form of Bad Coupling? and Plugabble Type Systems)
The one problem I have with this view is that most people who hold it seem to think typing should be a rarely used performance kludge. I’d also agree that typing should rarely be used as a performance kludge, but I don’t think that means typing should be rarely used. There are other reasons to use typing. Actually, there are quite a large number of them.
For me, the main justification has always been safety. Typing also has benefit as a form of documentation. Safety and documentation are things you want most of the time, not rarely, so why would you rarely want types?
I think one of the problems is that most people look at typing as a way that framework designers can restrict their users. But what if typing didn’t restrict users, but instead guided them? I think this would still meet the needs of framework designers. A framework change doesn’t need to have zero breaking changes. All it really needs to do is cover the reasonable points of view. If you provide a safety net, and your users tear it down, I don’t think any (reasonable) person would fault the framework designers for breaking those users.
A Metaphor
Consider programming like some kind of stunt in an Indiana Jones movie. In this stunt, you’re walking across a narrow beam, with a big pit of spikes down below. There’s also poison darts wizzing by from little holes in the side walls. Today’s type systems however fit into a few categories.
On type are harnesses that keep you from falling off, but they slow you down, and make you an easier target for the darts. These are your mandatory static type systems. Another type are safety nets, that let you fall, but at least keep you from hitting the spikes. These are the dynamically typed systems. You could go without a safety net at all, and save a bit of money and setup time. This would be assembler. Or you could go with a cheap and poorly designed harness. It would slow you down even more, and it might break and let you fall. This would be C or C++.
Although this metaphor isn’t perfect, I’d consider the darts to be complexity. You might be able to take one or two since the poison is somewhat weak, but there wizzing all over the place, and they add up. The spikes of course are the core dump that happens when runtime typing isn’t employed. Many static type systems employ both the harness and net, because the harness has a release latch. But this latch (reflection), is somewhat awkward and hard to use.
In the end we realize the best way through is a set of shields (unit tests) to protect us from the darts. But the only thing available to build these shields with is grass, and it takes a lot of grass to build a shield, since grass is kind of flimsy, our shields can only absorb so many darts. Plus we still have to worry about falling off and having to climb back up from our net.
I probably way over extended that metaphor, but it’s kind of catchy, and has a nice visual, so I’m keeping it.
Resolution
What I’d like to see is a type system that helps keep us from falling off, but doesn’t slow us down. I’m not sure how to represent this in my metaphor. Maybe as some kind of lightweight harness with a quick release/attach mechanism. When you have it on your sure you won’t fall, but if you need to do something that the cables are too restrictive for, you can detach. It’s important however that the choice to detach is not something that happens by accident. But it shouldn’t be hard to use either.
I think I’m asking for a lot here, but I do think it’s doable. If we could agree this was the way to go, we could start designing the syntax behind it. In a sense, we have all the basic ideas we need. The JVM and CLR provide just about all the necessary capabilities. The problem is that reflection is ugly and hard to use. We need a better designed latch. Even more important, we need one that’s designed for users who have a shield strapped to each forearm.
I'm afraid I may have blown the argument with that long drawn out metaphor, so I'll probably write about this again, but it might be a fun to read anyhow, so I'll publish.. really.. I'm doing it right .. now!
Posts
4 comments:
I think we should simply accept that static typing was a mistake, and duck typing+unit testing gets far more productivity and far more safety than any static typing system. The difference in performance is also typically not that big, as decent compilers can guess or JIT most of the time (and when they don't, throwing a few type hints at hot spots works quite well, as Lisp compilers show).
The best evidence that it's impossible is OCaml type systems for objects. It uses full duck typing - object "types" are defined only by their method signatures, their classes aren't considered at all. It has throughout type inference, and it automagically extracts interfaces, so if some function needs objects that understand method "foo", that's exactly what its type signature will say, without any work on your own. It is 100% statically safe - if something compiles, it must be type correct. This isn't even true in Java (covariance/contravariance issue). You can escape the type system by explicit casts, which throw exceptions if unsuccessful.
It lacks decent reflection, and the rest of the language isn't very oo. Other that that, it seems like almost the best type systems can do.
Now, I promised the evidence against type systems, not for them. So - take a few days and use object-oriented OCaml to implement some program. Whatever you feel like coding. When you finish, you will probably convert to "occasional compiler hints for performance" view of typing. Unless I'm wrong, you will think OCaml totally got it right. In either case, the question is solved.
I have looked into OCaml before. I never wrote anything in OCaml but I did write some stuff in F#, which is derived from OCaml.
I'll admit I got frustrated with that, but it had little to do with the language. It had more to do with the compiler breaking on me (something about a missing DLL).
Regardless however, I don't think OCaml is the end all of typing, and certainly doesn't fit in with the point of this post. OCaml is dogmatic about precision. From a scientific or theoretical perspective that's what makes the language so interesting, but it certainly doesn't make it easy to drop down to dynamic behavior.
Well, the interesting part is OCaml object system, not OCaml itself, and it would be nice to extract it and give it some sane syntax, to make the rest interfere less.
Obj.magic function is your escape. It is 'a -> 'b identity, so you are effectively telling the type system you're know it better. There are a few more limited casts too like :>.
Here's an example of this type system in action:
# let x = object method hello = Printf.printf "Hello, world!\n"; end;;
val x : < hello : unit > = <obj>
# let y = object method hello = Printf.printf "Hello, universe!\n"; end;;
val y : < hello : unit > = <obj>
# [x; y];;
- : < hello : unit > list = [<obj>; <obj>]
# let f z = z#hello;;
val f : < hello : 'a; .. > -> 'a = <fun>
# List.map f [x; y];;
Hello, world!
Hello, universe!
- : unit list = [(); ()]
x and y belong to completely different (and anonymous to make transcript simpler) classes, but duck typing together with type inference lets us put them in common container and List.map them, without losing any static safety.
I might be wrong, but it seems to me that if you want to have static safety by default, duck typing, and no excessive annotation (=> either static type inference or dynamic typing) together, you will end up with typing system rather similar to OCaml object system. And you seem to want all three properties from the type system, unless I misunderstood the metaphor :-)
Okay, I've got to admit, I barely have an idea what obj.magic does, it seems like docs on it are "sparse".
From what I can tell it's not even runtime safe. So yes it's an escape valve, but it's a bit too much of one. I wish I knew exactly what it's doing nonetheless, but I can't find any sufficient description.
Your example is easy to understand, but it makes me think you still don't understand my intent. It's not about duck typing statically.
What I'm thinking of is a way to write most of your code statically, but still allow you to subvert the system to do things that would be so much easier in a dynamic language.
Reducing type annotations and raising performance are nice goals, but they are so peripheral when compared to the bigger picture.
The big picture is about writing highly functional software fast, and having it work too.
Dynamic languages seem to help with the first part. Starting from a blank slate you write quicker if you don't write type names, or worry about type system annoyances.
But dynamic languages are missing a lot of tool capabilities. The most obvious is the static analysis performed by compilers and other tools that is important to the second step.
Sure you can write unit tests, but you might just end up writing your own custom static analysis tools inside your app/tests, which seems to me a waste of time.
Lastly, lack of typing makes your code harder to read because sometimes you just have to run the code to figure out what it does.
I'd like to see is the ability to write that type of code when you need it. But since it's rarely necessary it would be awfully nice to have a big flashing warning sign by it so I can read and refactor other code without those worries. Continuous vigilance usually turns into complacency, so I don't want to be required to be vigilant when there is no danger.
Post a Comment