What is Expressiveness in a Computer Language

[Jürgen Exner]

So you claim Java and Objective C are "simply bugs in the theory."

They are certainly off topic in CLPM.

jue

 

[Chris Smith]

It seems to me that most (all ? by definition ??) kinds of reasoning where we
want to invoke the word "type" tend to have a form where we reduce values (and
other things we want to reason about) to equivalence classes[*] w.r.t the
judgements we wish to make, and (usually) enrich that structure with
more-or-less stereotypical rules about which classes are substitutable for
which other ones. So that once we know what "type" something is, we can
short-circuit a load of reasoning based on the language semantics, by
translating into type-land where we already have a much simpler calculus to
guide us to the same answer.

(Or representative symbols, or... The point is just that we throw away the
details which don't affect the judgements.)

One question: is this more specific than simply saying that we use
predicate logic? A predicate divides a set into two subsets: those
elements for which the predicate is true, and those for which it is
false. If we then apply axioms or theorems of the form P(x) -> Q(x),
then we are reasoning from an "equivalence class", throwing away the
details we don't care about (anything that's irrelevant to the
predicate), and applying stereotypical rules (the theorem or axiom). I
don't quite understand what you mean by substituting classes.

 

[Joachim Durchholz]

The immutability comes from the fact (perhaps implicit in these
textbooks, or perhaps they are not really texts on formal type theory)
that types are assigned to expressions,

That doesn't *define* what's a type or what isn't!

If it's impossible to assign types to all expressions of a program in a
language, that does mean that there's no useful type theory for the
program, but it most definitely does not mean that there are no types in
the program.
I can still sensibly talk about sets of values, sets of allowable
operations over each value, and about relationships between inputs and
outputs of these operations.

So programs have types, even if they don't have a static type system.
Q.E.D.

Regards,
Jo

 

[rossberg]

(e-mail address removed)-sb.de writes:

| Gabriel Dos Reis wrote:
| > |
| > | (Unfortunately, you can hardly write interesting programs in any safe
| > | subset of C.)
| >
| > Fortunately, some people do, as living job.
|
| I don't think so. Maybe the question is what a "safe subset" consists
| of. In my book, it excludes all features that are potentially unsafe.

if you equate "unsafe" with "potentially unsafe", then you have
changed gear and redefined things on the fly, and things that could
be given sense before ceases to have meaning. I decline following
such an uncertain, extreme, path.

An unsafe *feature* is one that can potentially exhibit unsafe
behaviour. How else would you define it, if I may ask?

A safe *program* may or may not use unsafe features, but that is not
the point when we talk about safe *language subsets*.

I would suggest you give more thoughts to the claims made in

http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html

Thanks, I am aware of it. Taking into account the hypothetical nature
of the argument, and all the caveats listed with respect to C, I do not
think that it is too relevant for the discussion at hand. Moreover,
Harper talks about a relative concept of "C-safety". I assume that
everybody here understands that by "safe" in this discussion we mean
something else (in particular, memory safety).

Or are you trying to suggest that we should indeed consider C safe for
the purpose of this discussion?

- Andreas

 

[Gabriel Dos Reis]

(e-mail address removed)-sb.de writes:

| Gabriel Dos Reis wrote:
| > |
| > | (Unfortunately, you can hardly write interesting programs in any safe
| > | subset of C.)
| >
| > Fortunately, some people do, as living job.
|
| I don't think so. Maybe the question is what a "safe subset" consists
| of. In my book, it excludes all features that are potentially unsafe.

if you equate "unsafe" with "potentially unsafe", then you have
changed gear and redefined things on the fly, and things that could
be given sense before ceases to have meaning. I decline following
such an uncertain, extreme, path.

| So in particular, C-style pointers are out, because they can easily
| dangle, be uninitialisied, whatever.

sorry, the specific claim I was responding to is not whether *you* can
easily misuse C constructs. I would refrain from generalizing your
inability to write interesting correct programs in C, to a quality of
the language itself. Rather, the claim I was responding to is this:

(Unfortunately, you can hardly write interesting programs in any safe
subset of C.)

I would suggest you give more thoughts to the claims made in

http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html

-- Gaby

 

[rossberg]

So you claim Java and Objective C are "simply bugs in the theory."

You're misquoting me. What I said is that lack of soundness of a
particular type theory (i.e. a language plus type system) is a bug in
that theory.

But anyway, Java in fact is frequently characterised as having a bogus
type system (e.g. with respect to array subtyping). Of course, in a
hybrid language like Java with its dynamic checks it can be argued
either way.

Naturally, the type system of Objective-C is as broken as the one of
plain C.

- Andreas

 

[Joachim Durchholz]

Joachim Durchholz write:

No. I'm not sure about Pascal,

You'd have to use an untagged union type.
It's the standard maneuver in Pascal to get unchecked bitwise
reinterpretation.
Since it's an undefined behavior, you're essentially on your own, but in
practice, any compilers that implemented a different semantics were
hammered with bug reports until they complied with the standard - in
this case, an unwritten (and very unofficial) one, but a rather
effective one.

but (Standard) ML surely has none.
NLFFI?

Same with Haskell as defined by its spec.

Um... I'm not 100% sure, but I dimly (mis?)remember having read that
UnsafePerformIO also offered some ways to circumvent the type system.

(Not that this would be an important point anyway.)

OCaml has a couple of clearly
marked unsafe library functions, but no unsafe feature in the language
semantics itself.

If there's a library with not-typesafe semantics, then at least that
language implementation is not 100% typesafe.
If all implementations of a language are not 100% typesafe, then I
cannot consider the language itself 100% typesafe.

Still, even Pascal is quite a lot "more typesafe" than, say, C.

Tautology. Every language is "safe unless you use unsafe constructs".

No tautology - the unsafe constructs aren't just typewise unsafe ;-p

That's exactly why I replaced Luca Cardelli's "safe/unsafe"
"typesafe/not typesafe". There was no definition to the original terms
attached, and this discussion is about typing anyway.

(Unfortunately, you can hardly write interesting programs in any safe
subset of C.)

Now that's a bold claim that I'd like to see substantiated.

Huh? There is a huge, fundamental difference: namely whether a type
system is sound or not.

I think you're overstating the case.

In type theory, of course, there's no such things as an "almost typesafe
language" - it's typesafe or it isn't.

In practice, I find no implementation where type mismatches cannot
occur, if only when interfacing with the external world (except if you
cheat by treating everything external as a byte sequence, which is like
saying that all languages have at least a universal ANY type and are
hence statically-typed).
And in those languages that do have type holes, these holes may be more
or less relevant - and it's a *very* broad spectrum here.
And from that perspective, if ML indeed has no type hole at all, then
it's certainly an interesting extremal point, but I still have a
relevant spectrum down to assembly language.

Regards,
Jo

 

[Joachim Durchholz]

I don't think so. Maybe the question is what a "safe subset" consists
of. In my book, it excludes all features that are potentially unsafe.

Unless you define "safe", *any* program is unsafe.
Somebody could read the program listing, which could trigger a traumatic
childhood experiece.
(Yes, I'm being silly. But the point is very serious. Even with less
silly examples, whether a language or subset is "safe" entirely depends
on what you define to be "safe", and these definitions tend to vary
vastly across language communities.)

Regards,
Jo

 

[Joachim Durchholz]

It's also relevant how straightforward it is to distinguish between safe
and unsafe code, how explicit you have to be when you use unsafe code,
how likely it is that you accidentally use unsafe code without being
aware of it, what the generally accepted conventions in a language
community are, etc. pp.

Fully agreed.

 

[Anton van Straaten]

That language is not a subset, if at all, it's the other way round, but
I'd say they are rather incomparable. That is, they are different
languages.

The "subset" characterization is not important for what I'm saying. The
fact that they are different languages is what's important. If you
agree about that, then you can at least understand which language I'm
referring to when I say "latently-typed language".

Besides, many dynamically-typed languages have no formal models, in
which case the untyped formal model I've referred to is just a
speculative construct. The language I'm referring to with
"latently-typed language" is the language that programmers are familiar
with, and work with.

I have to agree.

\sarcasm One step further, and somebody starts calling C a "latently
memory-safe language", because a real programmer "knows" that his code
is in a safe subset... And where he is wrong, dynamic memory page
protection checks will guide him.

That's a pretty apt comparison, and it probably explains how it is that
the software we all use, which relies so heavily on C, works as well as
it does.

But the comparison critiques the practice of operating without static
guarantees, it's not a critique of the terminology.

Anton

 

[Chris Smith]

That doesn't *define* what's a type or what isn't!

I'm sorry if you don't like it, but that's all there is. That's the
point that's being missed here. It's not as if there's this thing
called a type, and then we can consider how it is used by formal type
systems. A type, in formal type theory, is ANY label that is assigned
to expressions of a program for the purpose of making a formal type
system work. If you wish to claim a different use of the word and then
try to define what is or is not a type, then be my guest. However,
formal type theory will still not adopt whatever restrictions you come
up with, and will continue to use the word type as the field has been
using the word for a good part of a century now.

The first step toward considering the similarities and differences
between the different uses of "type" in dynamic type systems and formal
type theory is to avoid confusing aspects of one field with the other.

 

[Andrew McDonagh]

That doesn't *define* what's a type or what isn't!

If it's impossible to assign types to all expressions of a program in a
language, that does mean that there's no useful type theory for the
program, but it most definitely does not mean that there are no types in
the program.
I can still sensibly talk about sets of values, sets of allowable
operations over each value, and about relationships between inputs and
outputs of these operations.

So programs have types, even if they don't have a static type system.
Q.E.D.

Of course not. Otherwise programs using dynamically typed systems
wouldnt exist.

Regards,
Jo

I haven't read all of this thread, I wonder, is the problem to do with
Class being mistaken for Type? (which is usually the issue)

 

[Marshall]

At the risk of injecting too much irrelevant philosophy into the
discussion, I will with great trepdiation reply.

I agree this is OT, but I'm not sure about the source of trepidation.

First in the abstrtact: No, understanding is approximating.
Agreed.


The world is inherently vague.

Our understanding of the world is vague. The world itself is
not at all vague.

We make false symbolic models of the world which
are consistent, but at some level they do not reflect reality,
Yes...

because reality isn't consistent.
What?!


Only by abtracting away the inherent
infinite amout of subtlety present in the real universe can we come to
comprehensible models.

Sure. (Although I object to "infinite.")

Those models can be consistent, but they are
not the universe. The models in their consistency, prove things which
are not true about the real universe.

Sure, sure, sure. None of these is a reaon to prefer the unsound
over the sound.

Now in the concrete: In my work productivity is ultimately important.
Therefore, we live by the 80-20 rule in numerous variations. One of
ths things we do to achieve productivity is simplify things. In fact,
we are more interested in an unsound simplification that is right 80%
of the time, but takes only 20% of the effort to compute, than a
completely sound (100% right) model which takes 100% of the time to
compute (which is 5 times as long). We are playing the probabilities.

What you are describing is using a precise mathematical function
to approximate a different precise mathematical function. This
argues for the value of approximation functions, which I do not
dispute. But this does not in any way support the idea of vague
trumping precise, informal trumping formal, or unsoundness as
an end in itself.

It's not that we don't respect the sound underpining, the model which
is consistent and establishes certain truths. However, what we want
is the rule of thumb which is far simpler and approximates the sound
model with reasonable accuracy. In particular, we accept two types of
unsoundness in the model. One, we accept a model which gives wrong
answers which are detectable. We code tests to catch those cases, and
use a different model to get the right answer. Two, we accept a model
which gets the right answer only when over-provisioned. for example,
if we know a loop will occassionaly not converge in the n-steps that
it theoretically should, we will run the loop for n+m steps until the
approximation also converges--even if that requires allocating m extra
copies of some small element than are theoretically necessary. A
small waste of a small resource, is ok if it saves a waste of a more
critical resource--the most critical resource of all being our project
timeliness.

Î¥es, I'm quite familiar with modelling, abstraction, approximation,
etc. However nothing about those endevours suggests to me
that unsoundness is any kind of goal.

Marshall's last point:


Flipping one coin to determine an election is not playing the
probabilities correctly. You need a plausible explanation for why the
coin should predict the right answer and a track record of it being
correct. If you had a coin that had correctly predicted the previous
42 presidencies and you had an explanation why the coin was right,
then it would be credible and I would be willing to wager that it
could also predict that the coin could tell us who the 44th president
would be. One flip and no explanation is not sufficient. (And to the
abstract point, to me that is all knowledge is, some convincing amount
of examples and a plausible explanation--anyone who thinks they have
more is appealing to a "knowledge" of the universe that I don't
accept.)

I used a coin toss; I could also have used a psycic hotline. There
is an explanation for why those things work, but the explanation
is unsound.

Look at where that got Russell and Whitehead.

Universal acclaim, such that their names will be praised for
centuries to come?

I'm just trying to be "honest" about that fact and find ways to
compensate for my own failures.

Limitation != failure.


Marshal

 

[Chris Smith]

I haven't read all of this thread, I wonder, is the problem to do with
Class being mistaken for Type? (which is usually the issue)

Hi Andrew!

Not much of this thread has to do with object oriented languages... so
the word "class" would be a little out of place. However, it is true
that the word "type" is being used in the dynamically typed sense to
include classes from class-based OO languages (at least those that
include run-time type features), as well as similar concepts in other
languages. Some of us are asking for, and attempting to find, a formal
definition to justify this concept, and are so far not finding it.
Others are saying that the definition is somehow implicitly
psychological in nature, and therefore not amenable to formal
definition... which others (including myself) find rather unacceptable.

I started out insisting that "type" be used with its correct formal
definition, but I'm convinced that was a mistake. Asking someone to
change their entire terminology is unlikely to succeed. I'm now
focusing on just trying to represent the correct formal definition of
types in the first place, and make it clear when one or the other
meaning is being used.

Hopefully, that's a fair summary of the thread to date.

 

[Andrew McDonagh]

Hi Andrew!

Hi Chris

Not much of this thread has to do with object oriented languages... so
the word "class" would be a little out of place.

Glad to here.

However, it is true
that the word "type" is being used in the dynamically typed sense to
include classes from class-based OO languages (at least those that
include run-time type features), as well as similar concepts in other
languages. Some of us are asking for, and attempting to find, a formal
definition to justify this concept, and are so far not finding it.
Others are saying that the definition is somehow implicitly
psychological in nature, and therefore not amenable to formal
definition... which others (including myself) find rather unacceptable.

I started out insisting that "type" be used with its correct formal
definition, but I'm convinced that was a mistake. Asking someone to
change their entire terminology is unlikely to succeed. I'm now
focusing on just trying to represent the correct formal definition of
types in the first place, and make it clear when one or the other
meaning is being used.

Hopefully, that's a fair summary of the thread to date.

Cheers much appreciated!

Andrew

 

[George Neuner]

No type theory is needed.
Assume that the wide index type goes into a function and the result is
assigned to a variable fo the narrow type, and it's instantly clear that
the problem is undecidable.

Yes ... the problem is undecidable and that can be statically checked.
But the result is that your program won't compile even if it can be
proved at runtime that an illegal value would never be possible.

Undecidability can always be avoided by adding annotations, but of
course that would be gross overkill in the case of index type widening.

Just what sort of type annotation will convince a compiler that a
narrowing conversion which could produce an illegal value will, in
fact, never produce an illegal value?

[Other than "don't check this" of course.]

George

 

[rossberg]

Um... I'm not 100% sure, but I dimly (mis?)remember having read that
UnsafePerformIO also offered some ways to circumvent the type system.

Neither NLFFI nor unsafePerformIO are official part of the respective
languages. Besides, foreign function interfaces are outside a language
by definition, and can hardly be taken as an argument - don't blame
language A that unsafety arises when you subvert it by interfacing with
unsafe language B on a lower level.

No tautology - the unsafe constructs aren't just typewise unsafe ;-p

That's exactly why I replaced Luca Cardelli's "safe/unsafe"
"typesafe/not typesafe". There was no definition to the original terms
attached, and this discussion is about typing anyway.

The Cardelli paper I was referring to discusses it in detail. And if
you look up the context of my posting: it was exactly whether safety is
to be equated with type safety.

I think you're overstating the case.

In type theory, of course, there's no such things as an "almost typesafe
language" - it's typesafe or it isn't.

Right, and you were claiming to argue from a type-theoretic POV.

[snipped the rest]

- Andreas

 

[Darren New]

Also: has subtyping polymorphism or not, has parametric polymorphism or
not.

And covariant or contravariant.

 

[Marshall]

Not at all. Almost all subprograms provably terminate (with a fairly
easy proof), even if they use general recursion or iteration.

Well, um, hmmm. If a subprogram uses recursion, and it is not
structural recursion, then I don't know how to go about proving
it terminates. Are the proof-termination techniques I don't
know about?

If we can specify a total order on the domain or some
subcomponents of the domain, and show that recursive
calls are always invoked with arguments less than (by
the order) those of the parent call, (and the domain is
well founded) then we have a termination proof.

(If we don't use recursion at all, and we only invoke
proven-terminating functions, same thing; actually
this is a degenerate case of the above.)

For iteration? Okay, a bounded for-loop is probably easy,
but a while loop? What about a function that calculates
the next prime number larger than its argument? Do we
have to embed a proof of an infinity of primes somehow?
That seems burdensome.

If it were not the case that almost all functions provably terminate,
then the whole idea would be hopeless.

I agree!

If a subprogram F calls G, then
in order to prove that F terminates, we probably have to prove that G
terminates. Consider a program where only half of all subprograms are
annotated as provably terminating. In that case, we would be faced with
very many cases where the proof cannot be discharged, because an
annotated subprogram calls an unannotated one.

Right, and you'd have to be applying the non-terminating annotation
all over the place.

If, on the other hand, more than, say, 95% of subprograms provably
terminate, then it is much more likely that we (or the inference
mechanism) can easily discharge any particular proof involving more
than one subprogram. So provably terminating should be the default,
and other cases should be annotated.

Well, I can still imagine that the programmer doesn't care to have
non-termination examined for every part of his code. In which case,
he would still be required to add annotations even when he doesn't
care about a particular subprograms lack of a termination proof.

The pay-for-it-only-if-you-want-it approach has some benefits.
On the other hand, if it really is as common and easy as you
propose, then annotating only when no proof is available is
perhaps feasible.

I'm still a bit sceptical, though.

I do not know how well such a type system would work in practice; it may
be that typical programs would involve too many non-trivial proofs. This
is something that would have to be tried out in a research language.

Yeah.


Marshall

 

[Chris Smith]

Just what sort of type annotation will convince a compiler that a
narrowing conversion which could produce an illegal value will, in
fact, never produce an illegal value?

The annotation doesn't make the narrowing conversion safe; it prevents
the narrowing conversion from happening. If, for example, I need to
subtract two numbers and all I know is that they are both between 2 and
40, then I only know that the result is between -38 and 38, which may
contain invalid array indices. However, if the numbers were part of a
pair, and I knew that the type of the pair was <pair of numbers, 2
through 40, where the first number is greater than the second>, then I
would know that the difference is between 0 and 38, and that may be a
valid index.

Of course, the restrictions on code that would allow me to retain
knowledge of the form [pair of numbers, 2 through 40, a > b] may be
prohibitive. That is an open question in type theory, as a matter of
fact; whether types of this level of power may be inferred by any
tractable procedure so that safe code like this may be written without
making giving the development process undue difficulty by requiring ten
times as much type annotations as actual code. There are attempts that
have been made, and they don't look too awfully bad.