> I'm not quite sure I understand your question, but I'll give it a shot. :-)
Thank you, and my apologies for my late reply. > The C/C++ model, in which the types are anchored to the machine hardware, in > the exception, not the rule. In the academic literature, "type theory" is > almost entirely focused on studying abstract models of computation that are > purely mathematical, and bear no resemblance to the underlying hardware. > The lambda calculus is the most general, and most commonly used formalism, > but there are many others; e.g. Featherweight Java provides a formal model > of objects and classes as they are used in Java. Understood, but I feel this is where theory has gone too far away from reality. Wikipedia (admittedly not an authoritative resource), lists a clear distinction between languages rooted to the Turing machine, and those rooted in lambda calculus: From: en.wikipedia.org: Programming_paradigm: "A programming paradigm is a fundamental style of computer programming. There are four main paradigms: object-oriented, imperative, functional and declarative. Their foundations are distinct models of computation: Turing machine for object-oriented and imperative programming, lambda calculus for functional programming, and first order logic for logic programming." While I understand the interest in purely theoretical models, I wonder two things: 1) Are these distinct models of computation valid? And, 2) If so, shouldn't a theory of types announce what model of computation they are working from? You say the C/C++ model is the exception, but in the programmer community (excepting web-based languages) it is the opposite. The machine model dominates. In fact, I'm not even sure how Java operates, but through some sorcery I don't want to take part in. > "Types and Programming Languages", by Benjamin Pierce, is an excellent > introductory textbook which describes how various language features, > including objects, can be formalized. If you are interested in OOP, Abadi > and Cardelli's "Theory of Objects" is the obvious place to start, although > I'd recommend reading Pierce's book first if you want to understand it. :-) > Abadi and Cardelli discuss both class-based languages, and pure object > languages. If you are interested in the type/object distinction in > particular, then I'll shamelessly plug my own thesis: "Pure Subtype Systems" > (available online), which describes a formal model in which types are > objects, and objects are types. If you are familiar with the Self language, > then you can think of it as a type system for Self. Thank you very much. I will look for them. > Once you have a type system in place, it's usually fairly straightforward to > compile a language down to actual hardware. An interpreter, like that used > in Python, is generally needed only for untyped or "dynamic" languages. > There are various practical considerations -- memory layout, boxed or > unboxed data types, garbage collection, etc. -- but the basic techniques are > described in any compiler textbook. Research in the areas of "typed > assembly languages" and "proof carrying code" are concerned with ensuring > that the translation from high-level language to assembly language is sound, > and well-typed at all stages. Very interesting. I appreciate the those leads.... -- MarkJ Tacoma, Washington -- http://mail.python.org/mailman/listinfo/python-list