What is Expressiveness in a Computer Language

[Andreas Rossberg]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

Easy, any statically typed language is not latently typed. Values have
no type associated with them, instead variables have types.

A (static) type system assigns types to (all) *expressions*. This
includes values as well as variables.

Don't confuse type assignment with type annotation (which many
mainstream languages enforce for, but also only allow for, variable
declarations).

- Andreas

 

[Rob Thorpe]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?
???

Easy, any statically typed language is not latently typed. Values have
no type associated with them, instead variables have types.

A (static) type system assigns types to (all) *expressions*.

That's right most of the time yes, I probably should have said
expressions. Though I can think of static typed languages where the
resulting type of an expression depends on the type of the variable it
is being assigned to.

This includes values as well as variables.

Well I haven't programmed in any statically typed language where values
have types themselves. Normally the language only knows that variable
Z is of type Q because it's in a variable of type Q, or as you mention
an expression of type Q. There are many things that could be
considered more than one type. The integer 45 could be unsigned 45 or
signed 45 or even float 45 depending on the variable it's in, but
without context it doesn't have a precise type.

It does imply the type to some extent though, you could imagine a
language where every value has a precise type. So, you've found a hole
in my definition.

Maybe a better definition would be:-

if (variables have types || expressions have types) <lang is statically
typed>
else if (values have types) <lang is latently/dynamically typed>
else <lang is untyped>

That seems to fit usage, quite well.

Even then there are problems. Perl has static types for arrays, hashs
and scalars. But scalars themselves can be integers, strings, etc.

Don't confuse type assignment with type annotation (which many
mainstream languages enforce for, but also only allow for, variable
declarations).

Point taken.

 

[Ketil Malde]

I thought the point was to separate the (bitwise) representation of a
value from its interpretation (which is its type). In a static
system, the interpretation is derived from context, in a dynamic
system values must carry some form of tags specifying which
interpretation to use.

I think this applies - conceptually, at least - also to expressions?

My impression is that dynamic typers tend to include more general
properties in their concept of types (div by zero, srqt of negatives,
etc).

-k

 

[Andreas Rossberg]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

That's right most of the time yes, I probably should have said
expressions. Though I can think of static typed languages where the
resulting type of an expression depends on the type of the variable it
is being assigned to.

Yes, but that's no contradiction. A type system does not necessarily
assign *unique* types to individual expressions (consider overloading,
subtyping, polymorphism, etc).

Well I haven't programmed in any statically typed language where values
have types themselves.

They all have - the whole purpose of a type system is to ensure that any
expression of type T always evaluates to a value of type T. So when you
look at type systems formally then you certainly have to assign types to
values, otherwise you couldn't prove any useful property about those
systems (esp. soundness).

- Andreas

 

[Chris Smith]

I'm not talking about correctness, I'm talking about typing.

Since you wrote that, I've come to understand that you meant something
specific by "property" which I didn't understand at first. From my
earlier perspective, it was obvious that correctness was a property of a
value. I now realize that you meant a property that's explicitly
associated with the value and plays a role in determining the behavior
of the language. Sorry for the confusion.

No, that isn't what I said. What I said was:
"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."

No, to answer Andreas' concern, you would only need to say:

... if a value has a property - called it's type - attached to it,
and the language semantics guarantees that only values defined by a
certain class may have that same property attached.

Easy, any statically typed language is not latently typed.

I'm actually not sure I agree with this at all. I believe that
reference values in Java may be said to be latently typed. This is the
case because each reference value (except null, which may be tested
separately) has an explicit property (called its "class", but surely the
word doesn't make any difference), such that the language semantics
guarantees that only a certain class of values may have that same
property, and the property is used to determine behavior of the language
in many cases (for example, in the case of type-based polymorphism, or
use of Java's instanceof operator). Practically all class-based OO
languages are subject to similar consideration, as it turns out.

I'm unsure whether to consider explicitly stored array lengths, which
are present in most statically typed languages, to be part of a "type"
in this sense or not.

 

[David Squire]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

But you left out the most significant part: "given it's type it can only
represent values *defined by a certain class*" (my emphasis). In C-ish
notation:

unsigned int x;

means that x can only represent elements that are integers elements of
the set (class) of values [0, MAX_INT]. Negative numbers and non-integer
numbers are excluded, as are all sorts of other things.

You over-condensed.

DS

NB. This is not a comment on static, latent, derived or other typing,
merely on summarization.

 

[Andreas Rossberg]

No, that isn't what I said. What I said was:
"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."


"it [= a value] [...] can [...] represent values"?


???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

But you left out the most significant part: "given it's type it can only
represent values *defined by a certain class*" (my emphasis).

That qualification does not remove the circularity from the definition.

In C-ish notation:

unsigned int x;

means that x can only represent elements that are integers elements of
the set (class) of values [0, MAX_INT]. Negative numbers and non-integer
numbers are excluded, as are all sorts of other things.

I don't see how that example is relevant, since the above definition
does not mention variables.

- Andreas

 

[Rob Thorpe]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

Yes, but the point is, as the other poster mentioned: values defined by
a class.
For example, in lisp:
"xyz" is a string, #(1 2 3) is an array, '(1 2 3) is a list, 45 is a
fixed-point number.
Each item that can be stored has a type, no item can be stored without
one. The types can be tested. Most dynamic typed languages are like
that.

Compare this to an untyped language where types cannot generally be
tested.

Yes, but that's no contradiction. A type system does not necessarily
assign *unique* types to individual expressions (consider overloading,
subtyping, polymorphism, etc).

That's a fair way of looking at it.

They all have - the whole purpose of a type system is to ensure that any
expression of type T always evaluates to a value of type T.

But it only gaurantees this because the variables themselves have a
type, the values themselves do not. Most of the time the fact that the
variable they are held in has a type infers that the value does too.
But the value itself has no type, in a C program for example I can take
the value from some variable and recast it in any way I feel and the
language cannot correct any errors I make because their is no
information in the variable to indicate what type it is.

So when you
look at type systems formally then you certainly have to assign types to
values, otherwise you couldn't prove any useful property about those
systems (esp. soundness).

Yes, but indirectly.

 

[Ketil Malde]

But it only gaurantees this because the variables themselves have a
type, the values themselves do not.

I think statements like this are confusing, because there are
different interpretations of what a "value" is. I would say that the
integer '4' is a value, and that it has type Integer (for instance).
This value is different from 4 the Int16, or 4 the double-precision
floating point number. From this viewpoint, all values in statically
typed languages have types, but I think you use 'value' to denote the
representation of a datum in memory, which is a different thing.

-k

 

[Andreas Rossberg]

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

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

Yes, but the point is, as the other poster mentioned: values defined by
a class.

I'm sorry, but I still think that the definition makes little sense.
Obviously, a value simply *is* a value, it does not "represent" one, or
several ones, regardless how you qualify that statement.

But it only gaurantees this because the variables themselves have a
type,

No, variables are insignificant in this context. You can consider a
language without variables at all (such languages exist, and they can
even be Turing-complete) and still have evaluation, values, and a
non-trivial type system.

But the value itself has no type

You mean that the type of the value is not represented at runtime? True,
but that's simply because the type system is static. It's not the same
as saying it has no type.

in a C program for example I can take
the value from some variable and recast it in any way I feel and the
language cannot correct any errors I make because their is no
information in the variable to indicate what type it is.

Nothing in the C spec precludes an implementation from doing just that.
The problem with C rather is that its semantics is totally
underspecified. In any case, C is about the worst example to use when
discussing type systems. For starters, it is totally unsound - which is
what your example exploits.

- Andreas

 

[Matthias Blume]

- In a dynamically typed language, you can run programs successfully
that are not acceptable by static type systems.

This statement is false.

For every program that can run successfully to completion there exists
a static type system which accepts that program. Moreover, there is
at least one static type system that accepts all such programs.

What you mean is that for static type systems that are restrictive
enough to be useful in practice there always exist programs which
(after type erasure in an untyped setting, i.e., by switching to a
different language) would run to completion, but which are rejected by
the static type system.

By the way, the parenthetical remark is important: If a language's
definition is based on a static type system, then there are *no*
programs in that language which are rejected by its type checker.
That's trivially so because strings that do not type-check are simply
not considered programs.

Here is an example in Common Lisp:

; A class "person" with no superclasses and with the only field "name":
(defclass person ()
(name))

; A test program:
(defun test ()
(let ((p (make-instance 'person)))
(eval (read))
(slot-value p 'address)))

(slot-value p 'address) is an attempt to access the field 'address in
the object p. In many languages, the notation for this is p.address.

Although the class definition for person doesn't mention the field
address, the call to (eval (read)) allows the user to change the
definition of the class person and update its existing
instances. Therefore at runtime, the call to (slot-value p 'adress)
has a chance to succeed.

I am quite comfortable with the thought that this sort of evil would
get rejected by a statically typed language.

 

[Matthias Blume]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that
a value represents values - which I find a strange and circular
definition.

But you left out the most significant part: "given it's type it can
only represent values *defined by a certain class*" (my emphasis). In
C-ish notation:

unsigned int x;

means that x can only represent elements that are integers elements of
the set (class) of values [0, MAX_INT]. Negative numbers and
non-integer numbers are excluded, as are all sorts of other things.

This x is not a value. It is a name of a memory location.

You over-condensed.

Andreas condensed correctly.

 

[David Squire]

Rob Thorpe wrote:
No, that isn't what I said. What I said was:
"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."
"it [= a value] [...] can [...] represent values"?
???
I just quoted, in condensed form, what you said above: namely, that
a value represents values - which I find a strange and circular
definition.

But you left out the most significant part: "given it's type it can
only represent values *defined by a certain class*" (my emphasis). In
C-ish notation:

unsigned int x;

means that x can only represent elements that are integers elements of
the set (class) of values [0, MAX_INT]. Negative numbers and
non-integer numbers are excluded, as are all sorts of other things.

This x is not a value. It is a name of a memory location.

You over-condensed.

Andreas condensed correctly.

I should have stayed out of this. I had not realised that it had
degenerated to point-scoring off someone typing "value" when it is clear
from context that he meant "variable".

Bye.

DS

 

[Darren New]

Yes, but the point is, as the other poster mentioned: values defined by
a class.

A value can only represent one value, right? Or can a value have
multiple values?

For example, in lisp:
"xyz" is a string,

"xyz" cannot represent values from the class of strings. It can only
represent one value.

I think that's what the others are getting at.

But it only gaurantees this because the variables themselves have a
type, the values themselves do not.

Sure they do. 23.5e3 is a "real" in Pascal, and there's no variable there.

("hello" % "there") is illegal in most languages, because the modulo
operator doesn't apply to strings. How could this be determined at
compile time if "hello" and "there" don't have types?

 

[Matthias Blume]

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

Yes, but the point is, as the other poster mentioned: values defined by
a class.
For example, in lisp:
"xyz" is a string, #(1 2 3) is an array, '(1 2 3) is a list, 45 is a
fixed-point number.
Each item that can be stored has a type, no item can be stored without
one. The types can be tested. Most dynamic typed languages are like
that.

Your "types" are just predicates.

Compare this to an untyped language where types cannot generally be
tested.

You mean there are no predicates in untyped languages?

But it only gaurantees this because the variables themselves have a
type, the values themselves do not.

Of course they do.

Most of the time the fact that the
variable they are held in has a type infers that the value does too.
But the value itself has no type, in a C program for example I can take
the value from some variable and recast it in any way I feel and the
language cannot correct any errors I make because their is no
information in the variable to indicate what type it is.

Casting in C takes values of one type to values of another type.

Yes, but indirectly.

No, this is usually done very directly and very explicitly.

 

[Matthias Blume]

Andreas Rossberg wrote:
Rob Thorpe wrote:
No, that isn't what I said. What I said was:
"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."
"it [= a value] [...] can [...] represent values"?
???
I just quoted, in condensed form, what you said above: namely, that
a value represents values - which I find a strange and circular
definition.

But you left out the most significant part: "given it's type it can
only represent values *defined by a certain class*" (my emphasis). In
C-ish notation:

unsigned int x;

means that x can only represent elements that are integers elements of
the set (class) of values [0, MAX_INT]. Negative numbers and
non-integer numbers are excluded, as are all sorts of other things.

This x is not a value. It is a name of a memory location.

You over-condensed.

Andreas condensed correctly.

I should have stayed out of this. I had not realised that it had
degenerated to point-scoring off someone typing "value" when it is
clear from context that he meant "variable".

If he really had meant "variable" then he would have been completely wrong.

Bye.

Bye.

 

[Chris F Clark]

A static
type system eliminates some set of tags on values by syntactic
analysis of annotations (types) written with or as part of the program
and detects some of the disallowed compuatations (staticly) at compile
time.

Adreas relied:

Explicit annotations are not a necessary ingredient of a type system,
nor is "eliminating tags" very relevant to its function.

While this is true, I disagree at some level with the second part. By
eliminating tags, I mean allowing one to perform "type safe"
computations without requiring the values to be tagged. One could
argue that the tags were never there. However, many of the
interesting polymorphic computations reaquire either that the values
be tagged or that some other process assures that at each point one
can determine apriori what the correct variant of computation is which
applies.

To me a static type system is one which does this apriori
determination. A dynamic type system does not do a apriori and
instead includes explicit information in the values being computed to
select the corret variant computations.

In that sense, a static type system is eliminating tags, because the
information is pre-computed and not explicitly stored as a part of the
computation. Now, you may not view the tag as being there, but in my
mind if there exists a way of perfoming the computation that requires
tags, the tag was there and that tag has been eliminated.

To put it another way, I consider the tags to be axiomatic. Most
computations involve some decision logic that is driven by distinct
values that have previously been computed. The separation of the
values which drive the compuation one-way versus another is a tag.
That tag can potentially be eliminated by some apriori computation.

In what I do, it is very valuable to move information from being
explicitly represented in the computed result into the tag, so that I
often have distinct "types" (i.e. tags) for an empty list, a list with
one element, a list with two elements, and a longer list. In that
sense, I agree with Chris Smith's assertion that "static typing" is
about asserting general properties of the algorithm/data. These
assertions are important to the way I am manipulating the data. They
are part of my type model, but they may not be part of anyone else's,
and to me toe pass a empty list to a function requiring a list with
two elements is a "type error", because it is something I expect the
type system to detect as incorrect. The fact that no one else may
have that expectation does not seem relevant to me.

Now, to carry this farther, since I expect the type system to validate
that certain values are of certain types and only be used in certain
contexts, I am happy when it does not require certain "tags" to be
actualy present in the data. However, because other bits of code are
polymorphic, I do expect certain values to require tags. In the end,
this is still a win for me. I had certain data elements that in the
abstract had to be represented explicitly. I have encoded that
information into the type system and in some cases the type system is
not using any bits in the computed representation to hold that
information. Whenever that happens, I win and that solves one of the
problems that I need solved.

Thus, a type system is a way for me to express certain axioms about my
algorithm. A dynamic type system encodes those facts as part of the
computation. A static type system pre-calculates certain "theorems"
from my axioms and uses those theorems to allow my algorithm to be
computed without all the facts being stored as part of the computation.

Hopefully, this makes my point of view clear.

-Chris

*****************************************************************************
Chris Clark Internet : (e-mail address removed)
Compiler Resources, Inc. Web Site : http://world.std.com/~compres
23 Bailey Rd voice : (508) 435-5016
Berlin, MA 01503 USA fax : (978) 838-0263 (24 hours)
------------------------------------------------------------------------------

 

[Rob Thorpe]

I think statements like this are confusing, because there are
different interpretations of what a "value" is. I would say that the
integer '4' is a value, and that it has type Integer (for instance).
This value is different from 4 the Int16, or 4 the double-precision
floating point number. From this viewpoint, all values in statically
typed languages have types, but I think you use 'value' to denote the
representation of a datum in memory, which is a different thing.

Well I haven't been consistent so far

But I mean the value as the semantics of the program itself sees it.
Which mostly means the datum in memory.

 

[Rob Thorpe]

Rob Thorpe wrote:

No, that isn't what I said. What I said was:
"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."

"it [= a value] [...] can [...] represent values"?

???

I just quoted, in condensed form, what you said above: namely, that a
value represents values - which I find a strange and circular definition.

Yes, but the point is, as the other poster mentioned: values defined by
a class.
For example, in lisp:
"xyz" is a string, #(1 2 3) is an array, '(1 2 3) is a list, 45 is a
fixed-point number.
Each item that can be stored has a type, no item can be stored without
one. The types can be tested. Most dynamic typed languages are like
that.

Your "types" are just predicates.

You can call them predicates if you like. Most people programming in
python, perl, or lisp will call them types though.

You mean there are no predicates in untyped languages?

Well, no there aren't. That's what defines a language as untyped.

Of-course you can make them with your own code, in for example
assembler, but that's outside the language.

Of course they do.

I think we're discussing this at cross-purposes. In a language like C
or another statically typed language there is no information passed
with values indicating their type. Have a look in a C compiler if you
don't believe me. You store 56 in a location in memory then in most
compilers all that will be store is 56, nothing more. The compiler
relys entirely on the types of the variables to know how to correctly
operate on the values. The values themselves have no type information
associated with them.

Casting in C takes values of one type to values of another type.

No it doesn't. Casting reinterprets a value of one type as a value of
another type.
There is a difference. If I cast an unsigned integer 2000000000 to a
signed integer in C on the machine I'm using then the result I will get
will not make any sense.

No, this is usually done very directly and very explicitly.

No it isn't.
If I say "4 is a integer" that is a direct statement about 4.
If I say "X is and integer and X is 4, therefore 4 is an integer" that
is a slightly less direct statement about 4.

The difference in directness is only small, and much more indirectness
is needed to prove anything useful about a system formally.

 

[Darren New]

The compiler
relys entirely on the types of the variables to know how to correctly
operate on the values. The values themselves have no type information
associated with them.

int x = (int) (20.5 / 3);

What machine code operations does the "/" there invoke? Integer
division, or floating point division? How did the variables involved in
the expression affect that?

No it doesn't. Casting reinterprets a value of one type as a value of
another type.

No it doesn't.
int x = (int) 20.5;
There's no point at which bits from the floating point representation
appear in the variable x.

int * x = (int *) 0;
There's nothing that indicates all the bits of "x" are zero, and indeed
in some hardware configurations they aren't.