First, you have introduced to me to a line of inquiry I had not
fully considered before, the notion of deriving more complex
type systems from simpler typing primitives. Hmmm....
Second, I think you have over estimated the nature of my initial inqiry.
I was just noting that the "transparent, modifiable, boot strapped"
systems seemed to historically be the province of untyped (Forth) or
latently typed (Smalltalk, Lisp) languages.
I was simply asking whether and how statically typed languages
would fit into the mix. One minor example I might propose is the
bare-metal Oberon system, but I have no first hand experience
with it.
So I'll rephrase my question in this manner. We can imagine a
Smalltalk or Lisp or Forth machine. Can we imagine a machine
predicated on a statically typed language - a Haskell machine, or
OCaml Machine or whatever - in the same way???
Why or why not?
- S.
On 6/4/2011 12:56 AM, C. Scott Ananian wrote:
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
_______________________________________________
fonc mailing list
fonc@vpri.org
http://vpri.org/mailman/listinfo/fonc
