[plt-scheme] type of language

From: Shriram Krishnamurthi (sk at cs.brown.edu)
Date: Wed Dec 9 19:33:58 EST 2009

There is NO consistent definition for "weak" and "strong" typing.  It
sometimes means "languages I dislike" vs "languages I like", and
sometimes vice versa.


On Wed, Dec 9, 2009 at 7:25 PM, John Clements <clements at brinckerhoff.org> wrote:
> On Dec 9, 2009, at 4:17 PM, hendrik at topoi.pooq.com wrote:
>>> 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.
>> A statically typed language is one in which the types of expressions
>> and variables and such can be determined without running the program.
>> It only manages to be a proof in the sense you describe if the type
>> system is strong as well.
> I wouldn't call such a language statically typed.
> I would agree with you, though, that (in addition to my earlier definition) a type system must associate "types" (whatever those are) with "terms" (whatever those are).
> Ultimately, of course, definitions such as this are decided in the court of popular opinion.  My arguments in this court are observed not to have much effect.
> John
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme

Posted on the users mailing list.