RE: bytecode unification for scripting (and other!) languages

["Shriram Krishnamurthi" <sk@cs.brown.edu>]

> 2. Having said that, I believe that programmers should actually think
about
>    their types, in all situations. As Michael also points out, if you
>    understand the types of your program well, you avoid many mistakes.
Many
>    errors manifest themselves in violations of data invariants, and that's
>    what these simple proof systems called type systems are good at.

I disagree with the implication of this.  The implication is that, when a
programmer reasons incorrectly about their types, they should get slapped
on the hand -- whether as a static rejection, a la ML, or as a dynamic check
failure, a la Scheme, is irrelevant.

I believe there is a very useful way of relaxing this restriction to capture
the essence of scripting, while still recovering it when programs grow to
engineer software.  PLT Scheme needs a "scripting" language level, where
operators coerce heavily: APPEND consumes strings as well as lists; FIRST
works on vectors, not just pairs; and so on.
MrSpidey then needs a scripting analysis level, where it flags these coerced
uses in ultra-special-red, meaning "this may have worked for you earlier,
but
it sure won't work now".  Based on the coercions

> 3. Still, when I write one-line scripts, I don't want to write down types,
>    because the typing of my program is so obvious that it just slows me
>    down. Then again, some scripts contain some really hairy
> pieces of code,
>    and perhaps I should write down types right there so that *I* the
>    scripter can figure out what I mean.
>
> 4. Because many scripts evolve into "real" programs, that means scripting
>    languages need a (partial) type reconstructing environments.
>
> 5. The problem with ML's version of this idea is that it is too rigid. It
>    is about a system of disjoint types (claims about value flow)
> and in our
>    daily experience of script programming, we need more. We also need more
>    because we tend to extend the data sets of programs over time, and ML
>    won't let us do this without major editing.
>
> 6. This reasoning led Cartwright, Fagan and myself to a discussion of soft
>    typing -- in 1988. Over the following 13 years, Cartwright and I
>    supervised three dissertations on this topic. I believe in working
>    systems and we produced two distinct soft typers with different
>    interfaces and different underlying mechanisms. If you don't know, take
>    a look at PLT's publication site
>
>      http://www.cs.rice.edu/CS/PLT/Publications/
>
>    Look for our PDLI 96 paper (lead author: Cormac Flanagan). Even
>    flame-throwing theory eaters will be able to read this introductory
>    paper. There is more there, and I am willing to report on my
>    experiences, if there is interest, because I am by far the
> most diligent
>    user of all these soft typing systems over the past 13 years.
>
> PLT is returning to this topic. Stay tuned. -- Matthias
>
>
>