This issues were in conversations in the mid-60s when I was in grad school.
One difference was that there was a computer (and more being thought of) -- the
Burroughs B5000 -- that removed one of the motivations for static typing -- it
implemented byte codes and 0 overhead dynamic type checking into the hardware
which was organized as what would have been called the first capability
architecture -- it was not crashable by a non-privileged programmer).
The semi-bug was that it was aimed at Algol/Simula like languages, so some
other
ideas were less efficient. This was resolved at PARC by dynamic microcoding of
the VM (both on the mainframes and on the personal computers we designed and
built). The game here was that if the micro-CPU was always waiting for memory
to
serve it (it was about 5 times faster) then you won (dynamic type checking was
not slowing anything down).
This left the other question and possible motivation for static type checking,
which was: could the tradeoffs it imposed still wind up helping the programmers
more than bogging them down?
The extreme case of this -- where the variables are actually constrained to the
specific values they are supposed to contain -- would be very useful if it
could
be made to generally work -- it amounts to declarative programming.
Another extreme case would concern procedures/methods (we've called it
"semantic
typing"). For example, we want to find an operator that will do something
specific -- like the sine function -- and we type our local name for this so
that the only value it can have is a procedure that will compute sine. We could
think of this as a kind of unit test for resources, or we could think of this
as
search criteria. Ted Kaehler implemented the Squeak method finder to do some of
this. You give it examples of relations and it finds the methods. So 3 . 4 . 7
will yield both "+" and "xor". 30 . 0.5 will find "degreeSine", etc.
Examples are not enough for semantic typing, but we can see that with an
Internet of possible resources, it would be useful to be able to characterize
transformations in this way.
Back to normal approaches to typing. This leaves us partly with what kinds of
bugs do you prefer and when do you want them to materialize?" kind of
questions.
It's always seemed to me that what we really need to be working on is something
more like "real specifications that execute to produce prototypes (and can be
debugged) much more than weak schemes that are complex enough to introduce
severe cognitive load, but aren't comprehensive enough to come close to paying
their way.
Cheers,
Alan
________________________________
From: C. Scott Ananian <csc...@laptop.org>
To: Fundamentals of New Computing <fonc@vpri.org>
Sent: Fri, June 3, 2011 9:56:21 PM
Subject: Re: [fonc] Static typing and/vs. boot strap-able, small kernel,
comprehensible, user modifiable systems
On Fri, Jun 3, 2011 at 11:37 PM, Scott McLoughlin <scottmc...@gmail.com> wrote:
> What is the relationship, positive and negative, between static
> typing in language design and user-transparent and modifiable
> systems bootstrapped from small kernels?
"Small type systems" aren't very powerful, and tend to grate on their
users. So people dream of more powerful type systems, to let them
write more flexible code. Soon you're in Hindley-Milner territory or
fighting the halting theorem and your system isn't so small and
understandable any more.
The solution seems to be a "pluggable types" system, which lets you
build a complicated and/or domain-specific static type system (or
several of them) from a small kernel (or a purely dynamic system).
AFAIK, this hasn't gotten a lot of attention from the research
community, partly because no one seems quite certain how to go about
building such a thing. Gilad Bracha seems to have done the most
thinking about it; see his position paper linked from:
http://bracha.org/Site/Newspeak.html
The bibliography of his position paper cites a number of other related papers.
I spend some time around 2007 trying to figure out how to write Java
1.5's type system in terms of a smaller kernel type system. I didn't
get very far. (I made much more progress on the syntactic evolution
of Java 1.5 from Java 1.0.) There are links between type systems and
abstract interpretation (see http://lambda-the-ultimate.org/node/2208
); that may hold the key.
Perhaps some others of the list can fill in more details.
--scott
--
( http://cscott.net )
_______________________________________________
fonc mailing list
fonc@vpri.org
http://vpri.org/mailman/listinfo/fonc
_______________________________________________
fonc mailing list
fonc@vpri.org
http://vpri.org/mailman/listinfo/fonc
