What is Expressiveness in a Computer Language

[Rob Thorpe]

Why not?

Well it's really a matter of perspective isn't it. In some cases it
may even be what the programmer intends.

From my perspective I don't expect a large positive number to turn into

a negative one just because I've requested that it be signed. The
behaviour I would expect is that either the variable being set gets the
right number, or an error occurs. I don't care if the reporting is at
runtime or compile time, so long as it can be seen.

--
Anyway, this is a small point. Does the fact that you only disagreed
with me on this point indicate that you agreed with everything else?

.... Only joking I think you and I have irreconcilable views on this
subject.
I think we can agree that value mostly have some sort of type in a
statically typed language. You may say that they have directly have
types, but I can't see how that can be, as far as I can see they have
types only indirectly. This is only a minor point though.

The issue of typing of values vs variables is not practically
meaningless though.

The main problem I find with statically typed programs is that much of
the world outside the program is not statically typed. Library and API
writers in-particular seem to treat static typing carelessly. As a
result it's not generally possible to write a program meaningfully
inside the static type system, as the type systems designers intended.
You're force to break it all over the place with casts etc anyway. And
at every place you break it the possibility of error occurs and flow
from that place into the rest of the program. So, you end up actually
checking the values of variables rather than relying on their types
anyway. And this can be difficult because their values have no
associated information telling you their types.

It's different writing a function deep inside a large program, in this
case data can be cleaned up beforehand. And in this case the static
typing works are intended and becomes more useful.


Anyway, I don't think it would help either of us to continue this
sub-thread any more. Feel free to reply to this post, but I might not
reply back.

Static typing is rather off topic on most of the newsgroups this thread
is in anyway, and I suspect the people in them are getting rather sick
of it.

 

[Andreas Rossberg]

As far as I know, LOTOS is the only
language that *actually* uses abstract data types

Maybe I don't understand what you mean with ADT here, but all languages
with a decent module system support ADTs in the sense it is usually
understood, see ML for a primary example. Classes in most OOPLs are
essentially beefed-up ADTs as well.

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."

Not counting C/C++, I don't know when I last worked with a typed
language that does *not* have this ability... (which is slightly
different from ADTs, btw)

- Andreas

 

[Rob Thorpe]

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.)

Yes, I agree. That does not apply in general though.
In general the value of the variable could be, for example, read from a
file, in which case the compiler may know it's type, but not any more.

I was talking about the general case.

 

[Vesa Karvonen]

[...]

This static vs dynamic type thing reminds me of one article written by
Bjarne Stroustrup where he notes that "Object-Oriented" has become a
synonym for "good". More precisely, it seems to me that both camps
(static & dynamic) think that "typed" is a synonym for having
"well-defined semantics" or being "safe" and therefore feel the need
to be able to speak of their language as "typed" whether or not it
makes sense.

Let me add another complex subtlety, then: the above description misses
an important point, which is that *automated* type checking is not the
whole story. I.e. that compile time/runtime distinction is a kind of
red herring.

I agree. I think that instead of "statically typed" we should say
"typed" and instead of "(dynamically|latently) typed" we should say
"untyped".

In a statically-checked language, people tend to confuse automated
static checking with the existence of types, because they're thinking in
a strictly formal sense: they're restricting their world view to what
they see "within" the language.

That is not unreasonable. You see, you can't have types unless you
have a type system. Types without a type system are like answers
without questions - it just doesn't make any sense.

Then they look at programs in a dynamically-checked language, and see
checks happening at runtime, and they assume that this means that the
program is "untyped".

Not in my experience. Either a *language* specifies a type system or
not. There is little room for confusion. Well, at least unless you
equate "typing" with being "well-defined" or "safe" and go to great
lengths to convince yourself that your program has "latent types" even
without specifying a type system.

It's certainly close enough to say that the *language* is untyped.

Indeed. Either a language has a type system and is typed or has no
type system and is untyped. I see very little room for confusion
here. In my experience, the people who confuse these things are
people from the dynamic/latent camp who wish to see types everywhere
because they confuse typing with safety or having well-defined
semantics.

But a program as seen by the programmer has types: the programmer
performs (static) type inference when reasoning about the program, and
debugs those inferences when debugging the program, finally ending up
with a program which has a perfectly good type scheme. It's may be
messy compared to say an HM type scheme, and it's usually not proved to
be perfect, but that again is an orthogonal issue.

There is a huge hole in your argument above. Types really do not make
sense without a type system. To claim that a program has a type
scheme, you must first specify the type system. Otherwise it just
doesn't make any sense.

Mathematicians operated for thousands of years without automated
checking of proofs, so you can't argue that because a
dynamically-checked program hasn't had its type scheme proved correct,
that it somehow doesn't have types. That would be a bit like arguing
that we didn't have Math until automated theorem provers came along.

No - not at all. First of all, mathematics has matured quite a bit
since the early days. I'm sure you've heard of the axiomatic method.
However, what you are missing is that to prove that your program has
types, you first need to specify a type system. Similarly, to prove
something in math you start by specifying [fill in the rest].

1. "Untyped" is really quite a misleading term, unless you're talking
about something like the untyped lambda calculus. That, I will agree,
can reasonably be called untyped.

Untyped is not misleading. "Typed" is not a synonym for "safe" or
"having well-defined semantics".

So, will y'all just switch from using "dynamically typed" to "latently
typed"

I won't (use "latently typed"). At least not without further
qualification.

-Vesa Karvonen

 

[Dimitri Maziuk]

George Neuner sez:

If the index computation involves wider types it can still produce
illegal index values. The runtime computation of an illegal index
value is not prevented by narrowing subtypes and cannot be statically
checked.

My vague recollection is that no, it won't unless _you_ explicitly code an
unchecked type conversion. But it's been a while.

HTH
Dima

 

[Rob Thorpe]

I don't think dynamic typing is that nebulous. I remember this being
discussed elsewhere some time ago, I'll post the same reply I did then
..
A language is statically typed if a variable has a property - called
it's type - attached to it, and given it's type it can only represent
values defined by a certain class.

A language is latently typed if a value has a property - called it's
type - attached to it, and given it's type it can only represent values
defined by a certain class.

Some people use dynamic typing as a word for latent typing, others use
it to mean something slightly different. But for most purposes the
definition above works for dynamic typing also.

Untyped and type-free mean something else: they mean no type checking
is done.

Since people have found some holes in this definition I'll have another
go:-

Firstly, a definition, General expression (gexpr) are variables
(mutable or immutable), expressions and the entities functions return.

A statically typed language has a parameter associated with each gexpr
called it's type. The code may test the type of a gexpr. The language
will check if the gexprs of an operator/function have types that match
what is required, to some criteria of sufficiency. It will emit an
error/warning when they don't. It will do so universally.

A latently typed language has a parameter associated with each value
called it's type. The code may test the type of a value. The language
may check if the gexprs of an operator/function have types that match
what is required, to some criteria of sufficiency. It will not
necessarily do so universally.

An untyped language is one that does not possess either a static or
latent type system. In an untyped language gexprs possess no type
information, and neither do values.

 

[Vesa Karvonen]

Darren New wrote: [...]

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."

Not counting C/C++, I don't know when I last worked with a typed
language that does *not* have this ability... (which is slightly
different from ADTs, btw)

Would Java count?

-Vesa Karvonen

 

[Andreas Rossberg]

Would Java count?

Yes, you are right. And there certainly are more in the OO camp.

But honestly, I do not remember when I last had to actively work with
one of them, including Java...

- Andreas

 

[Rob Thorpe]

I agree. I think that instead of "statically typed" we should say
"typed" and instead of "(dynamically|latently) typed" we should say
"untyped".


That is not unreasonable. You see, you can't have types unless you
have a type system. Types without a type system are like answers
without questions - it just doesn't make any sense.


Not in my experience. Either a *language* specifies a type system or
not. There is little room for confusion. Well, at least unless you
equate "typing" with being "well-defined" or "safe" and go to great
lengths to convince yourself that your program has "latent types" even
without specifying a type system.

The question is: What do you mean by "type system"?
Scheme and Lisp both define how types work in their specifications
clearly, others may do too, I don't know.
Of-course you may not consider that as a type system if you mean "type
system" to mean a static type system.

Indeed. Either a language has a type system and is typed or has no
type system and is untyped. I see very little room for confusion
here. In my experience, the people who confuse these things are
people from the dynamic/latent camp who wish to see types everywhere
because they confuse typing with safety or having well-defined
semantics.

No. It's because the things that we call latent types we use for the
same purpose that programmers of static typed languages use static
types for.

Statically typed programmers ensure that the value of some expression
is of some type by having the compiler check it. Programmers of
latently typed languages check, if they think it's important, by asking
what the type of the result is.

The objection here is that advocates of statically typed language seem
to be claiming the "type" as their own word, and asking that others use
their definitions of typing, which are really specific to their
subjects of interest. This doesn't help advocates of static languages/
latently typed languages, or anyone else. It doesn't help because
no-one else is likely to change their use of terms, there's no reason
why they would. All that may happen is that users of statically typed
languages change the words they use. This would confuse me, for one. I
would much rather understand what ML programmers, for example, are
saying and that's hard enough as it is.

There's also my other objection, if you consider latently typed
languages untyped, then what is assembly?

 

[Darren New]

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

I don't know of any others in actual use. Could you name a couple?

Note that I don't consider things like usual OO languages (Eiffel,
Smalltalk, etc) to have "abstract data types".

 

[Darren New]

Maybe I don't understand what you mean with ADT here, but all languages
with a decent module system support ADTs in the sense it is usually
understood, see ML for a primary example.

OK. Maybe some things like ML and Haskell and such that I'm not
intimately familiar with do, now that you mention it, yes.

Classes in most OOPLs are essentially beefed-up ADTs as well.

Err, no. There's nothing really abstract about them. And their values
are mutable. So while one can think about them as an ADT, one actually
has to write code to (for example) calculate or keep track of how many
entries are on a stack, if you want that information.

Not counting C/C++, I don't know when I last worked with a typed
language that does *not* have this ability... (which is slightly
different from ADTs, btw)

Java? C#? Icon? Perl? (Hmmm... Pascal does, IIRC.) I guess you just work
with better languages than I do.

 

[Andreas Rossberg]

OK. Maybe some things like ML and Haskell and such that I'm not
intimately familiar with do, now that you mention it, yes.

Well, Modula and CLU already had this, albeit in restricted form.

Err, no. There's nothing really abstract about them. And their values
are mutable. So while one can think about them as an ADT, one actually
has to write code to (for example) calculate or keep track of how many
entries are on a stack, if you want that information.

Now you lost me completely. What has mutability to do with it? And the
stack?

AFAICT, ADT describes a type whose values can only be accessed by a
certain fixed set of operations. Classes qualify for that, as long as
they provide proper encapsulation.

Java? C#? Icon? Perl? (Hmmm... Pascal does, IIRC.) I guess you just work
with better languages than I do.

OK, I admit that I exaggerated slightly. Although currently I'm indeed
able to mostly work with the more pleasant among languages.

(Btw, Pascal did not have it either, AFAIK)

- Andreas

 

[David Hopwood]

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.

But one that is at least two hundred years old [*], and so unlikely to be
fixed now.

In any case, the intent of this usage (in both mathematics and programming)
is that different *instances* of a variable can be associated with different
values.

[*] introduced by Leibniz, according to <http://members.aol.com/jeff570/v.html>,
but that was presumably in Latin. The first use of "variable" as a noun
recorded by the OED in written English is in 1816.

 

[Rob Thorpe]

Marshall schreef:


C has union.

That's not the same thing. The value of a union in C can be any of a
set of specified types. But the program cannot find out which, and the
language doesn't know either.

With C++ and Java dynamic types the program can test to find the type.

 

[Darren New]

AFAICT, ADT describes a type whose values can only be accessed by a
certain fixed set of operations.

No. AFAIU, an ADT defines the type based on the operations. The stack
holding the integers 1 and 2 is the value (push(2, push(1, empty()))).
There's no "internal" representation. The values and operations are
defined by preconditions and postconditions.

Both a stack and a queue could be written in most languages as "values
that can only be accessed by a fixed set of operations" having the same
possible internal representations and the same function signatures.
They're far from the same type, because they're not abstract. The part
you can't see from outside the implementation is exactly the part that
defines how it works.

Granted, it's a common mistake to write that some piece of C++ code
implements a stack ADT.

For example, an actual ADT for a stack (and a set) is shown on
http://www.cs.unc.edu/~stotts/danish/web/userman/umadt.html
Note that the "axia" for the stack type completely define its operation
and semantics. There is no other "implementation" involved. And in LOTOS
(which uses ACT.1 or ACT.ONE (I forget which)) as its type, this is
actually how you'd write the code for a stack, and then the compiler
would crunch a while to figure out a corresponding implementation.

I suspect "ADT" is by now so corrupted that it's useful to use a
different term, such as "algebraic type" or some such.

Classes qualify for that, as long as they provide proper encapsulation.
Nope.

OK, I admit that I exaggerated slightly. Although currently I'm indeed
able to mostly work with the more pleasant among languages.

Yah.

(Btw, Pascal did not have it either, AFAIK)

I'm pretty sure in Pascal you could say

Type Apple = Integer; Orange = Integer;
and then vars of type apple and orange were not interchangable.

 

[Dr.Ruud]

Rob Thorpe schreef:

Dr.Ruud:

That's not the same thing.

That is your opinion. In the context of this discussion I don't see any
problem to put C's union under "dynamic types".

The value of a union in C can be any of a
set of specified types. But the program cannot find out which, and
the language doesn't know either.

With C++ and Java dynamic types the program can test to find the type.

When such a test is needed for the program with the union, it has it.

 

[Chris Smith]

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).

So the compiler now attempts to prove theorems about the program, but
once it has done so it uses the results merely to optimize its runtime
behavior and then throws the results away. I'd call that not a
statically typed language, then. The type-checking behavior is actually
rather irrelevant both to the set of valid programs of the language, and
to the language semantics (since the same could be accomplished without
the type checking). It is only relevant to performance. Obviously, the
language probably qualifies as dynamically typed for most common
definitions of that term, but I'm not ready to accept one definition and
claim to understand it, yet, so I'll be cautious about classsifying the
language.

The compiler might actually refuse to compile type-incorrect programs,
depending on compiler flags and/or declarations in the code.

Then those compiler flags would cause the compiler to accept a different
language, and that different language would be a statically typed
language (by which I don't mean to exclude the possibility of its also
being dynamically typed).

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

So my answer is that it's not statically typed in the first case, and is
statically typed in the second case, and it intuitively appears to be
dynamically typed at least in the first, and possibly in the second as
well.

 

[Chris Smith]

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.

Really? I can see that in a strong enough static type system, many
dynamic typing features would become unobservable and therefore would be
pragmatically excluded from any probable implementations... but I don't
see any other kind of mutual exclusion between the two.

 

[Joe Marshall]

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.

Agreed. That's why I've been biting my tongue and avoiding posting.
The discussion is going along the lines of the blind men and the
elephant. I've seen about seven different definitions of what a `type'
is, and most of the arguments seem to come from people misunderstanding
the other person's definition. I think that *most* of the people
arguing here would agree with each other (possibly in detail) if only
they understood each other.

Static type aficionados have a specialized jargon that has precise
meaning for a number of the terms being used. People that aren't into
that field of computer science use the same terms in a much looser
sense. But static type aficionados are definitely in the minority in
comp.lang.lisp, and probably in a few of the other comp.langs as well.

What we need is an FAQ entry for how to talk about types with people
who are technically adept, but non-specialists. Or alternatively, an
FAQ of how to explain the term `dynamic typing' to a type theorist.

 

[Marshall]

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

What prohibits us from describing an abstract type as a set of values?

There were papers observing this as early as 1970.
References?


(There are also theoretic problems with the types-as-sets view, because
sufficiently rich type systems can no longer be given direct models in
standard set theory. For example, first-class polymorphism would run
afoul the axiom of foundation.)

There is no reason why we must limit ourselves to "standard set theory"
any more than we have to limit ourselves to standard type theory.
Both are progressing, and set theory seems to me to be a good
choice for a foundation. What else would you use?

(Agree with the rest.)


Marshall