Matthias said:
This is simply not true. See above.
OK, let's try to distill this to some simple questions.
Assume you have a compiler ML->CL that translates an arbitrary ML
program with a main function into Common Lisp. The main function is a
distinguished function that starts the program (similar to main in C).
The result is a Common Lisp program that behaves exactly like its ML
counterpart, including the fact that it doesn't throw any type errors at
runtime.
Assume furthermore that ML->CL retains the explicit type annotations in
the result of the translation in the form of comments, so that another
compiler CL->ML can fully reconstruct the original ML program without
manual help.
Now we can modify the result of ML->CL for any ML program as follows. We
add a new function that is defined as follows:
(defun new-main ()
(loop (print (eval (read)))))
(We assume that NEW-MAIN is a name that isn't defined in the rest of the
original program. Otherwise, it's easy to automatically generate a
different unique name.)
Note that we haven't written an interpreter/compiler by ourselves here,
we just use what the language offers by default.
Furthermore, we add the following to the program: We write a function
RUN (again a unique name) that spawns two threads. The first thread
starts the original main function, the second thread opens a console
window and starts NEW-MAIN.
Now, RUN is a function that executes the original ML program (as
translated by ML->CL, with the same semantics, including the fact that
it doesn't throw any runtime type errors in its form as generated by
ML->CL), but furthermore executes a read-eval-print-loop that allows
modification of the internals of that original program in arbitrary
ways. For example, the console allows you to use DEFUN to redefine an
arbitrary function of the original program that runs in the first
thread, so that the original definition is not visible anymore and all
calls to the original definiton within the first thread use the new
definition after the redefinition is completed. [1]
Now here come the questions.
Is it possible to modify CL->ML in a way that any program originally
written in ML, translated with ML->CL, and then modified as sketched
above (including NEW-MAIN and RUN) can be translated back to ML? For the
sake of simplicity we can assume an implementation of ML that already
offers multithreading. Again, for the sake of simplicity, it's
acceptable that the result of CL->ML accepts ML as an input language for
the read-eval-print-loop in RUN instead of Common Lisp. The important
thing here is that redefinitions issued in the second thread should
affect the internals of the program running in the first thread, as
described above.
To ask the question in more detail:
a) Is it possible to write CL->ML in a way that the result is both still
statically type checkable and not considerably larger than the original
program that was given to ML->CL. Especially, is it possible to do this
without implementing a new interpreter/compiler on top of ML and then
letting the program run in that language, but keep the program
executable in ML itself?
(So, ideally, it should be roughly only as many lines longer as the
modified CL version is compared to the unmodified CL version.)
b) Otherwise, is there a way to extend ML's type system in a way that it
is still statically checkable and can still handle such programs?
c) If you respond with yes to either a or b, what does your sketch of an
informal proof in your head look like that convincingly shows that this
can actually work?
d) If you respond with no to both a or b, would you still disagree with
the assessment there is a class of programs that can be implemented with
dynamically typed languages but without statically typed ones? If so, why?
[11 Except perhaps for a class of programs that would change their
runtime and/or space complexity, provided they would need lots of
dynamic type checks.
This comment makes me /very/ uneasy. Namely, the funny thing here
is that you seem to question a statement that you make /yourself/ even
though it is undoubtedly true. *Of course* you can write everything
that can be written in a statically typed language in a dynamically
typed language in such a way that runtime behavior is the same
(including complexity). Translating a well-typed ML program into,
say, Lisp is completely straightforward. (Early ML implementations
were done that way.)
Well, nothing in this thread makes me uneasy at all. I am not trying to
defend dynamic typing out of pure personal preference. I want to find
out if we can objectively classify the programs that are expressible in
either statically typed languages or dynamically typed languages. Until
recently, I have thought that the class of programs you can write with a
dynamically typed language is a strict superset of the programs you can
write with a statically typed language. It is especially the class of
programs that allows full-fledged runtime metaprogramming, as sketched
above, that statically typed languages cannot implement by definition
without resorting to implement a full interpreter/compiler for a
dynamically typed language.
If it turns out that statically typed languages can indeed express a
class of programs that exhibit a certain behavior that you cannot write
in a dynamically typed language without implementing a full
interpreter/compiler for a statically typed language on top, this
wouldn't make me feel "uneasy". To the contrary, I would be happy
because I would finally understand what all the fuss about static typing
is about.
If it is your only concern that you defend your pet programming style,
well, that's not my problem. I am interested in insights.
PS: You don't need to try and convince me of the virtues of dynamic
typing. I *come* from this world -- having implemented at least three
(if not four -- depending on how you count) interpreters/compilers for
dynamically typed languages. Because of this I also already know all
the arguments that you are undoubtedly thinking of bringing forward,
having either used them myself or once marveled at them when I heard
them from other, then like-minded folks. But the long-term effect of
working with and on such systems was that I now prefer to avoid them.
"Run-time metaprogrammming" you say? The emperor has no clothes.
I don't care whether you have made bad experiences in this regard or
not, to more or less the same degree that you probably don't care
whether I have made bad experiences with static type systems. (And
that's fine.)
I am only asking questions that we can objectively answer. Can static
typing and runtime metaprogramming be reconciled, yes or no?
Pascal
[1] Yes, with all the dangers that this may incur! There are ways to
handle the potential dangers of such an approach. That's what dynamic
metaobject protocols are designed for. However, this doesn't matter for
the sake of this discussion.
And it's much worse