Path: csiph.com!usenet.pasdenom.info!weretis.net!feeder1.news.weretis.net!feeder.erje.net!eu.feeder.erje.net!xlned.com!feeder3.xlned.com!news2.euro.net!newsgate.cistron.nl!newsgate.news.xs4all.nl!post.news.xs4all.nl!not-for-mail
MIME-Version: 1.0
In-Reply-To: <CAOvMSvXy=iJhUtMfncv-RE3HQw+7DJO-M1-TaeAFFhnDe9mpUA@mail.gmail.com>
References: <CAMjeLr_7A-NRtec=K_ZsjXA_oJHnD6+vpttz4Ma0vtDRbb+o2w@mail.gmail.com> <CAOvMSvXy=iJhUtMfncv-RE3HQw+7DJO-M1-TaeAFFhnDe9mpUA@mail.gmail.com>
Date: Tue, 16 Apr 2013 16:16:42 -0700
Subject: Re: [TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages
From: Mark Janssen <dreamingforward@gmail.com>
To: DeLesley Hutchins <delesley@gmail.com>
Content-Type: text/plain; charset=ISO-8859-1
Cc: types-list@lists.seas.upenn.edu, Python List <python-list@python.org>
Precedence: list
Newsgroups: comp.lang.python
Message-ID: <mailman.697.1366154203.3114.python-list@python.org>
Lines: 64
NNTP-Posting-Host: 2001:888:2000:d::a6
Xref: csiph.com comp.lang.python:43713

> 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