What is Expressiveness in a Computer Language

[David Hopwood]

At the same time, though, maybe I do want
the compiler to infer that tax cannot be negative (or maybe it can; I'm
not an accountant; I know my tax has never been negative), [...]

Tax can be negative, e.g. when a business is claiming back VAT (sales tax)
on its purchases, but the things it is selling have lower-rated or zero
VAT (or it is making a loss).

Note that even without encapsulation, the kind of typing information
we're looking at can be very non-trivial in an imperative language. For
example, I may need to express a method signature that is kind of like
this:

1. The first parameter is an int, which is either between 4 and 8, or
between 11 and 17.

2. The second parameter is a pointer to an object, whose 'foo' field is
an int between 0 and 5, and whose 'bar' field is a pointer to another
object with three fields 'a', 'b', and 'c', each of which has the full
range of an unconstrained IEEE double precision floating point number.

3. After the method returns, it will be known that if this object
previously had its 'baz' field in the range m .. n, it is now in the
range (m - 5) .. (n + 1).

4. After the method returns, it will be known that the object reached by
following the 'bar' field of the second parameter will be modified so
that the first two of its floating point numbers are guaranteed to be of
the opposite sign as they were before, and that if they were infinity,
they are now finite.

5. After the method returns, the object referred to by the global
variable 'zab' has 0 as the value of its 'c' field.

Just expressing all of that in a method signature looks interesting
enough. If we start adding abstraction to the type constraints on
objects to support encapsulation (as I think you'd have to do), then
things get even more interesting.

1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.

 

[Jürgen Exner]

David Hopwood wrote:
[...]

There is no such error message listed in 'perldoc perldiag'.
Please quote the actual text of your error message and include the program
that produced this error.
Then people here in CLPM may be able to assist you.

jue

 

[Chris Smith]

1 and 2 are easy enough. 3 to 5 are best expressed as assertions rather
than types.

One of us is missing the other's meaning here. If 3 to 5 were expressed
as assertions rather than types, then the type system would become
incomplete, requiring frequent runtime-checked type ascriptions to
prevent it from becoming impossible to write software. That's not my
idea of a usable language.

 

[David Hopwood]

One of us is missing the other's meaning here. If 3 to 5 were expressed
as assertions rather than types, then the type system would become
incomplete, requiring frequent runtime-checked type ascriptions to
prevent it from becoming impossible to write software. That's not my
idea of a usable language.

Maybe I'm not understanding what you mean by "complete". Of course any
type system of this expressive power will be incomplete (whether or not
it can express conditions 3 to 5), in the sense that it cannot prove all
true assertions about the types of expressions.

So yes, some assertions would need to be checked at runtime (others could be
proven to always hold by a theorem prover).

Why is this a problem? The goal is not to check everything at compile time;
the goal is just to support writing correct programs.

 

[David Hopwood]

David Hopwood wrote:
[...]

There is no such error message listed in 'perldoc perldiag'.
Please quote the actual text of your error message and include the program
that produced this error.
Then people here in CLPM may be able to assist you.

Yes, I'm well aware that most of this thread has been off-topic for c.l.p.m,
but it is no less off-topic for the other groups (except possibly c.l.functional),
and I can't trim the Newsgroups line down to nothing.

Don't you have a newsreader that can mark whole threads that you don't want
to read?

 

[Marshall]

David Hopwood wrote:
[...]

There is no such error message listed in 'perldoc perldiag'.
Please quote the actual text of your error message and include the program
that produced this error.
Then people here in CLPM may be able to assist you.

Yes, I'm well aware that most of this thread has been off-topic for c.l.p..m,
but it is no less off-topic for the other groups (except possibly c.l.functional),
and I can't trim the Newsgroups line down to nothing.

Don't you have a newsreader that can mark whole threads that you don't want
to read?

Sure, or he could just skip over it. Or he could make a simple
request, such as "please trim comp.lang.whatever because it's
off-topic here." But he hasn't done any of these, choosing instead
to drop in with his occasional pointless snarky comments.


Marshall

 

[Chris Smith]

Maybe I'm not understanding what you mean by "complete". Of course any
type system of this expressive power will be incomplete (whether or not
it can express conditions 3 to 5), in the sense that it cannot prove all
true assertions about the types of expressions.

Ah. I meant complete enough to accomplish the goal in this subthread,
which was to ensure that the compiler knows when a particular int
variable is guaranteed to be greater than 18, and when it is not.

 

[Marshall]

Chris Smith schrieb:
For example, I wrote that example using variables of type int. If we
were to suppose that we were actually working with variables of type
Person, then things get a little more complicated. We would need a few
(infinite classes of) derived subtypes of Person that further constrain
the possible values for state. For example, we'd need types like:

Person{age:{18..29}}

But this starts to look bad, because we used to have this nice
property called encapsulation. To work around that, we'd need to
make one of a few choices: [...] (c) invent some kind of generic
constraint language so that constraints like this could be expressed
without exposing field names. [...] Choice (c), though, looks a
little daunting.
That's not too difficult.
Start with boolean expressions.
If you need to check everything statically, add enough constraints that
they become decidable.

I'm not sure I understand. Could you elaborate?

Preconditions/postconditions can express anything you want, and they are
an absolutely natural extensions of what's commonly called a type
(actually the more powerful type systems have quite a broad overlap with
assertions).
I'd essentially want to have an assertion language, with primitives for
type expressions.

Now, I'm not fully up to speed on DBC. The contract specifications,
these are specified statically, but checked dynamically, is that
right? In other words, we can consider contracts in light of
inheritance, but the actual verification and checking happens
at runtime, yes?

Wouldn't it be possible to do them at compile time? (Although
this raises decidability issues.) Mightn't it also be possible to
leave it up to the programmer whether a given contract
was compile-time or runtime?

I've been wondering about this for a while.


Marshall

 

[Marcin 'Qrczak' Kowalczyk]

It arranges that the expression "b" after that line (barring further
changes) has type int{16..16}, which would make the later call to
signContract illegal.

The assignment might be performed in a function called there, so it's
not visible locally.

Propagating constraints from conditionals is not applicable to mutable
variables, at least not easily.

I think that constant bounds are not very useful at all. Most ranges
are not known statically, e.g. a variable can span the size of an
array.

 

[David Hopwood]

Ah. I meant complete enough to accomplish the goal in this subthread,
which was to ensure that the compiler knows when a particular int
variable is guaranteed to be greater than 18, and when it is not.

I don't think that placing too much emphasis on any individual example is
the right way of thinking about this. What matters is that, over the range
of typical programs written in the language, the value of the increased
confidence in program correctness outweighs the effort involved in both
adding annotations, and understanding whether any remaining run-time checks
are guaranteed to succeed.

Look at it this way: suppose that I *need* to verify that a program has
no range errors. Doing that entirely manually would be extremely tedious.
If the compiler can do, say, 90% of the work, and point out the places that
need to be verified manually, then that would be both less tedious, and
less error-prone.

 

[Chris Smith]

I don't think that placing too much emphasis on any individual example is
the right way of thinking about this. What matters is that, over the range
of typical programs written in the language, the value of the increased
confidence in program correctness outweighs the effort involved in both
adding annotations, and understanding whether any remaining run-time checks
are guaranteed to succeed.

Are you really that short on people to disagree with?

In this particular branch of this thread, we were discussing George's
objection that it would be ridiculous for a type system to check that a
variable should be greater than 18. There is no such thing as placing
too much emphasis on what we were actually discussing. If you want to
discuss something else, feel free to post about it. Why does it bother
you that I'm considering George's point?

 

[Chris Smith]

The assignment might be performed in a function called there, so it's
not visible locally.

Indeed, I pointed that out a few messages ago. That doesn't mean it's
impossible, but it does mean that it's more difficult. Eventually, the
compiler will have to stop checking something, somewhere. It certainly
doesn't, though, have to stop at the first functional abstraction it
comes to. The ways that a function modifies the global application
state certainly ought to be considered part of the visible API of that
function, and if we could reasonably express that in a type system, then
that's great! Granted, designing such a type system for an arbitrary
imperative language seems a little scary.

Propagating constraints from conditionals is not applicable to mutable
variables, at least not easily.

Certainly it worked in the code from my original response to George.
Regardless of whether it might not work in more complex scenarios (and I
think it could, though it would be more challenging), it still doesn't
seem reasonable to assert that the technique is not applicable. If the
type system fails, then it fails conservatively as always, and some
programmer annotation and runtime check is needed to enforce the
condition.

I think that constant bounds are not very useful at all. Most ranges
are not known statically, e.g. a variable can span the size of an
array.

I think you are overestimating the difficulties here. Specialized
language already exist that reliably (as in, all the time) move array
bounds checking to compile time; that means that there exist at least
some languages that have already solved this problem. Going back to my
handy copy of Pierce's book again, he claims that range checking is a
solved problem in theory, and the only remaining work is in how to
integrate it into a program without prohibitive amounts of type
annotation.

 

[Darren New]

Now, I'm not fully up to speed on DBC. The contract specifications,
these are specified statically, but checked dynamically, is that
right?

Yes, but there's a bunch more to it than that. The handling of
exceptions, an in particular exceptions caused by failed pre/post
conditions, is an integral part of the process.

Plus, of course, pre/post condition checking is turned off while
checking pre/post conditions. This does make sense if you think about it
long enough, but it took me several months before I realized why it's
necessary theoretically rather than just practically.

Wouldn't it be possible to do them at compile time?

For some particularly simple ones, yes. For others, like "the chess
pieces are in a position it is legal to get to from a standard opening
set-up", it would be difficult. Anything to do with I/O is going to be
almost impossible to write a checkable postcondition for, even at
runtime. "After this call, the reader at the other end of the socket
will receive the bytes in argument 2 without change."

As far as I understand it, Eiffel compilers don't even make use of
postconditions to optimize code or eliminate run-time checks (like null
pointer testing).

 

[Darren New]

The assignment might be performed in a function called there, so it's
not visible locally.

In Hermes, which actually does this sort of constraint propagation, you
don't have the ability[1] to munge some other routine's[2] local
variables, so that becomes a non-issue. You wind up with some strange
constructs, tho, like an assignment statement that copies and a
different assignment statement that puts the rvalue into the variable on
the left while simultaneously destroying whatever variable held the rvalue.


[1] You do. Just not in a way visible to the programmer. The compiler
manages to optimize out most places that different names consistantly
refer to the same value.

[2] There aren't subroutines. Just processes, with their own address
space, to which you send and receive messages.

 

[Darren New]

Specialized
language already exist that reliably (as in, all the time) move array
bounds checking to compile time;

It sounds like this means the programmer has to code up what it means to
index off an array, yes? Otherwise, I can't imagine how it would work.

x := read_integer_from_stdin();
write_to_stdout(myarray[x]);

What does the programmer have to do to implement this semantic in the
sort of language you're talking about? Surely something somewhere along
the line has to "fail" (for some meaning of failure) at run-time, yes?

 

[Marshall]

Going back to my
handy copy of Pierce's book again, he claims that range checking is a
solved problem in theory, and the only remaining work is in how to
integrate it into a program without prohibitive amounts of type
annotation.

This is in TAPL? Or ATTPL? Can you cite it a bit more specifically?
I want to reread that.


Marshall

 

[George Neuner]

What matters is that, over the range
of typical programs written in the language, the value of the increased
confidence in program correctness outweighs the effort involved in both
adding annotations, and understanding whether any remaining run-time checks
are guaranteed to succeed.

Agreed, but ...

Look at it this way: suppose that I *need* to verify that a program has
no range errors. Doing that entirely manually would be extremely tedious.
If the compiler can do, say, 90% of the work, and point out the places that
need to be verified manually, then that would be both less tedious, and
less error-prone.

All of this presupposes that you have a high level of confidence in
the compiler. I've been in software development for going in 20 years
now and worked 10 years on high performance, high availability
systems. In all that time I have yet to meet a compiler ... or
significant program of any kind ... that is without bugs, noticeable
or not.

I'm a fan of static typing but the major problem I have with complex
inferencing (in general) is the black box aspect of it. That is, when
the compiler rejects my code, is it really because a) I was stupid, b)
the types are too complex, or c) the compiler itself has a bug. It's
certainly true that the vast majority of my problems are because I'm
stupid, but I've run into actual compiler bugs far too often for my
liking (high performance coding has a tendency to uncover them).

I think I understand how to implement HM inferencing ... I haven't
actually done it yet, but I've studied it and I'm working on a toy
language that will eventually use it. But HM itself is a toy compared
to an inferencing system that could realistically handle some of the
problems that were discussed in this and Xah's "expressiveness" thread
(my own beef is with *static* checking of range narrowing assignments
which I still don't believe can be done regardless of Chris Smith's
assertions to the contrary).

It seems to me that the code complexity of such a super-duper
inferencing system would make its bug free implementation quite
difficult and I personally would be less inclined to trust a compiler
that used it than one having a less capable (but easier to implement)
system.

George

 

[Chris Smith]

This is in TAPL? Or ATTPL? Can you cite it a bit more specifically?
I want to reread that.

It's TAPL. On further review, I may have done more interpretation than
I remembered. In particular, the discussion is limited to array bounds
checking, though I don't see a fundamental reason why it wouldn't extend
to other kinds of range checking against constant ranges as we've been
discussing here.

Relevant sections are:

Page 7 footnote: Mentions other challenges such as tractability that
seem more fundamental, but those are treated as trading off against
complexity of annotations; in other words, if we didn't require so many
annotations, then it might become computationally intractable. The next
reference better regarding tractability.

Section 30.5, pp. 460 - 465: Gives a specific example of a language
(theoretical) developed to use limited dependent types to eliminate
array bounds checking. There's a specific mention there that it can be
made tractable because the specific case of dependent types needed for
bounds checking happens to have efficient algorithms, although dependent
types are intractable in the general case.

I'm afraid that's all I've got. I also have come across a real-life
(though not general purpose) languages that does bounds checking
elimination via these techniques... but I can't find them now for the
life of me. I'll post if I remember what it is, soon.

 

[David Hopwood]

Agreed, but ...


All of this presupposes that you have a high level of confidence in
the compiler. I've been in software development for going in 20 years
now and worked 10 years on high performance, high availability
systems. In all that time I have yet to meet a compiler ... or
significant program of any kind ... that is without bugs, noticeable
or not.

That's a good point. I don't think it would be an exaggeration to say
that the some of the most commonly used compilers are riddled with bugs.
gcc is a particularly bad offender, and at the moment seems to be introducing
bugs with each new version at a faster rate than they can be fixed. Sun's
javac also used to be poor in this respect, although I haven't used recent
versions of it.

One of the main reasons for this, IMHO, is that many compilers place too
much emphasis on low-level optimizations of dubious merit. For C and
Java, I've taken to compiling all non-performance-critical code without
optimizations, and that has significantly reduced the number of compiler
bugs that I see. It has very little effect on overall execution performance
(and compile times are quicker).

I don't think that over-complex type systems are the cause of more than a
small part of the compiler bug problem. In my estimation, the frequency of
bugs in different compilers *for the same language* can vary by an order of
magnitude.

I'm a fan of static typing but the major problem I have with complex
inferencing (in general) is the black box aspect of it. That is, when
the compiler rejects my code, is it really because a) I was stupid, b)
the types are too complex, or c) the compiler itself has a bug.

Rejecting code incorrectly is much less of a problem than accepting it
incorrectly. *If* all compiler bugs were false rejections, I would say that
this would not be too much of an issue.

Unfortunately there are plenty of bugs that result in silently generating
bad code. But I don't think you can avoid that by using a language with a
simpler type system. The quality of a compiler depends much more on the
competence and attitudes of the language implementation developers, than
it does on the language itself.

[Although, choosing a language with a more quality-conscious compiler
development team doesn't necessarily help if it is compiling to C, since
then you still have to deal with C compiler bugs, but on autogenerated
code :-(.]

It's certainly true that the vast majority of my problems are because
I'm stupid, but I've run into actual compiler bugs far too often for my
liking (high performance coding has a tendency to uncover them).

Yes. Cryptographic algorithms, and autogenerated code also tend to do that.

I think I understand how to implement HM inferencing ... I haven't
actually done it yet, but I've studied it and I'm working on a toy
language that will eventually use it. But HM itself is a toy compared
to an inferencing system that could realistically handle some of the
problems that were discussed in this and Xah's "expressiveness" thread
(my own beef is with *static* checking of range narrowing assignments
which I still don't believe can be done regardless of Chris Smith's
assertions to the contrary).

It seems to me that the code complexity of such a super-duper
inferencing system would make its bug free implementation quite
difficult and I personally would be less inclined to trust a compiler
that used it than one having a less capable (but easier to implement)
system.

I don't think that the complexity of such a system would need to be
any greater than that of the optimization frameworks used by many
compilers. IIUC, what Chris Smith is suggesting is essentially equivalent
to doing type inference on the SSA form of the program.

 

[Joachim Durchholz]

Now, I'm not fully up to speed on DBC. The contract specifications,
these are specified statically, but checked dynamically, is that
right?

That's how it's done in Eiffel, yes.

In other words, we can consider contracts in light of
inheritance, but the actual verification and checking happens
at runtime, yes?

Sure. Though, while DbC gives rules for inheritance (actually subtypes),
these are irrelevant to the current discussion; DbC-minus-subtyping can
still be usefully applied.

Wouldn't it be possible to do them at compile time? (Although
this raises decidability issues.)

Exactly, and that's why you'd either uses a restricted assertion
language (and essentially get something that's somewhere between a type
system and traditional assertion); or you'd use some inference system
and try to help it along (not a simple thing either - the components of
such a system exist, but I'm not aware of any system that was designed
for the average programmer).

Mightn't it also be possible to
leave it up to the programmer whether a given contract
was compile-time or runtime?

I'd agree with that, but I'm not sure how well that would hold up in
practice.

Regards,
Jo