• These ideas came from a FONC thread.

Static Disadvantages

• 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. -- Gilad Bracha

That seems to be the core reason for the use of dynamically-typed languages in small systems.

Generating Machines

> 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 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 in this paper and in the bluespec section of this paper).

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., 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.