On Sat, Jun 4, 2011 at 10:52 AM, Scott McLoughlin <[email protected]>wrote:
> 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. > Let me quote from the Gilad Bracha position paper I cited before: The disadvantages of mandatory typing are not as universally acknowledged. > Types constrain the expressiveness of the language. While all major > programming languages are Turing-complete, and so may be considered “equally > expressive”, the fact is that a mandatory type system greatly reduces the > number of > legal programs that can be expressed in a language. That seems to be the core reason for the use of dynamically-typed languages in small systems. 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??? Yes. The most extreme example is Bluespec ( http://en.wikipedia.org/wiki/Bluespec,_Inc.) which is a strongly-typed Haskell variant which compiles directly to logic gates. (I find the Bluespec website is pretty uninformative; you might find better information at http://citeseerx.ist.psu.edu/search?q=bluespec and in the bluespec section of http://research.microsoft.com/en-us/um/people/simonpj/papers/history-of-haskell/history.pdf). Bluespec has an extremely powerful type-checker, which can verify arithmetic properties of the generated hardware, for example: bundle :: Bit[n] -> Bit[m] -> Bit[n+m] The basic issue here -- with Bluespec and other such efforts -- is that the types are unnecessary at run time. They are only used to verify correctness. So there's no strong reason to build a "machine" which runs the typed language. It's more accurate to say that a typed language is *compiled to* the machine. Also related are the G-machine, ABC-machine, etc ( http://lambda-the-ultimate.org/node/3030 ) which are usually described as abstract machines, but could be compiled to hardware. The source for these is usually a strongly-typed functional program -- but although the types may guide compilation, they disappear by runtime. --scott -- ( http://cscott.net )
_______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
