Lambda the Ultimate

The idea of a router in Croquet seems very odd, and yet by design, it is at the center of all synchronizations, psuedo-time, whatever you name it.

I just can't imagine such a system that emphasizes so much on scalability and fault tolerance eventually boils down to a single bottleneck of all. Correct me if I'm wrong.

I'm repeatedly surprised how much headway Smalltalk makes -- in spite of its lack of support for static safety and formal methods.

There's a lot to be said for a heavily interactive, always live, environment which promotes experimentation. I'd love to see new languages go down that road.

I'm currently working on a paper on how live editing and dynamic inheritance are supported in SuperGlue. Smalltalk/Self/Morphic/EToys/etc... are very influential. It is disappointing that our mainstream languages are stuck in the 60s on this topic.

Incremental interactive development, rather than dynamic typing per se, have been Lisp and Smalltalk's real contributions to programming, IMHO, and the great myth is that you can't have that style of development with static typing. But as I've written before, this isn't true: O'Caml and EMACS + Tuareg Mode give you an excellent incremental, interactive development experience, complete with time-travel debugger, at least for bytecode. But you don't have to commit to native code until you're done. To make matters even better, at a certain point in development, it makes sense to start using omake -P to do a continuous build of your code as you're editing/saving it. Type, try, save; type, try, save... this is what's most great about Lisp, Smalltalk, Python, Ruby, O'Caml, Scala... IMHO.

You can have a reasonable facsimile of the Smalltalk/Lisp style of development in more static languages, but it's not quite the same thing.

With the continuous build approach, the difference is whether, or to what extent, the program has to be restarted in order to use new code. Restarting means you lose state, and may have to redo things to get back to the point the program was at when you changed the code.

In many cases, this may not be a big deal, and the two approaches may appear equivalent. But there are situations in which the Smalltalk/Lisp style has advantages that are difficult to duplicate with more static languages (including some Schemes, btw). Smalltalk development environments are an example: you wouldn't want to have to restart the entire environment whenever you changed some code.

Java went to quite a bit of trouble to improve matters in this area with its classloader mechanism, but even that only takes you part of the way to what a really dynamic language can do. The classloader mechanism essentially allows bits of a system to be restarted, without losing state or interrupting other bits. That can be particularly important in a server context, where you may have active clients that you don't want to have to interrupt in order to load some new or changed code.

There are also other ways to mitigate the effects of having to restart the program to load code, and some of them are worth doing from a software design perspective anyway, such as separating components that ought to be separated (e.g. separating the development environment from code being developed). But there are tradeoffs, not only in capabilities but also in the implementation complexity of the approaches the more static systems need to use to emulate dynamic functionality.

It's true that Lisp and Smalltalk both have a kind of "the image is the world" perspective and treat issues surrounding redefinition and the like in terms of it, and even the Haskells and O'Camls of the world have yet to catch up to that. I only want to dissuade people of the notion that "static typing" necessarily means "edit/compile/test/crash/debug." Hopefully in the future, one of the benefits that will come out of the Acute effort will be even more compelling support for "dynamic loading and controlled rebinding to local resources," aka "solving the upgrade problem."

I'll prove by counter-example:

Naughty Dog's Goal compiler was highly incremental - we would press CTRL+T in Emacs, the code would be compiled, then sent to the execution environment (the PS2) and get patched into the running run-time. Goal is a Scheme variant, but we had static typing to a large degree and in addition, it was a very imperative language.

So, as you can see - there's no relationship between static typing and incremental updates. Quite the contrary.

First of all, a characterization of Goal as "a Scheme variant, but we had static typing to a large degree" is, to put it mildly, not compelling as a counterexample of the difficulties in achieving coherent incremental update in statically-typed languages. Regardless, it's certainly true that there's no necessary relationship between static typing and incremental updates if you don't mind that your incremental updates can cause type unsoundness or, in the case of a running system, drop state on the floor.

If you wish not to allow incremental updates to (potentially) make your system incoherent, though, you need some level of mechanism to prevent it. I refer you to Acute: High-level Programming Language Design for Distributed Computation, which deals with dynamic linking and threads as well as distribution; and The Missing Link - Dynamic Components for ML, which describes Alice ML's approach to the problem. These are probably the best extant work on addressing the real issues of dynamic linking in actual strongly-and-statically-typed languages with pervasive Hindley-Milner type inference.

I don't think I was arguing that there aren't any difficulties in achieving coherent incremental updates in a statically-typed language. I was just stating the fact that it is possible. Actually, I very much agree that it is quite difficult - especially if you want to have it done automagically.

In our case, we simply lived with the dangers of incremental updates. Our updates typically were code updates. In practice (for us, mind you), we didn't need to change data-types that often, and when we did - we could usually get by with appending a new member at the end of the structure, or reuse paddings. When we couldn't get away with that, we simply followed the following procedure, which mostly worked: 1) Update the data type (no code has yet to use the new data type, so we're good), 2) Update the static data, using this data type, and then 3) Update code that is using the data. It would have been much better if there was an automatic way of doing this, but it worked.

Of course, if your data structure refers to external data, like e.g. levels on disk, then this won't work - you need to reprocess all the external data. But, as I said - this doesn't happen often. By the way, the value of incremental updates is huge in terms of programmer productivity, so I'd just like to say that it is great that people are actively working on this, and I will definitely check out Acute and Alice ML. Thanks for the links - this is exactly why I love Lambda the Ultimate, I learn something new every time I visit these pages!

Thanks for the very patient response. As usual, I think I've come on too strongly. Of course there's great value in, e.g. Lisp's traditional ability to redefine functions/variables at any time, even with the burden of responsibility that that places on the programmer—there's a good argument to be made that the whole point of Lisp is "with great power comes great responsibility," and contrary to the impression that I generally give here, I'm sympathetic to that argument.

As you obviously are aware, things get hairier if you attempt to apply the "level of staticness," if you will, of an ML or Haskell to the question without essentially saying "and here we devolve to fully dynamic typing." It's perfectly reasonable to say "That's not a goal that I have." But if you do, or are simply curious, I think you will find those references informative, even if impractical. :-)

Paul wrote: Regardless, it's certainly true that there's no necessary relationship between static typing and incremental updates if you don't mind that your incremental updates can cause type unsoundness or, in the case of a running system, drop state on the floor.

Just to check I follow: are you saying that statically typed languages will find it harder to avoid dropping state on the floor than dynamically typed languages? If so, why?

I guess you might mean that it makes a mockery of the kind of guarantees that static type systems are supposed to give you if there is such a gaping hole. If so, I disagree: I do think the benefits of type safety tend to get oversold, but not being a panacea doesn't stop them being meaningful.

edit: changed above para after Paul's reply, since it was a bit incoherent, 'tho Paul figured out what I meant...

Charles Stewart: Just to check I follow: are you saying that statically typed languages will find it harder to avoid dropping state on the floor than dynamically typed languages? If so, why?

No, I was making something closer (but still not quite there) to your next point, that is, a cultural one: folks who prefer what guarantees are possible in statically-typed languages aren't likely to be happy with a proclaimed "solution" to incremental updating that carries a significant risk of damaging the integrity of a running system.

Charles Stewart: I guess you might mean that it makes a mockery of the kind of guarantees that static type systems are supposed to give you in the presence of such a gaping hole. If so, I disagree: I do think the benefits of type safety tend to get oversold, but not being a panacea doesn't stop them being meaningful.

I agree with this. Heck, I even enjoy Lisp's free-for-all approach to this—it might even be the thing I appreciate most about dynamically-typed languages. Being able to SSH-tunnel to a running process, start a REPL, and fix whatever's broken even as it's running is a killer feature. All I'm pointing out is that, as seems to me to so often be the case, there's a tendency to say something that sounds an awful lot like "incremental updating has nothing to do with static types" or "incremental updating is a solved problem," when what's going on in the research being referred to is something that goes quite a bit beyond whatever the claimed staticness (e.g. Goal) or claimed safety (dropping state in a running system, new code being observationally inconsistent with the code it's replacing) of the existing approaches is. It's not that everyone needs the strong guarantees; it's that until and unless the research is done, too many people believe, incorrectly, that no such strong guarantees are possible, and the misinformation tends to spread.

... I'd actually got the wrong end of the stick of the comment of yours I replied to. There does seem to be a disconnect between the kind of expectations one has between the local claims of value-meaningfulness of this one expression one gets with the types-as-assertions in the soft-typing/clean-C++ neck of the woods, and the holistic guarantees that one gets with Haskell-style load-up-all-your compile-time checks on our integrated value-inference system.

I only know about Goal by reputation, so I can't comment on specifics. But the relationship between static typing and incremental updates has to do with the degree to which static type information is erased in the compiled code. Because the information is static, it's conventionally assumed that it doesn't need to be explicitly present in the compiled code. However, dropping that information has a cost in terms of what kinds of incremental updates are possible.

There are many ways this can be addressed, from imposing restrictions on what constitutes a valid update, to retaining more information at runtime and, typically, compromising on optimizations. It sounds as though Goal took something closer to the latter approach, but generally statically typed languages tend much more strongly towards the former approach. At least in the case of the languages inspired by type theory, the update question is complicated by concerns about semantic integrity, although I'm sure the prospect of forgoing basic compilation optimizations is not an insignificant factor, either.

It continues to seem to me that a lot of both the disagreements over static vs. dynamic typing as well as approaches to adding desirable features in the static case are at least potentially solved by abandoning type erasure. You have to abandon it to get type-safe marshaling/unmarshaling; you have to abandon it to get type-safe distributed programming; you have to abandon it to get type-safe dynamic linking; you have to abandon it to get proof-carrying code...

I seem to recall that I got some push-back when I said "down with type erasure" before. Can someone refresh my memory as to what the issues are, or where that thread is?

Don't you lose sacrifice some of the optimizations? As I understand it, Alice ML chose a compromise solution where the granularity is at the module level. This allows type erasure within a module, but provides a form of open programming at the targeted component level.

One is removal of metadata. Excluding targets with tight memory constraints--there is often no reason to remove metadata from the generated code image. Even in the C/C++ world, such information is often kept around until the final link, and is also kept around in the final executable if you pass the "-g" flag to your compiler. (What, after all, is debugging info but metadata describing the types of terms)? Unfortunately, there's no portable way to get at the stabs/dwarf/whatever in a C/C++ program, but that's another issue.

Another form of type erasure is found in code optimization. Removal of runtime checks which are known to always be true (by this I mean "proven by the compiler" as opposed to "believed by the programmer"); conversion of dynamic lookups to static lookups, and other optimizations where type lookups which always return the same result are replaced with the result. Such optimizations must often be reduced or not done at all if runtime replacement of types is to be done--they depend heavily on the assumption that certain things won't change.

In languages with type systems more expressive than C/C++ - such as ML or Haskell or others derived from polymorphic lambda calculi - types are generally not fully "static" in the way metadata is. In particular, you generally have to pass witness types instantiating polymorphic definitions, in order to be able to determine the actual types of objects used/constructed in polymorphic code. Eliminating this (runtime) type passing is the interesting part of type erasure that PL theory usually is concerned with.

In particular, you generally have to pass witness types instantiating polymorphic definitions, in order to be able to determine the actual types of objects used/constructed in polymorphic code. Eliminating this (runtime) type passing is the interesting part of type erasure that PL theory usually is concerned with.

If I understand the above correctly, then monomorphized code would not suffer from the above problem, correct? We have a rudimentary knowledge of what types are being processed at a given time due to the code duplication. Not sure this buys you much in real life, but given monomorphization doesn't result in huge code blowups like one might expect, perhaps it might find some use. I'm not sure if it requires whole program analysis though.

Yes, monomorphisation can eliminate this. But monomorphisation is only applicable to limited forms of polymorphism, and it requires whole program compilation or variations thereof (like with C++ templates). The MLton compiler for SML does this.

The programs for which you can do monomorphisation form a strict subset of the programs for which you can do type erasure. Monomorphisation is inapplicable to more expressive, but still type-erasing languages like OCaml or Haskell, because of features like higher-ranked or first-class polymorphism, existential types, or polymorphic recursion. In the presence of these, actual instantiations can depend on dynamic values.

BTW, this is precisely the reason why C++ imposes certain ad-hoc restrictions on templates, e.g. prohibiting virtual template members - they would give rise to a form of first-class polymorphism, and hence destroy the monomorphisation approach to template compilation.

The programs for which you can do monomorphisation form a strict subset of the programs for which you can do type erasure. Monomorphisation is inapplicable to more expressive, but still type-erasing languages like OCaml or Haskell, because of features like higher-ranked or first-class polymorphism, existential types, or polymorphic recursion.

So an approach like that of .NET would work: JIT specialization of code + sharing where possible. Introducing some form of runtime information+compilation is thus necessary for such higher-ranked programs?

Jitting does not solve the general problem. For example, with existential types, the required type information does not come from a caller, but is retrieved from a value encapsulating it, inside some function. You would have to jit the continuation of the retrieval operation everytime control passes it if you wanted to achieve monomorphisation that way.

So, yes, some form of runtime type information will be necessary - unless your language has the valuable property that does enable type erasure (the property in question is known as parametricity).

Runtime compilation is an independent issue.

For example, with existential types, the required type information does not come from a caller, but is retrieved from a value encapsulating it, inside some function. You would have to jit the continuation of the retrieval operation everytime control passes it if you wanted to achieve monomorphisation that way.

Hmm, that seems a bit strange; I'll definitely have to think about it further.

In any case, thanks for the explanation. Last I heard, BitC was planning code specialization for performance reasons (no boxing). Given your explanation, it seems they must then forbid more expressive programs, or violate parametricity; regardless of the choice, then it seems they are crippling themselves since integrated theorem proving is a critical goal of BitC. Would you say that's accurate?

I believe the types of programs they are interested in (at least at first) are low-level programs (first-order?), not higher-ranked ones, so perhaps the first option is the only one for them.

AFAICS, dynamic specialisation is an inherently non-parametric operation. So I'd say you are right, they either have to keep some type info around at runtime, or restrict the forms of polymorphism they support. Whether that's "crippling" I don't know - of course, you can go a long way without higher forms of polymorphism.

Please see also the correction to my last reply to Scott Johnson for an example of first-class polymorphism. Note that jit-time specialisation would be very costly, as you would have to perform two specialisations for every iteration of the loop.

Just realized that this monomorphization thread is more relevant to me than I first thought...

I'm in the process of designing a language based on first class messages. The type system can support higher order functions and higher order messaging.

I was planning to target .NET using it as a first-order target language, where all message receivers/objects are compiled to ordinary .NET generic classes when sufficient info is available to resolve a definition to a parametric class. This strikes me as a form of monomorphization.

I'm aware of some situations which will require some dynamic compilation when sufficient info isn't available until runtime, and sometimes runtime method lookup, but I believe they will be rare corner cases, ie. folds over collections of distinct types.

So the dynamic type info of .NET is the only thing saving me from the pitfalls of monomorphization that you've described, is that correct?

From the sound of it, it seems to be pretty similar to what I've described, yes.

Is there a well known way to determine whether code is "monomorphilizable" vs. code that needs a polymormorphic type erasing representation? For my language above, I'd like to be able to monomorphize when I can, and just compile to using straight 'object' when I can't.

then determining simply if the number of "versions" of a polymorphic function is finite or not.

One annoying thing about C++, I guess, is you generally have to choose between fully monomorphic generics (using templates or ad-hoc static overloading) or a fully polymorphic generics (using virtual functions and specification using a base class). You can combine the two approaches, of course, but I doubt the language semantics give compilers too much leeway to figure out an ideal set of function implementations.

I think I know what your talking about...but not being familiar with how ML works under the hood, I'm interested in hearing more.

We'll ignore C, as its type system is simple. We'll also ignore the issue of type inference for now. :)

The main feature of ML's type system without a direct analog in C++ is the algebraic datatype--in particular, the algebraic sum. (C++ does have unions, but they are unsafe). If we have a List(t) datatype, there are typically two cases to consider--the empty case, and the non-empty one; these are treated as two distinct types in ML. (In C++ one typically unifies these, and uses NULL pointers to encode the empty list as a special case--a distinction beyond the type system. One could also use subtype polymorhism, and have empty-and non-empty lists as subclasses of an abstract list type. This is a closer analog to algebraic sums, and expresses the distinction between the empty/non-empty list in the type system, but this is seldom done in practice). Functions can be written to take an arbitrary List(t) as argument, and may have match clauses which give different behavior on empty and non-empty lists.

In the case of a C++ implementation using inheritance, no attempt by the language is typically made to perform complete type erasure. Vtables are kept around, and dynamic dispatch is used to select between the non-empty and empty versions as appropriate. (This can be expensive, which is why C++ lists aren't implemented in this fashion). In the case of ML, though, no "vtables" or other metadata indicating type is used in dispatch. Am I correct?

If so, how does this work exactly? One difference between algebraic sums and general inheritance is that the number of summands which form a given algebraic type is fixed (a list can either be empty or not, for example), but the number of classes which can inherit from a given base class is not.

I would love to hear more on this topic; feel free to point me at books or papers as well.

This relates to an oldish thread between myself and Curtis W, which unfortunately became contentious, because he asserted (by analogy—it became quite clear that Curtis understood the limits of it) that incomplete pattern matching on variant types is tantamount to dynamic casting in some sense. Setting aside how good or bad one feels that analogy is, there's an important point there, which is that a function that relies on incomplete pattern matching of variant types can't be total, and this is based on a crucial point about variant types: the variants are all known at compile time, so if any of them aren't matched, the function will fail when faced with such a term.

In O'Caml, however, this restriction is both known, and known to be undesirable in some ways, so in addition to classical variant types, O'Caml offers polymorphic variants, which feature bound constraints (that is, you can refer to polymorphic variants that are "at least" this type, "at most" that type, or fully-specified). Under the covers, the way this works is, of course, by tagging, so there is a bit of runtime overhead associated with matching; nevertheless the construct is fully statically sound. My post here recapitulates an example from "Code Reuse Through Polymorphic Variants," in which polymorphic variants are applied to solving the Expression Problem. Lately we've begun to see several different approaches to overcoming the extreme staticness of classical variant types—see the materials on the Expression Problem in Scala ("Independently Extensible Solutions to the Expression Problem") and gbeta, for example.

If we have a List(t) datatype, there are typically two cases to consider--the empty case, and the non-empty one; these are treated as two distinct types in ML.

No, that is not correct. There is only one type, which has two different constructors. These do not form separate types, in the same way two integer constants do not form separate types (note that int can also be understood as a predefined algebraic datatype). Constructors are not types -- rather, they have the same technical status as labels of a record type (and are in fact dual to those); both just denote an index. Technically, this is quite different from the OO encoding using subtyping, even though the effect is similar.

Note that ML also has an infinite sum type -- the exception type.

In any case, all this is completely unrelated to what I was talking about. Sum types have nothing to do with (parametric) polymorphism.

To see what I actually meant, assume you have a polymorphic language with a function

toString : forall a. a -> String

that can convert any type of value into a (useful) string representation. Obviously, to perform its task, it has to know the actual type "a" it is used at. Now consider this simple example:

print(x) = output(toString(x))

The function print again is fully polymorphic, but it calls toString. In order to have the relevant type information at the call site of toString, it must be passed to print - unless you monomorphise the definition of print by copying it for each type it is used with, see naasking's posting.

ML does not allow functions like toString, thus types can be erased. Haskell supports functions like that, but does something similar to vtables to get around passing actual types. In ML, you have to make the "vtable" explicit.

Just for completeness, here is a simple example of first-class polymorphism, where monomorphisation is not possible:

g(f, x, b) = if b then f(x) else f(666)
g(toString, true)

Edit: Sorry, it was late. Scratch that example, it does not make much sense. Here is a proper one:

g(fs) = for i = 0..len(fs)-1 do (fs[i](5); fs[i]("foo"))

This function receives a vector of polymorphic functions and applies each to 5 and "foo". The vector can be constructed dynamically, and at the point it is constructed you generally do not know how it will be used. Consequently, there is no way monomorphisation could be applied.

No, that is not correct. There is only one type, which has two different constructors. These do not form separate types, in the same way two integer constants do not form separate types (note that int can also be understood as a predefined algebraic datatype). Constructors are not types -- rather, they have the same technical status as labels of a record type (and are in fact dual to those); both just denote an index. Technically, this is quite different from the OO encoding using subtyping, even though the effect is similar.

For me, each value that leads to a different code path is a distinct type. So null and non-null-list are different types.

Most programs in "traditional" programming languages are only partially specified in regard to the above, which leads to many subtle bugs. Functional programming languages are better in this respect.

For me, each value that leads to a different code path is a distinct type. So null and non-null-list are different types.

Your definition of type is parameterized over a program? The values nil and a cons cell do not necessarily lead to different code paths in all programs---so they are only sometimes different types? (Or do you mean "potentially lead to different code paths", ie, everything is a type?)

Also: are two strings of different types if their contents are different? The type of an integer changes when it's incremented?

Also: are two strings of different types if their contents are different? The type of an integer changes when it's incremented?

Sometimes yes. That's the nature of dependent types is it not?

Sometimes yes. That's the nature of dependent types is it not?

Well yes, but taking that as a definition of type would seem to preclude "more" useful notions of type systems (say, those with decidable checking). I really should have added "necessarily" in two places in the sentence you quoted.

Two strings with different contents are both the same type and not the same type. They are both from the type of strings... but one might have a type that has the members of "hello", and the other is a type that has members of "world". Any particular value can belong to a myriad of type families.

From the moment two strings can lead to different code paths, then they are different types.

If an integer is incremented, then its type changes only if the new value can lead to different code paths.

When I/O is involved, it seems like then you could get up to as many types as there are possible bits in the variable? Not that it would happen in all systems, but it is perhaps interesting to think about the worst case. How would that work out in terms of programmer and maintainer understanding and productivity?

For example, the set of integers is one type. Individual values do not become types themselves unless used as such.

Here is a concrete example: the Direction enumeration. Usually, it goes like this:


enum Direction {
Left = 1,
Right,
Top,
Bottom
}


Integers 1, 2, 3 and 4 are not different types, unless specifically required, as in the case of the Direction enumeration.

If we had an I/O function which prompted the user for direction, would would have to promote the result from type int to type Direction.

This ties nicely with the discussion dependent types and linear types we had some time ago.

Types are defined in terms of their corresponding (families of) type systems, no? You have an ad-hoc, informal type system that you layer across existing ones, and that's fine - but it's not the same system, and statements about what is a type in that system aren't meaningful regarding what's a type in another system.

Sum types, as commonly understood, do not involve subtyping.

If we have a List(t) datatype, there are typically two cases to consider--the empty case, and the non-empty one; these are treated as two distinct types in ML.

In the case of ML, though, no "vtables" or other metadata indicating type is used in dispatch. Am I correct?

If one accepts your usage of "type", then you are not correct: ML does not do type erasure, but preserves a run-time tag associated with each value indicating its type, to the extent of identifying which constructor built that value.

(I find this a remarkably odd usage of "type", myself.)

See Polymorphic Type Reconstruction for Garbage Collection without Tags. This paper shows how you can reconstruct the types of heap values during the execution of ML programs without any type passing, essentially by running type inference again. It's claimed that any term whose type cannot be reconstructed cannot be used in the rest of the program - that ought to be about as true as parametricity. Running the garbage collector seems like a modest cost to support a code upgrade that requires finding the types of every value on the heap, especially compared to the overhead of using explicit type-passing.

I don't remember which thread you're thinking of, but the optimization issue is likely to remain a big one in practice. If a particular type of bit pattern is expected at a term's compiled representation, you limit the ability to change the expected bit pattern without updating the compiled code for every term through which that pattern flows. Untyped languages get around this with their universal type representations. To do something comparable with a statically-checked language, at the limit, the internal implementation would need to look a lot like a completely untyped Lisp, and its performance would be that of the untyped language.

Something like that could be useful to have (are there any examples?), but I bet it would just result in compilers which try to optimize anyway, and re-impose limits on what can be done dynamically. Part of the issue here is that it really isn't always necessary to be able to do everything dynamically.

[Edit: of course Google easily finds Paul's Down with type erasure! battle cry.]

Doing really late dynamic binding seems to me like it would bring with it all sorts of scary debugging issues. It would depend on how good the type system is, and how well people make use of it. If everything devolves into void* or object then I wouldn't want to go there.

What issues are you thinking of?

(Given that I've never used Smalltalk, I'm pretty clueless about what the reality of debugging late-bound dynamic systems is actually like. So I could be scared of nothing real. It anecdotally sounded to me like in Smalltalk you would basically have to send your entire world to somebody else if you wanted them to reason about it because basically any part of it could have been changed locally. So maybe you can't even copy and paste code to send folks, at least in situations where you are really trying to nail down what is going on.)

What I have seen in the systems I have used is that when something is late-bound or is dynamically typed to the point of basically being void* in the source code, it can be very difficult for me to reason about what is causing bug XYZ that I've just been assigned to fix - when compared to a more statically typed situation.

And, if things can and will be re-binding themselves to be different things all the time... zoiks.

In reality, my (relatively small) experience with languages like this is that these issues rarely come up and rarely come up in a big way. You are right though that these are potentially issues. But, for example, in Scheme you can, anywhere, write (set! + myfunc), so in theory, understanding (+ 2 2) in an incompletely known context is impossible. However, such code does not actually happen in an uncontrolled manner ((set! + myfunc) actually does happen though.).

Another thing I think you miss is to be this highly dynamic, or at least, in the languages that are archetypes for extreme late-binding also carry around tons of run-time information allowing you to easily and comprehensively examine. I'm not a big fan of Smalltalk, but I recommend playing around with it and it's debugging/reflection abilities to see what it's like. My main issue with debugging in Smalltalk does come in part from late-binding, but only at the level of a typical OO languages: finding the true cause of an error can have you wandering all over Smalltalk's relatively complex inheritance heirarchy. I'm not a big fan of deep inheritance.

But, for example, in Scheme you can, anywhere, write (set! + myfunc), so in theory, understanding (+ 2 2) in an incompletely known context is impossible. However, such code does not actually happen in an uncontrolled manner ((set! + myfunc) actually does happen though.)

I think it's worth mentioning that many module systems for Scheme constrain this behavior, including the R6RS library system, in which "all explicitly exported variables are immutable in both the exporting and importing libraries". This improves the ability to reason about code statically, whether by human or machine.

On a somewhat related note, the DrScheme REPL avoids the inconsistencies that can arise with dynamic loading of modified code by the simple expedient of a Run button which restarts execution of the current program in a fresh environment.

I guess the take-home message is that raould can use some Scheme systems without fear. :)

...and I really do want to have the time to play with PLT and Erlang (especially since they have some tools - MrFlow, Dialyzer - which could make me a little less scared of the dynamic typing).

Scheme was a favourite in college until I met SML :-)

There have been some attempts in this direction, particularly with robotics (providing the students with an actual robot, a programming language, simulator, and debugger). An interesting new approach, given the importance of multi-core programming, is the Parallax Propeller. I think it hits your points: it's a self-contained computer (microcontroller) with in-circuit monitor and debugging, a low-level language (Propeller Assembly), and a high-level language (Spin). Spin is higher-level than Propeller Assembly, but not much higher. It does abstract away some of the smaller details of running the processor, so it's easier to pick up.

An interesting feature is that the machine bootstraps into Spin, so that initial programming is in the high-level language, with the ability to "drop down" into assembly where needed. This is similar to the model used in old consumer-grade 8-bit micros, and might be less intimidating to beginning programmers.

Do you a think a virtual machine that looks low level would be distinguishable from an actual low level real machine? To beginning programmers? Everything is mediated by an interface anyway; one necessarily takes it on faith that one is actually directly manipulating any given model. We can discriminate no finer than the tools we use.

Schematics, really? I suppose an animation of a machine whose assembler was used would be a big help to explain what is meant by code execution. (Normally I reply when I'm more immediately interested in applying ideas, but here I'm just commenting without any plans.)

It's easily distinguishable, as anyone who's seriously crashed their actual hardware knows :-)