[TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages

[Mark Janssen]

> 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