Untyped Scheme should be built on Typed Scheme? WAS: Re: [plt-scheme] macro question

From: hendrik at topoi.pooq.com (hendrik at topoi.pooq.com)
Date: Mon Dec 22 15:03:01 EST 2008

On Sun, Dec 21, 2008 at 08:39:10PM -0500, Shriram Krishnamurthi wrote:
> Every language grows and changes over time.  What if you found out
> after a while that your type system inhibited the growth of your
> language?

Then you would have chosen the wrong type system, and you'd better fix 
it.

>  So better to build atop the "untyped" language.

There is no such thing as untyped data.  What there is is data whose 
nature is not made clear in the program text.  Data are typed by the 
intention of the programmer, the programmer who defined a variable 
intends certain kind of data to reside in that variable -- those data 
that are compatiple with his intention while he writes the program, and 
no others.

To the extent that an explicit type system can express those intentions, 
it supports the programmer in his efforts to write correct code;  to the 
extent that it does not, it gets in his way.  I really believe we know 
enough about type systems not that it is possible to edvise hslpful 
ones.  In the few cases where a decent type system cannot express the 
programmers' intentions, there will have to be some kind of escape from 
it, such as a type 'reference to anything', or 'reference to anything 
with an encoding that can tell us what kind of thing it is at run time.'  
But the overwhelming majority of code will involve variables about which 
much more is statically known.

  Static type checking is the most powerful easily implemented formal 
verificatin tool we have in out eternal battle against bugs.  It doesn't 
handle everything, but whe should use it for all it's worth.

-- hendrik


Posted on the users mailing list.