🚀 go-pugleaf

In article <49229@nigel.ee.udel.edu>, carroll@cis.udel.edu (Mark Carroll) writes:
|> 
|> Any typing error that would be trapped in a staticly typed language
|> can be captured in a dynamically typed languages using dataflow
|> analysis. If the error can't be caught with dataflow, then either
|> the program would be written differently in the static language (in
|> which case, the same safe version could be written with the dynamic
|> typed language), or the staticly typed language would have a kludged
|> dynamic typer, in which case the static language would be as subject
|> to error as the dynamic.
|> 
Any proof of this claim?  I don't believe it.

This claim seems to be the same as saying that dataflow analysis can always
determine the types of variables and expressions.  This is not true.
Given a powerful enough type system, type inference is undecideable.

In general, it is easier to decide whether a program is legally typed
than to discover a legal typing for it.  Determining whether a program
will have a typing error often requires finding program invariants.
Dynamic typing means that programmers don't have to write down these
invariants, which is why languages with dynamic typing are easier to
program in, at least for medium-scale programming.

For the record, I am a Smalltalk fan, and have been working at developing
a type system and a type inference system for it.  Type inference is
basically the same as dataflow anlysis.  Type inference is MUCH harder
than type checking.  It has lots of advantages, to be sure.  However,
I don't believe that "any typing error" that would be detected by a
type checker could be detected by a type inference system, i.e. by 
dataflow analysis.

Ralph Johnson -- University of Illinois at Urbana-Champaign