Re: the forward method [dynamic vs. static typing]

[Joe Marshall <address@hidden>]

John Clements <clements@brinckerhoff.org> writes:

> Typically, type systems help you to construct a proof that certain
> errors cannot arise during evaluation.  When parts of that proof are
> used to alter the evaluation itself, you suddenly have a class of
> _runtime_ errors (or rather, "mis-behaviors") that can only be
> understood by examining the type proof.

I think that John has identified what it is that made me uncomfortable
with this style.  I generally think of the type system as meta
information.  Intertwining the control flow with the meta information
about the value flow not only makes it hard for humans to reason about
the program, it makes it hard for programs to reason about it as well.

It also seems to me that it can make programs more fragile.  To take
the example of `dvi2ps', suppose one has code that uses type inference
to deduce that to print your LaTeX file it must first run TeX, then
dvi2ps, then send the result to the postscript printer (it deduces
this by seeing that the output type of TeX is a dvi file and that the
input type to the printer is a ps file).  Now suppose that someone
`enhances' dvi2ps such that it can generate a PDF file, too.  You no
longer have the guarantee that the output of dvi2ps is a ps file.  One
can envision several ways to recover from this, but I don't see a
general solution.