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

On Fri, Dec 11, 2009 at 03:29:22PM -0500, Carl Eastlund wrote:
> 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

I see.  You're using a completely different sense of the words "strong" 
and "weak" than I do.  I've been using the words in my sense since the 
seventies (and possibly the late sixties).  In the 60's data types meant 
you would declare your variables, specifying what types they were to have 
(or leave to language to choose a default), and this informed the 
compiler which forms of machine instructions you intended to use.  This 
was a great advance on, say, assemply language, when you had to specify 
this explicitly with each instruction.  It greatly reduced the 
opportunity for making errors.  Even PL/1, which provided 
pointers and a non-garbage-collected heap, did not pick up on the 
possibility that when you define a variable to be of pointer type, it 
might make sense to specify what kind of thing it pointed to.  
Presumably assembler programmers knew that it was useful to have a 
pointer sometimes point to one kind of thing and sometimes another.
I think the name "type system" is still appropriate for languages like 
this, and, regrettably, they are still in heavy use.

It wsa with Algol 68 that I encountered what I learned to call a strong 
type system, to contrast with a weak type system.  A strong type system 
actually had the rigidity to implicitly prove that values would at run 
time, always be of the types they were declared with.  It baffles me 
that languages without this property have remained in the mainstream as 
long as they have.
  Oh, I don't mean that it isn't necessary sometimes to escape from the 
panguage to express machine-specific things that language designers 
didn't choose to implement in the language.  But it whould not be 
possible to escape by accident.
  Languages like C++ can certainly be considered to have type systems.  
Bad type systems, if you like.  Type systems not strong enough to hold a 
program up under stress, perhaps.  But if we're not going to be able to 
use the word "weak" for this, we'll have to find another word.  the 
systems are still with us, and we need terminology that works.  And as 
far as I know, the terminology that I use has a long history.

  As you use them, the words "weak" and "strong" don't seem to have much 
significance.  Perhaps that arose in an isolated community that never 
saw weak typing (as I use the word) and never had to talk about it.

-- hendrik