[plt-scheme] type of language

Hi,

On Wed, 9 Dec 2009 16:09:15 -0800
John Clements <clements at brinckerhoff.org> wrote:

> > Weak/Strong typing: If a language is weakly typed, it tries to
> > convert the types automatically and guess what you want to do. For
> > example, consider "1" + 1. If a language is weakly typed, the
> > answer is usually 2 (or "11"), because it guessed what you wanted
> > to do. If it is strongly typed, you get an error/exception that
> > this is not valid, one cannot add a string and an integer together.
> > 
> > Popular example of weak typing: PHP
> > Popular example of strong typing: Scheme :)
> 
> Ack! I totally reject this definition of "weak" vs. "strong" typing.
> Generally, the difference you're describing has nothing to do with
> the language's type system per se, but rather with the definition of
> its primitives, and how flexible or restrictive they are.

Ok, what would be a better definition?

> > Dynamic/Static typing: is the type information enforced? Can a
> > "variable" change its type? Is it possible to call a function with
> > types that weren't considered by the implemnentor of the function?
> > Do you need to declare the types of function arguments and return
> > values?
> > 
> > Popular example of dynamic typing: Scheme :)
> > Popular example of static typing: Java
> > Popular example of static typing with type inference: ML
> > (type inference = you don't need to specify the types, the language
> > finds out about them by itself)
> 
> Ack! I totally disagree with this as well.
> 
> A statically-typed language is one with a built-in proof system that
> demonstrates the impossibility of certain runtime errors.  These
> languages refuse to run any programs for which their proof system
> cannot construct such a proof.
> 
> The choice of *which* errors are fenced out by the proof system is up
> to the designer of the type system, which makes clear distinctions
> between statically-typed languages and non-statically-typed languages
> impossible.

I don't see how a clear distinction between these two would not be
possible. Care to provide an example?

regards,
Marek