[TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages
dreamingforward at gmail.com
Tue Apr 16 19:16:42 EDT 2013
> 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....
More information about the Types-list