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

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.

--Carl