I agree with Jay McCarthy that static typing is anti-human. I think I can give a slightly more elaborate example of a program that every static type checker must reject, but that is nevertheless correct. Everything below is valid Common Lisp:
(defclass person ()
((name :initarg :name
:accessor person-name)))
(defmethod display ((p person))
(format t "Person: Name ~S, address ~S."
(person-name p)
(person-address p)))
A static type checker must reject this program because there is no address field defined in the class person that person-address presumably refers to. However, below is a run of the program in a Lisp listener that runs to a correct completion without fatal (!) errors:
CL-USER 1 > (defvar *p* (make-instance 'person :name "Pascal")) *P*
CL-USER 2 > (display *p*)
Error: Undefined function PERSON-ADDRESS called with arguments
(#<PERSON 4020059AB3>).
1 (continue) Try invoking PERSON-ADDRESS again.
2 Return some values from the call to PERSON-ADDRESS.
3 Try invoking something other than PERSON-ADDRESS with the
same arguments.
4 Set the symbol-function of PERSON-ADDRESS to another
function.
5 (abort) Return to level 0.
6 Return to top loop level 0.
Type :b for backtrace or :c <option number> to proceed. Type :bug-form "<subject>" for a bug report template or :? for other options.
CL-USER 3 : 1 > (defclass person ()
((name :initarg :name
:accessor person-name)
(address :initarg :address
:accessor person-address)))
#<STANDARD-CLASS PERSON 4130371F6B>
CL-USER 4 : 1 > :c 1
Error: The slot ADDRESS is unbound in the object #<PERSON 41303DD973> (an instance of class #<STANDARD-CLASS PERSON 4130371F6B>). 1 (continue) Try reading slot ADDRESS again. 2 Specify a value to use this time for slot ADDRESS. 3 Specify a value to set slot ADDRESS to. 4 (abort) Return to level 0. 5 Return to top loop level 0.
Type :b for backtrace or :c <option number> to proceed. Type :bug-form "<subject>" for a bug report template or :? for other options.
CL-USER 5 : 1 > :c 3
Enter a form to be evaluated: "Belgium" Person: Name "Pascal", address "Belgium". NIL
CL-USER 6 > (display *p*) Person: Name "Pascal", address "Belgium". NIL
The "trick" is that the Lisp listener allows for interactive modification of a program while it is running. No static type checker can anticipate what modifications will be performed at runtime.
This is not a toy feature of Common Lisp, but something that many Lisp developers rely on. For example, my own ContextL library crucially relies on the very class redefinition feature I demonstrate above. Joe Marshall provides another account how such features can solve real-world problems.
13 comments:
"A static type checker must reject this program because there is no address field defined in the class person that person-address presumably refers to."
Sure, but it should be trivial to define one, in Haskell for example:
person-address = undefined
The program will build, and blow up at runtime, like yours. And if you're running it in a repl(like GHCi), you can then actually write the function.
The point of this example is that you don't have to provide a definition for person-address at all to run this program, not even an "undefined" one. I know it's hard to imagine that this could be crucial given just such a small example, but trust me, it is. ;)
Is not this just an example of differences in how Lisp REPL is used compared to e.g. Haskell. I understand in Common Lisp "runtime programming" seems almost idiomatic. Haskell is more conservative following "WCL" (write-compile loop).
Now imagine this happens in production. The static typed version is more likely to catch this type of errors where Lisp version works fine just until untested path is reached and results in a runtime error and a call to support.
Is there a way in CL to check all the paths are fine but to run them (which is in most cases at least not feasible?) I am not aware of one.
On the other hand in Haskell one can use error (or todo wrapper below) anywhere so it is easy to grep and implement later for such paths. I am not aware if there is a way to replace such implementation at runtime.
todo :: String -> a
todo s = error ("Not implemented. "++s)
+1 for Static typing.
Pipo,
No, this is not just a REPL example, this is part of the semantics of the Common Lisp object system which you can rely on in any program.
This feature, and similar others, are actually taken advantage of in production systems. The Common Lisp condition / exception system is designed in such a way that you can both interactively and programmatically change and re-execute relevant parts of your program.
Good Common Lisp compilers give warnings for undefined functions, type mismatches, and similar issues. Unlike most statically typed languages, however, they don't keep you from running a program even in the presence of such warnings. This is a crucial advantage.
There is no point in having to manually insert stubs in your program just to make it compile and run. Please also check out Joe Marshall's blog post for a more comprehensive example that illustrates this.
-1 for you. ;)
"Good Common Lisp compilers give warnings for undefined functions, type mismatches, and similar issues."
GHC 7.6 can defer type errors until runtime too: http://www.haskell.org/ghc/docs/latest/html/users_guide/defer-type-errors.html :).
It's nice to see that GHC provides such a feature. However, I suspect that this is considered merely an aid during software development, not a feature for deployed software. What I show in my blog post is that you can react to the exception / condition you get when calling an undefined function, or accessing an undefined field, provide the definition after the fact, and then continue the execution without restarting the whole program. You can make this work without requiring user interaction. This is part of the Common LIsp language specification, not an extension of a particular compiler. As I already stated in my blog post, for example my own ContextL library relies on this feature in its implementation, which is portable across eight different Common Lisp implementations.
With GHC, can you react to such type errors at runtime, change the involved definitions, and then continue running? Is this a feature you can rely to consistently work in well-specified ways?
Daniel Herring sent me the following comment and gave me permission to reproduce it here:
"There are many reasons to patch running code. Live upgrades and security patches are two examples. Interactive debugging is another use case, especially when bugs are hard to trigger or understand, algorithms are ill-defined, etc. By their post-facto nature, these examples preclude full knowledge when the code is first compiled.
CLOS provides excellent support for the object changes that are often required. Factor tracks filesystem changes to simplify world updates, and it (at least used to) also tracks and re-applies changes to inlined functions.
While language support for dynamic changes (including typing) is helpful, it is not strictly required. Language runtimes usually provide powerful debug hooks. Coupled with an intimate knowledge of the runtime, these make hot patching possible. For example, patches may be applied by atomically inserting jumps to new code. Large structural changes may require inserting breakpoints to guard the change.
In fact, Ksplice has made a business of patching live Linux kernels."
This sort of wide-open system would be easier to exploit by the black-hats. And it could be harder to test.
I don't have any real experience with such dynamical systems, though I've coded lisp and Ruby. And I have great respect for the ability of people to adapt and manage in the face of the unexpected. But it sounds like a formula for unreliability to me.
Think about a computerized space shot, surgery, Mars robot, traffic controller, driverless car, smart bomb, or your bank account.
Some kinds of systems are by definition flexible in the face of dropped data and failures: Craigslist, Google search, restaurant selection. Others are more demanding.
Big Rick,
The issues you are concerned with are orthogonal to the issues being discussed here. If somebody can gain unauthorized access to a system, they can affect reliability in negative ways, no matter whether the system is dynamically or statically typed, or whether it allows for runtime changes or not. You need good security and protection in any case.
However, dynamically adaptable systems can help with reliability. For example, it was possible to fix the flash memory management anomaly that occurred with the Mars rover Spirit while the system was deployed because it provided ways to dynamically adapt it, not in spite of this. Since it is hard to anticipate what potential problems might occur, it's better to provide as many adaptation opportunities as possible, to ensure (eventual) reliability.
This is good to hear. But I'm still concerned that the language processor would not warn the programmer about referencing undefined fields before the software goes into production.
I don't use common lisp so I don't know if would provide that warning, at "compile time".
It is good engineering practice in general to eliminate sources of variability as much as possible; So that the bits that run in production are the bits that you tested before hand.
In the case of the Mars software this was true, they ran it on a ground "satellite" first.
But think of Microsoft's problem with "DLL Hell". The bits the customer was running were different than the bits that were tested. The production software was too "dynamic".
Big Rick,
You have now stated two times that you don't have real experience with the kinds of systems under discussion. Maybe it's worthwhile to change that, if you are interested and find the time to do so.
Keep in mind that the example I have given in my blog post is just for illustration. Just like programs that print "Hello, World!", or compute Fibonacci numbers recursively, are examples that nobody actually really wants to run, this example also just shows off a feature of a programming language that can be a building block for more relevant applications, but not necessarily exactly in the way I have shown. I actually already hinted at that in my blog post.
Consider this a starting point for people who are interested to dive deeper and get a more complete view of what is possible, and what the real advantages and disadvantages are. If this doesn't work for you, then I apologize. If this doesn't work for anybody, then I guess I failed, but I'm optimistic that this isn't the case.
I understand that an example in a blog needs to be short, but this simply does not convince me. It’s very artificial. It is true that a static type checker would complain here and even if we execute it anyway then at runtime there would be no mechanism to change the system so that it can continue to run.
A small example in Haskell:
add a b = a + b
add10 = add 10
GHC could reject this program but we know it’s obviously correct. The reason is that it infers a too specific type for `add10` from Integer to Integer while `add` at the same time more generic is and for all numbers works.
We would first need to tell GHC to not use the monomorphism restriction to make this work. This, in my opinion, demonstrates more nicely how a static type checker can reject obviously correct programs.
Now this example is trivial to fix but the one that you gave as an example is different. Before you even run the progam you will know that you are calling a function that does not exist. So you can decide to either add it and make it work with persons or remove it.
At least in our Lisp environments we really never extend classes at runtime. We did add data patterns at runtime and functions that work with this data. This is a useful thing and if we had used Haskell we would either have to use an interpreter (which may be fast enough) or restart the application.
This usecase is easier to solve in dynamically typed languages. To some extent this can be done in Haskell too. For example at Facebook they are using a known API and load a dynamically linked library into the software while it is running. They can this way hotswap it. For many cases this can turn out to be good or as I mentioned above an interpreter might be efficient enough.
But in reality this has to do with the task at hand. Only a certain amount of software _really_ benefits from being updatable at runtime. In most cases I reckon it’s perfectly good to just restart the software. Also the example that Joe Marshall provided does not impress me too much.
In my environment it’s given that we run tens or hundreds of images on Amazon. We can’t log in to the live systems and update them. Ops prefer dockerized images to which developers even have no access. If a bug is being identified in monitoring you updated the docker image and update it without downtime (hopefully).
While it is true that static type systems reject also correct programs this is more of a theoretical argument. In practice what we really have to do is to often write a small amount of boilerplate code to make it work. And some systems (for example GHC) are getting better and better and reduce the amount of code that we need to write. But the protection from type errors is a very good help.
I only need to remember the past 12 months. We had a few problems with very evil bugs that were extremly hard to find. And in nearly all cases a type error was the root cause. Something that could not have happened in Haskell. I admit that the latest error was a logical one. It took us over a year to discover that an (and ...) was too permissive and was missing another clause. But I kid you not when I say that the great majority of difficult problems were type errors.
And here I mean runtime exceptions that reduce the user experience or simply crash the program.
Jeff Haskell,
Your example is not a good one for illustrating the point of this discussion. As you state yourself, a language is conceivable that would accept your example as correct. However, the discussion is about examples where no statically type-checked language could ever be designed that would consider them correct. My example not only cannot be accepted by a static type checker, it also illustrates a feature of a language that is actually in use in some applications.
Pascal
Post a Comment