What is Expressiveness in a Computer Language

[Joachim Durchholz]

And so conflating the two notions of type (-checking) as a kind of category
error ? If so then I see what you mean, and it's a useful distinction, but am
unconvinced that it's /so/ helpful a perspective that I would want to exclude
other perspectives which /do/ see the two as more-or-less trivial variants on
the same underlying idea.

It is indeed helpful.
Just think of all the unit tests that you don't have to write.

Regards,
Jo

 

[Rob Thorpe]

It is no different from any other compiler, really. If the compiler
sees the literal 1 in a context that demands type int, then it knows
perfectly well what value that is.

Well, with a literal yes. But with the value of some variable x at
runtime it only know the type because it knows the type of the
variable. Similarly the type of values generated by an expression are
only known because the type the expression generates is known.

Would you?

So, why do you think this "does not make sense"?

Well, it makes sense in terms of the C spec certainly.
It does not make sense in that it does not emit an error.

And, as this example
illustrates, casting in C maps values to values. Depending on the
types of the source and the target, a cast might change the underlying
representation, or it might leave it the same. But it does produce a
value, and the result value is usually not the same as the argument
value, even if the representation is the same.

Yes. I'm not arguing with that.

 

[Joachim Durchholz]

I think you missed my point. My point was that a language is
statically typed IF IT IS DEFINED THAT WAY, i.e., if it has a static
type system that is PART OF THE LANGUAGE DEFINITION. The details are
up to each individual definition.

Well, that certainly makes more sense to me.

Regards,
Jo

 

[Joachim Durchholz]

Static type systems potentially change the semantics of a
language in ways that cannot be captured by dynamically typed languages
anymore, and vice versa.

Very true.

I also suspect that's also why adding type inference to a
dynamically-typed language doesn't give you all the benefits of static
typing: the added-on type system is (usually) too weak to express really
interesting guarantees, usually because the language's semantics isn't
tailored towards making the inference steps easy enough.

Conversely, I suspect that adding dynamic typing to statically-typed
languages tends to miss the most interesting applications, mostly
because all the features that can "simply be done" in a
dynamically-typed language have to be retrofitted to the
statically-typed language on a case-by-case basis.

In both cases, the language designers often don't know the facilities of
the opposed camp well enough to really assess the trade-offs they are doing.

There is, of course, room for research on performing static type checks
in a running system, for example immediately after or before a software
update is applied, or maybe even on separate type checking on software
increments such that guarantees for their composition can be derived.
However, I am not aware of a lot of work in that area, maybe because the
static typing community is too focused on compile-time issues.

I think it's mostly because it's intimidating.

The core semantics of an ideal language fits on a single sheet of paper,
to facilitate proofs of language properties. Type checking
dynamically-loaded code probably wouldn't fit on that sheet of paper.
(The non-core semantics is then usually a set of transformation rules
that map the constructs that the programmer sees to constructs of the
core language.)

Regards,
Jo

 

[Marshall]

When I used the word "type" above, I was adopting the
working definition of a type from the dynamic sense. That is, I'm
considering whether statically typed languages may be considered to also
have dynamic types, and it's pretty clear to me that they do.

I suppose this statement has to be evaluated on the basis of a
definition of "dynamic types." I don't have a firm definition for
that term, but my working model is runtime type tags. In which
case, I would say that among statically typed languages,
Java does have dynamic types, but C does not. C++ is
somewhere in the middle.


Marshall

 

[Marshall]

Hmm... I think this distinction doesn't cover all cases.

Assume a language that
a) defines that a program is "type-correct" iff HM inference establishes
that there are no type errors
b) compiles a type-incorrect program anyway, with an establishes
rigorous semantics for such programs (e.g. by throwing exceptions as
appropriate).
The compiler might actually refuse to compile type-incorrect programs,
depending on compiler flags and/or declarations in the code.

Typed ("strongly typed") it is, but is it statically typed or
dynamically typed?

I think what this highlights is the fact that our existing terminology
is not up to the task of representing all the possible design
choices we could make. Some parts of dynamic vs. static
a mutually exclusive; some parts are orthogonal. Maybe
we have reached the point where trying to cram everything
in two one of two possible ways of doing things isn't going
to cut it any more.

Could it be that the US two-party system has influenced our
thinking?</joke>


Marshall

 

[Matthias Blume]

Well, it makes sense in terms of the C spec certainly.
It does not make sense in that it does not emit an error.

Why not?

 

[David Hopwood]

In a C compiler the compiler has no idea what the values are in the program.
It knows only their type in that it knows the type of the variable they
are contained within.
Would you agree with that?

No. In any language, it may be possible to statically infer that the
value of an expression will belong to a set of values smaller than that
allowed by the expression's type in that language's type system. For
example, all constants have a known value, but most constants have a
type which allows more than one value.

(This is an essential point, not just nitpicking.)

 

[Marshall]

On a semantic level, the tag is always there - it's the type (and
definitely part of an axiomatic definition of the language).
Tag elimination is "just" an optimization.

I see what you're saying, but the distinction is a bit fine for me.
If the language has no possible mechanism to observe the
it-was-only-eliminated-as-an-optimization tag, in what sense
is it "always there?" E.g. The 'C' programming language.


Marshall

 

[Marshall]

Oh, but it *does* make sense to talk about dynamic tagging in a statically
typed language.

That's part of what makes the term "dynamically typed" harmful: it implies
a dichotomy between "dynamically typed" and "statically typed" languages,
when in fact dynamic tagging and static typing are (mostly) independent
features.

That's really coming home to me in this thread: the terminology is *so*
bad. I have noticed this previously in the differences between
structural
and nominal typing; many typing issues associated with this distinction
are falsely labeled as a static-vs-dynamic issues, since so many
statically
type languages are nominally typed.

We need entirely new, finer grained terminology.


Marshall

 

[Dr.Ruud]

Marshall schreef:

"dynamic types." I don't have a firm definition for
that term, but my working model is runtime type tags. In which
case, I would say that among statically typed languages,
Java does have dynamic types, but C does not. C++ is
somewhere in the middle.

C has union.

 

[David Hopwood]

It's worth noting, too, that (in some sense) the type of an object can change
over time[*]. That can be handled readily (if not perfectly) in the informal
internal type system(s) which programmers run in their heads (pace the very
sensible post by Anton van Straaten today in this thread -- several branches
away), but cannot be handled by a type system based on sets-of-values (and is
also a counter-example to the idea that "the" dynamic type of an object/value
can be identified with its tag).

([*] if the set of operations in which it can legitimately partake changes.
That can happen explicitly in Smalltalk (using DNU proxies for instance if the
proxied object changes, or even using #becomeA, but can happen anyway in less
"free" languages -- the State Pattern for instance, or even (arguably) in the
difference between an empty list and a non-empty list).

Dynamic changes in object behaviour are not incompatible with type systems based
on sets of values (e.g. semantic subtyping). There are some tricky issues in
making such a system work, and I'm not aware of any implemented language that
does it currently, but in principle it's quite feasible.

For a type system that can handle dynamic proxying, see
<http://www.doc.ic.ac.uk/~scd/FOOL11/FCM.pdf>.

 

[Joachim Durchholz]

It's worth noting, too, that (in some sense) the type of an object can
change over time[*].

No. Since a type expresses invariants, this is precisely what may *not*
happen.

No. A type is a set of allowable values, allowable operations, and
constraints on the operations (which are often called "invariants" but
they are invariant only as long as the type is invariant).

I very much agree that the association of a type with a value or a name
should be constant over their lifetime - but that doesn't follow from
the definition of "type", it follows from general maintainability
considerations (quite strong ones actually).

Regards,
Jo

 

[Marshall]

Nice post! One question:

3. A really natural term to refer to types which programmers reason
about, even if they are not statically checked, is "latent types". It
captures the situation very well intuitively, and it has plenty of
precedent -- e.g. it's mentioned in the Scheme reports, R5RS and its
predecessors, going back at least a decade or so (haven't dug to check
when it first appeared).

Can you be more explicit about what "latent types" means?
I'm sorry to say it's not at all natural or intuitive to me.
Are you referring to the types in the programmers head,
or the ones at runtime, or what?


Marshall

 

[Marshall]

That's not true. ML has variables in the mathematical sense of
variables -- symbols that can be associated with different values at
different times. What it doesn't have is mutable variables (though it
can get the effect of those by having variables be immutable
references to mutable memory locations).

While we're on the topic of terminology, here's a pet peeve of
mine: "immutable variable."

immutable = can't change
vary-able = can change

Clearly a contradiction in terms.

If you have a named value that cannot be updated, it makes
no sense to call it "variable" since it isn't *able* to *vary.*
Let's call it a named constant.


Marshall

 

[Darren New]

doesn't fit with my intuitions very well -- most noticeably in that the sets
are generally unbounded

Errr, not in Ada. Indeed, not in any machine I know of with a limited
address space.

Indeed, this view is much too narrow. In particular, it cannot explain
abstract types, which is *the* central aspect of decent type systems.

Well, it's Ada's view. I didn't say it was right for theoretical
languages or anything like that. As far as I know, LOTOS is the only
language that *actually* uses abstract data types - you have to use the
equivalent of #include to bring in the integers, for example. Everything
else uses informal rules to say how types work.

But Ada's definition gives you a very nice way of talking about things
like whether integers that overflow are the same type as integers that
don't overflow, or whether an assignment of an integer to a positive is
legal, or adding a CountOfApples to a CountOfOranges is legal, or
whether passing a "Dog" object to an "Animal" function parameter makes
sense in a particular context.

Indeed, the ability to declare a new type that has the exact same
underlying representation and isomorphically identical operations but
not be the same type is something I find myself often missing in
languages. It's nice to be able to say "this integer represents vertical
pixel count, and that represents horizontal pixel count, and you don't
get to add them together."

 

[Andreas Rossberg]

While we're on the topic of terminology, here's a pet peeve of
mine: "immutable variable."

immutable = can't change
vary-able = can change

Clearly a contradiction in terms.

If you have a named value that cannot be updated, it makes
no sense to call it "variable" since it isn't *able* to *vary.*
Let's call it a named constant.

The name of a function argument is a variable. Its denotation changes
between calls. Still it cannot be mutated. Likewise, local "constants"
depending on an argument are not constant.

- Andreas

 

[Andreas Rossberg]

It's worth noting, too, that (in some sense) the type of an object
can change over time[*].

No. Since a type expresses invariants, this is precisely what may
*not* happen.

No. A type is a set of allowable values, allowable operations, and
constraints on the operations (which are often called "invariants" but
they are invariant only as long as the type is invariant).

The purpose of a type system is to derive properties that are known to
hold in advance. A type is the encoding of these properties. A type
varying over time is an inherent contradiction (or another abuse of the
term "type").

- Andreas

 

[Matthias Blume]

While we're on the topic of terminology, here's a pet peeve of
mine: "immutable variable."

immutable = can't change
vary-able = can change

Clearly a contradiction in terms.

No, it is not a contradiction. See the mathematical usage of the word
"variable". Immutable variables can stand for different values at
different times, even without mutation involved, usually because they
are bound by some construct such as lambda.

If you have a named value that cannot be updated, it makes
no sense to call it "variable" since it isn't *able* to *vary.*

Mutation is not the only way for an expression to evaluate to
different values over time.

 

[Matthias Blume]

[ ... ] As far as I know, LOTOS is the only
language that *actually* uses abstract data types - you have to use
the equivalent of #include to bring in the integers, for
example. Everything else uses informal rules to say how types work.

There are *tons* of languages that "actually" facilitate abstract data
types, and some of these languages are actually used by real people.