🚀 go-pugleaf

On 11 Mar 91 20:35:48 GMT, gudeman@cs.arizona.edu (David Gudeman) said:

gudeman> In article <PCG.91Mar10181749@aberdb.cs.aber.ac.uk> Piercarlo
gudeman> Antonio Grandi writes:

pcg> A point of order: I would not use 'dynamic types' here.  I would say
pcg> 'latent types'. The idea is that dynamically typed should be reserved
pcg> for the (currently rare!) case where the language allows the type of a
pcg> *value* to change dynamically,...

pcg> <type>		The equivalence class of all <values> to which
pcg> 			a given set of operations can be meanigfully
pcg> 			applied.

pcg> Now we switch to some more advanced language and we add while the
pcg> program is executing a new operation, say '/', with two arguments,
pcg> one is 'unsigned' and the other is 'positive' (nonzero).  Then we
pcg> can dynamically change the typing of the value '1', because now it
pcg> can be *both* an 'unsigned' and a 'positive'.

gudeman> This only happens in a statically typed language.  In a
gudeman> dynamically typed language you don't declare the types that an
gudeman> operator works on, so this doesn't happen.

No, no, we have *two* misunderstanding here. I have never said that in
this example one need declare *explicitly* the types of the arguments of
an operator; simply, that a type is defined by the operators that can be
meaningfully applied to the values of that type. Since / cannot be
meaningfully applied to zero, adding it to the language means that one
implicitly is distinguishing between the <type> 'unsigned' and
'positive', because the second argument to / cannot be zero.

gudeman> This definition of types originated with the implicit assumption that
gudeman> the set of operations are fixed.  When operations can be added at
gudeman> runtime, bizarre situations arise where the type of a value can
gudeman> change.  This doesn't shouldn't prompt us to add complexity to the
gudeman> language, trying to distinguish between <type> and <typing>.

But changing <type> is of the essence. It happens all the time. Every
time you use an interactive lanfguage like Scheme and you define a new
function. Also, when you edit the definition of a C++ struct and
recompile.

Consider the latter example; the <typing> has not changed, but the
<type> has. This is dangerous; for example all the values created under
the old definition may well be no longer meaningful. Data restructuring
is needed then.

This si for example well understood in the capability architecture
business; a capability architecture only has <typing>, and tags each
value with a type code. Each type code is associated with a type
manager, the module that implements all the operations on values with
that type code (this will be well known to you, but I repeat just to
provide context). Now if the type manager changes, often one has to
assign a new type code to it, because changes in the <type> should be
reflected in changes in the <typing>. Not necessarily, for example we
can keep the same <typing> if the new <type> is a superset (or even
subset) of the old, of course, as when we don't change the
encoding/decoding functions for composite values. Example in C++:

	struct Complex { float re, im; };
	Complex operator +(const Complex &a, const Complex &b) { ... };

If we change this to

	struct Complex { float real, imaginary; };
	Complex operator +(const Complex &a, const Complex &b) { ... };

We need not change the <typing> of complex <type> values; we just have
to edit and recompile 'operator +' with the names of the new
decomposition functions.

But if we change it to

	struct Complex { float im, re; }
	Complex operator +(const Complex &a, const Complex &b) { ... };

The <typing> has not changed, but the <type> has changed in a way such
that the <typing> chould change.

Naturally most people are blinkered in that they ignore the issue of
persistency, but unfortunately in the real world almost all data are
persistent, and the difference between <type> and <typing> is thus
terribly important.

An example of this is the protocol revision level field in many
protocols; each protocol is really a type specification, where each
packet header is a value in the type defined by the protocol operations
that it triggers.

I will venture as far as saying that the difference between <type> and
<typing> which is inherent in most all languages, operating systems,
databases out there is regrettable and is only really an efficiency
hack, just like the one between 'eq' and 'equal', and it generates much
the same class of problems.

gudeman> Rather we should drop this notion of <type> altogether and
gudeman> define

gudeman> <type>			a set of values.

This is wrong, as far as I can see, because then there is no way to know
the <type> or <typing> of a value. As soon as you instead have a
'typeof' operation, you create equivalence classes. Please note: in my
porposed definitions, <value> is just a number, and absolutely nothing
else, and it does not carry any other information than that number.

I think you are wrongly assuming, in other words, in your definition
above, that there is some magic way to know which set a value belongs
to, without encoding it into the value itself. This is not possible, I
am afraid. On the other hand if you encode the set into the value
itself, then you are defining types as equivalence classes, and your
definition and mine are exactly equivalent, except maybe that yours
hides the difference between <type> (a concept) and <typing> (an
economical implementation of that concept).

gudeman> Then no seperate notion of <typing> is needed.

Quite the opposite... The end result of your proposal is to drop the
notion of <type> and keep only that of <typing>, not viceversa.

gudeman> In fact, this is what is done in most dynamically typed
gudeman> languages.

In this you are right. Indeed in most languages, whatever their typing
discipline, one can only handle <typing>, not <types>. This is a gross
limitation, and one that is simply unacceptable when you have persistent
values. The limitation can be gotten around using gross hacks; for
example when the <type> changes but not the <typing>, e.g. when a new
release of Unix switches the implementation of /etc/passwd from a text
file to an hash file, you need a program to convert formats, whose role
is essentially that of converting one <type> to another to maintain ther
illusion that <typing> has not changed.

gudeman> It makes it trivial to do useful things like define hierarchies
gudeman> of types (subsets) and to have values that are of several
gudeman> different types (membership in different sets).

Actually it makes it incredibly opaque. I know no language that IMNHO
does a satisfactory job of reconciling the gross rigidities of doing
<typing> with the reality that <types> are equivalence classes. For
example, to repeat my usual party line, there ar eno languages that have
any decent algebra on the various aspects of <typing>; they all limit
the <typing> algebra to an awakward subset of the possibilities demanded
by applications.

gudeman> It also gives you powerful machinery for defining complex types
gudeman> and for deciding type membership.  It also gives you a fairly
gudeman> simple way to define the result of the 'typeof' function(s)
gudeman> even though a value may have may types: you just define some
gudeman> arbitrary (but useful) partition of the set of all values, and
gudeman> give each set a name.

This is just <typing>, according to my terminology. You have thrown away
the notion of <type> entirely.

gudeman> (There are people who complain about using the word "set" here
gudeman> since it makes it problematic to make <type> a value.  (eg: T
gudeman> is the type that contains all types that do not contains
gudeman> themselves.  Is T in the type T?)  However, that is a problem
gudeman> cause by defining <type> to be a value.  It is not inherent in
gudeman> defining a type as a set.)

While a <type> is an equivalence class, and thus not a value, a <typing>
can be represented as a value, e.g. by assigning to each <typing> class
an arbitrary code. Then these codes *do* form a <type>. This is like the
solution to paradoxes in Russell's (the mathematician, not the like
minded functional language :->) Principia...
--
Piercarlo Grandi                   | ARPA: pcg%uk.ac.aber@nsfnet-relay.ac.uk
Dept of CS, UCW Aberystwyth        | UUCP: ...!mcsun!ukc!aber-cs!pcg
Penglais, Aberystwyth SY23 3BZ, UK | INET: pcg@aber.ac.uk