What is Expressiveness in a Computer Language

[Marshall]

There is a third option: it may be that at the point where I am writing
this code, I simply don't bother yet whether a and b will always be
numbers. In case something other than numbers pop up, I can then
make a decision how to proceed from there.

Ouch; I have a really hard time understanding this.

I can't see how you'd call + on a and b if you think they might
not be numbers. If they could be something other than numbers,
and you're treating them as if they are, is that sort of like
doing a case analysis and only filling in one of the cases?
If so, wouldn't you want to record that fact somehow?


Marshall

 

[Chris Smith]

That was the point of my first sentence (quoted above). I take it, and I
assumed that you shared my view, that there is no single "the" type system --
that /a/ type system will yield judgements on matters which it has been
designed to judge.

Yes, I definitely agree.

My point was that if you leave BOTH the "something" and the response to
verification failure undefined, then your definition of a dynamic type
system is a generalization of the definition of a conditional
expression. That is (using Java),

if (x != 0) y = 1 / x;
else y = 999999999;

is not all that much different from (now restricting to Java):

try { y = 1 / x; }
catch (ArithmeticException e) { y = 999999999; }

So is one of them a use of a dynamic type system, where the other is
not?

Incidentally, using that idea, we get a fairly close analogy to the difference
between strong and weak static type systems.

I think, actually, that the analogy of the strong/weak distinction
merely has to do with how much verification is done. But then, I
dislike discussion of strong/weak type systems in the first place. It
doesn't make any sense to me to say that we verify something and then
don't do anything if the verification fails. In those cases, I'd just
say that verification doesn't really exist or is incorrectly
implemented. Of course, this would make the type system weaker.

I wonder whether that way of looking at it -- the "error" never happens since
it is replaced by a valid operation -- puts what I want to call dynamic type
systems onto a closer footing with static type systems.

Perhaps. I'm thinking some things over before I respond to Anton. I'll
do that first, and some of my thoughts there may end up being relevant
to this question.

b) I want to separate the systems of reasoning (whether formal or informal,
static or dynamic, implemented or merely conceptual, and /whatever/ we call 'em
;-) from the language semantics. I have no objection to <some type system>
being used as part of a language specification, but I don't want to restrict
types to that.

In the pragmatic sense of this desire, I'd suggest that a way to
characterize this is that your type system is a set of changes to the
language semantics. By applying them to a language L, you obtain a
different language L' which you can then use. If your type system has
any impact on the set of programs accepted by the language (static
types) or on any observable behavior which they exhibit (dynamic types),
then I can't see a justification for claiming that the result is the
same language; and if it does not, then the whole exercise is silly.

Of course, we can talk about what kinds of operations we want to forbid, but
that seems (to me) to be orthogonal to this discussion. Indeed, the question
of dynamic/static is largely irrelevant to a discussion of what operations we
want to police, except insofar as certain checks might require information
which isn't available to a (feasible) static theorem prover.

Indeed, that is orthogonal to the discussion from the perspective of
static types. If you are proposing that it is also orthogonal with
respect to dynamic types, that will be a welcome step toward our goal of
a grand unified type theory, I suppose. I have heard from others in
this thread that they don't believe so. I am also interested in your
response to the specific example involving an if statement at the
beginning of this reply.

 

[Rob Thorpe]

Rob Thorpe schreef:


There are many different languages under the umbrella of "assembly", so
your suggestion is bound to be false.

Well yes, it is false, I know of several typed assemblers.
But I mentioned that point elsewhere so I didn't repeat it. This
thread is huge and I expect no-one will have read it all, so I will be
more clear in future.

 

[Darren New]

I can't see how you'd call + on a and b if you think they might
not be numbers.

Now substitute "<" for "+" and see if you can make the same argument.

 

[Chris Smith]

Ouch; I have a really hard time understanding this.

I can't see how you'd call + on a and b if you think they might
not be numbers. If they could be something other than numbers,
and you're treating them as if they are, is that sort of like
doing a case analysis and only filling in one of the cases?
If so, wouldn't you want to record that fact somehow?

The obvious answer -- I don't know if it's what Pascal meant -- is that
they might be 4x4 matrices, or anything else that behaves predictably
under some operation that could be called addition. As a mathematical
analogy, the entire mathematical field of group theory comes from the
idea of performing operations on values without really knowing what the
values (or the operations) really are, but only knowing a few axioms by
which the relationship between the objects and the operation is
constrained.

[As an interesting coincidence, group theory papers frequently use the
addition symbol to represent the (arbitrary) binary relation of an
Abelian group. Not that this has anything to do with choosing "+" for
the example here.]

Programming languages do this all the time, as well. The most popular
example is the OO sense of the word polymorphism. That's all about
being able to write code that works with a range of values regardless of
(or, at least, a range that less constraining than equlity in) types.

 

[Chris Uppal]

So what you are suggesting may be an interesting notion, but it's not
what is called "type" in a technical sense. Overloading the same term
for something different is not a good idea if you want to avoid
confusion and misinterpretations.

Frivolous response: the word "type" has been in use in the general sense in
which I wish to use it for longer than that. If theorists didn't want ordinary
people to abuse their technical terms they should invent their own words not
borrow other people's ;-)

Just for interest, here's one item from the OED's entry on "type" (noun):

The general form, structure, or character distinguishing
a particular kind, group, or class of beings or objects;
hence transf. a pattern or model after which something is made.

And it has supporting quotes, here are the first and last:

1843 Mill Logic iv. ii. §3 (1856) II. 192
When we see a creature resembling an animal, we
compare it with our general conception of an animal;
and if it agrees with that general conception, we include
it in the class. The conception becomes the type of comparison.

1880 Mem. J. Legge vi. 76
Every creature has a type, a peculiar character of its own.

Interestingly the first one is from:
John Stuart Mill
A System of Logic
(but it's not mathematical logic ;-).

OK, I admitted I was being frivolous. But I really don't see why a type system
(as understood by type theorists) /must/ have no runtime element. Just as I
wouldn't stop calling a type system a "type system" if it were designed to work
on incomplete information (only part of the program text is available for
analysis) and so could only make judgements of the form "if X then Y".


[JVM dynamic class loading]

Incidentally, I know this scenario very well, because that's what I'm
looking at in my thesis .

All of this can easily be handled
coherently with well-established type machinery and terminology.

I'd be interested to know more, but I suspect I wouldn't understand it :-(

A type system states
propositions about a program, a type assignment *is* a proposition. A
proposition is either true or false (or undecidable), but it is so
persistently, considered under the same context. So if you want a type
system to capture temporal elements, then these must be part of a type
itself. You can introduce types with implications like "in context A,
this is T, in context B this is U". But the whole quoted part then is
the type, and it is itself invariant over time.

But since the evolving type-attribution that I'm thinking of also includes time
as a static element (at each specific time there is a specific attribution of
types), the dynamic logic can also be viewed as invarient in time, since each
judgement is tagged with the moment(s) to which it applies.

But there we go. I don't expect you to agree, and though I'll read any reply
with interest, I think I've now said all I have to say in this particular
subthread.

Cheers.

-- chris

 

[Chris Smith]

Programming languages do this all the time, as well. The most popular
example is the OO sense of the word polymorphism. That's all about
being able to write code that works with a range of values regardless of
(or, at least, a range that less constraining than equlity in) types.

It's now dawned on me that I need not have restricted this to the OO
sense of polymorphism. So let me rephrase. Polymorphism *is* when
programming languages do that.

 

[Marshall]

But, as a sort of half-way, semi-formal, example: consider the type environment
in a Java runtime. The JVM does formal type-checking of classfiles as it loads
them. In most ways that checking is static -- it's treating the bytecode as
program text and doing a static analysis on it before allowing it to run (and
rejecting what it can't prove to be acceptable by its criteria). However, it
isn't /entirely/ static because the collection of classes varies at runtime in
a (potentially) highly dynamic way. So it can't really examine the "whole"
text of the program -- indeed there is no such thing. So it ends up with a
hybrid static/dynamic type system -- it records any assumptions it had to make
in order to find a proof of the acceptability of the new code, and if (sometime
in the future) another class is proposed which violates those assumptions, then
that second class is rejected.

I have to object to the term "hybrid".

Java has a static type system.
Java has runtime tags and tag checks.

The two are distinct, and neither one is less than complete, so
I don't think "hybrid" captures the situation well.


Marshall

 

[Chris Smith]

Java has a static type system.
Java has runtime tags and tag checks.
Yes.

The two are distinct, and neither one is less than complete

How is neither one less than complete?

 

[Rob Thorpe]

Luca Cardelli has given the most convincing one in his seminal tutorial
"Type Systems", where he identifies "typed" and "safe" as two orthogonal
dimensions and gives the following matrix:

| typed | untyped
-------+-------+----------
safe | ML | Lisp
unsafe | C | Assembler

Now, jargon "dynamically typed" is simply untyped safe, while "weakly
typed" is typed unsafe.

Consider a langauge something like BCPL or a fancy assembler, but with
not quite a 1:1 mapping with machine langauge.

It differs in one key regard: it has a variable declaration command.
This command allows the programmer to allocate a block of memory to a
variable. If the programmer attempts to index a variable outside the
block of memory allocated to it an error will occur. Similarly if the
programmer attempts to copy a larger block into a smaller block an
error would occur.

Such a language would be truly untyped and "safe", that is safe
according to many peoples use of the word including, I think, yours.

But it differs from latently typed languages like python, perl or lisp.
In such a language there is no information about the type the variable
stores. The programmer cannot write code to test it, and so can't
write functions that issue errors if given arguments of the wrong type.
The programmer must use his or her memory to substitute for that
facility. As far as I can see this is a significant distinction and
warrants a further category for latently typed languages.


As a sidenote: the programmer may also create a tagging system to allow
the types to be tracked. But this is not the same as saying the
language supports types, it is akin to the writing of OO programs in C
using structs.

 

[rossberg]

But it differs from latently typed languages like python, perl or lisp.
In such a language there is no information about the type the variable
stores. The programmer cannot write code to test it, and so can't
write functions that issue errors if given arguments of the wrong type.
The programmer must use his or her memory to substitute for that
facility. As far as I can see this is a significant distinction and
warrants a further category for latently typed languages.

Take one of these languages. You have a variable that is supposed to
store functions from int to int. Can you test that a given function
meets this requirement?

You see, IMO the difference is marginal. From my point of view, the
fact that you can do such tests *in some very trivial cases* in the
languages you mention is an artefact, nothing fundamental.

- Andreas

 

[Rob Thorpe]

Take one of these languages. You have a variable that is supposed to
store functions from int to int. Can you test that a given function
meets this requirement?

The answer is no for python and perl AFAIK. Also no for lisp _aux
naturelle_ (you can do it by modifying lisp though of-course, I believe
you can make it entirely statically typed if you want).

But the analogous criticism could be made of statically typed
languages.
Can I make a type in C that can only have values between 1 and 10?
How about a variable that can only hold odd numbers, or, to make it
more difficult, say fibonacci numbers?

You see, IMO the difference is marginal. From my point of view, the
fact that you can do such tests *in some very trivial cases*

They are not very trivial for practical programming purposes though,
they are important.

in the
languages you mention is an artefact, nothing fundamental.

The cases can be far from trivial. In lisp a type specifier can mean
something like "argument must be a 10x10 matrix with top corner element
larger than 35" You can also, for example, easily make predicates that
tell if a value is odd, or a fibonacci number.

The system simply extends in different directions.

 

[Chris Uppal]

Marshall wrote:

[me:]

I have to object to the term "hybrid".

Java has a static type system.
Java has runtime tags and tag checks.

It has both, agreed, but that isn't the full story. I think I explained what I
meant, and why I feel the term is justified as well as I can in the second half
of the paragraph you quoted. I doubt if I can do better.

Maybe you are thinking that I mean that /because/ the JVM does verification,
etc, at "runtime" the system is hybrid ?

Anyway that is /not/ what I mean. I'm (for these purposes) completely
uninterested in the static checking done by the Java to bytecode translator,
javac. I'm interested in what happens to the high-level, statically typed, OO,
language called "java bytecode" when the JVM sees it. That language has a
strict static type system which the JVM is required to check. That's a
/static/ check in my book -- it happens before the purportedly correct code is
accepted, rather than while that code is running.

I am also completely uninterested (for these immediate purposes) in the run
time checking that the JVM does (the stuff that results in
NoSuchMethodException, and the like). In the wider context of the thread, I do
want to call that kind of thing (dynamic) type checking -- but those checks are
not why I call the JVMs type system hybrid either.

Oh well, having got that far, I may as well take another stab at "hybrid".
Since the JVM is running a static type system without access to the whole text
of the program, there are some things that it is expected to check which it
can't. So it records preconditions on classes which might subsequently be
loaded. Those are added to the static checks on future classes, but -- as far
as the original class is concerned -- those checks happen dynamically. So part
of the static type checking which is supposed to happen, has been postponed to
a dynamic check. It's that, and /only/ that which I meant by "hybrid".

Of course, /if/ we grant that runtime checking of the sort done by Smalltalk or
Lisp also constitutes a "type system" in some sense that puts it on a par with
static type checking, then that would be another, very different, reason to
claim that Java had a hybrid type system (though, in fact, I'd rather claim
that it had two independent type systems). But that's the bigger question
point under discussion here and I wasn't trying to beg it by using the word
"hybrid".

-- chris

 

[Dr.Ruud]

Chris Smith schreef:

Static types are not fuzzy

Static types can be fuzzy as well. For example: a language can define
that extra accuracy and bits may be used for the implementation of
calculations: d = a * b / c
Often some minimum is guaranteed.

I see it as quite reasonable when there's an effort by several
participants in this thread to either imply or say outright that
static type systems and dynamic type systems are variations of
something generally called a "type system", and given that static
type systems are quite formally defined, that we'd want to see a
formal definition for a dynamic type system before accepting the
proposition that they are of a kind with each other.

The 'dynamic type' is just another type.

 

[Eliot Miranda]

Execpt that every operation is implemented by every object in Smalltalk.

No they are not. Objects implement the methods defined by their class
and (inherit) those implemented by the class's superclasses. Note that
classes do _not_ have to inherit from Object, and so one can create
classes that implement no methods at all. It is a common idiom to
create a class that implements two methods, an initialization method and
a doesNotUnderstand: method, so create a transparent proxy that
intercepts any and all messages sent to it other than the initialization
method (*).

[(*) With suitable hackery (since Smalltalk gives access to the
execution stack through thisContext) one can also invoke
doesNotUnderstand: if the initialization message is sent from any object
other than the class.]

Unless you specify otherwise, the implementation of every method is to
call the receiver with doesNotUnderstand. (I don't recall whether the
class of nil has a special rule for this or whether it implements
doesNotUnderstand and invokes the appropriate "don't send messages to
nil" method.)

No. The run-time error of trying to invoke an operation that isn't
implemented by an object is to send the doesNotUnderstand: message.
This is another attempt to invoke an operation, i.e. whatever the
object's doesNotUnderstand: method is, if any. If the object doesn't
implement doesNotUnderstand:, which is quite possible, then the system,
will likely crash (either with an out of memory error as it goes into
infinite recursion) or hang (looping attempting to find an
implementation of doesNotUnderstand.

There are a number of Smalltalk extensions, such as
multiple-inheritance, that rely on implementing doesNotUnderstand.

Which has nothing to do with the separation between message send and
method invocation, or the fact that doesNotUnderstand: is a message
send, not a hard call of a given doesNotUnderstand: method.

 

[Darren New]

classes do _not_ have to inherit from Object,

I was unaware of this subtlety. Thanks!

 

[rossberg]

Rob Thorpe write:

The answer is no for python and perl AFAIK. Also no for lisp _aux
naturelle_ (you can do it by modifying lisp though of-course, I believe
you can make it entirely statically typed if you want).

But the analogous criticism could be made of statically typed
languages.
Can I make a type in C that can only have values between 1 and 10?
How about a variable that can only hold odd numbers, or, to make it
more difficult, say fibonacci numbers?

Fair point. However, there are in fact static type systems powerful
enough to express all of this and more (whether they are convenient
enough in practice is a different matter). On the other hand, AFAICS,
it is principally impossible to express the above property on functions
with tags or any other purely dynamic mechanism.

The cases can be far from trivial. In lisp a type specifier can mean
something like "argument must be a 10x10 matrix with top corner element
larger than 35" You can also, for example, easily make predicates that
tell if a value is odd, or a fibonacci number.

Now, these are yet another beast. They are not tags, they are
user-defined predicates. I would not call them types either, but that's
an equally pointless battle.

- Andreas

 

[Chris Uppal]

But then, I
dislike discussion of strong/weak type systems in the first place. It
doesn't make any sense to me to say that we verify something and then
don't do anything if the verification fails. In those cases, I'd just
say that verification doesn't really exist or is incorrectly
implemented.

Hmm, that seems to make what we are doing when we run some tests dependent on
what we do when we get the results. If I run a type inference algorithm on
some of my Smalltalk code, and it tells me that something is type-incorrect,
then I think I'd like to be able to use the same words for the checking
regardless of whether, after due consideration, I decide to change my code, or
that it is OK as-is. Minor point, though...

Anyway:

if (x != 0) y = 1 / x;
else y = 999999999;

is not all that much different from (now restricting to Java):

try { y = 1 / x; }
catch (ArithmeticException e) { y = 999999999; }

So is one of them a use of a dynamic type system, where the other is
not?

My immediate thought is that the same question is equally applicable (and
equally interesting -- i.e. no simple answer ;-) for static typing. Assuming
Java's current runtime semantics, but positing different type checkers, we can
get several answers.

A] Trivial: neither involves the type system at all. What we are seeing
is a runtime check (not type check) correctly applied, or made unnecessary by
conditional code. And, obviously we can take the same line for the "dynamic
type checking" -- i.e. that no type checking is involved.

B] More interesting, we could extend Java's type system with a NotZero
numeric type (or rather, about half a dozen such), and decree that 1 / x was
only legal if
x : NotZero
Under that type system, neither of the above would be type legal, assuming x is
declared int. Or both would be legal if it was declared NotZero -- but in both
cases there'd be a provably unnecessary runtime check. The nearest "dynamic
type system" equivalent would be quite happy with x : int. For the first
example, the runtime checks would never fire (though they would execute). For
the second the runtime "type" might come into play, and if it did, then the
assignment of 999999999 would take place /because/ the illegal operation (which
can be thought of as casting 0 to NotZero) had been replaced by a specific
legal one (throwing an ArithmeticException in this case).

C] A different approach would be to type the execution, instead of the value,
so we extend Java's type system so that:
1 / x
had type (in part) <computation which can throw ArithmeticException>. The
first example as a whole then would also have (in part) that type, and the
static type system would deem that illegal. The second example, however, would
be type-legal. I hope I don't seem to be fudging the issue, but I don't really
think this version has a natural "dynamic type system" equivalent -- what could
the checker check ? It would see an attempt to throw an exception from a place
where that's not legal, but it wouldn't make a lot of sense to replace it with
an IllegalExceptionException ;-)

D] Another possibility would be a static type checker after the style of
but extended so that it recognised the x != 0 guard as implicitly giving x :
NonZero. In that case, again, the first example is static type-correct but the
second is not. In this case the corresponding "dynamic type system" could, in
principle, avoid testing x for zero the second time. I don't know whether that
would be worth the effort to implement. In the second example, just as in
, the reason the program doesn't crash when x == 0 is that the "dynamic type
system" has required that the division be replaced with a throw.

One could go further (merge and [C], or [C] and [D] perhaps), but I don't
think it adds much, and anyway I'm getting a bit bored.... (And also getting
sick of putting scare quotes around "dynamic type system" every time ;-)

Personally, of the above, I find most appealing.

-- chris

 

[Chris Smith]

Chris Smith schreef:


Static types can be fuzzy as well. For example: a language can define
that extra accuracy and bits may be used for the implementation of
calculations: d = a * b / c
Often some minimum is guaranteed.

Who cares how many bits are declared by the type? Some specific
implementation may tie that kind of representation information to the
type for convenience, but the type itself is not affected by how many
bits are used by the representation. The only thing affected by the
representation is the evaluation semantics and the performance of the
language, both of which only come into play after it's been shown that
the program is well-typed.

The 'dynamic type' is just another type.

That's essentially equivalent to giving up. I doubt many people would
be happy with the conclusion that dynamically typed languages are typed,
but have only one type which is appropriate for all possible operations.
That type system would not be implemented, since it's trivial and
behaves identically to the lack of a type system, and then we're back
where we started.

 

[Pascal Costanza]

How expressive does that end up being for real problems ? I mean obviously in
some sense it's crippling, but how much of a restiction would that be for
non-accademic programming.

I don't know your definition of "real problem" , but ACL2 is
definitely used in industrial settings.

See
http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/intro-to-acl2.pdf


Pascal