[plt-scheme] Re: plt-scheme type of language

From: Carl Eastlund (carl.eastlund at gmail.com)
Date: Fri Dec 11 15:29:22 EST 2009

On Fri, Dec 11, 2009 at 3:07 PM,  <hendrik at topoi.pooq.com> wrote:
> On Fri, Dec 11, 2009 at 11:28:20AM -0800, YC wrote:
>> Perhaps a site with a few pages summarizing what type systems are, what they
>> do, what attributes describe them, and why strong typing makes no sense, and
>> then link back to PLAI for more in-depth information?  Of course, this is
>> just an idea.
> Just as a matter of interest, why does strong typing make no sense?
> -- hendrik

A typed language has a type checker (some way of checking a property
of programs) and a soundness proof (a guarantee that programs with
this property are "good" in some sense).

A "strong" type system does not give any more than the above, and a
"weak" type system no less.  At best, these words are vague
descriptions of the sort of property that is checked.  However, a
"strong" type system does not necessarily correspond to a stronger
property being checked (i.e. rejecting strictly more programs), and it
certainly does not mean a stronger guarantee from the soundness proof.

>From this perspective, it is hard to see what the difference between
"strong" or "weak" type systems is.  They're both just different kinds
of type systems.


Posted on the users mailing list.