What is Expressiveness in a Computer Language

P

Pascal Costanza

Matthias said:
By this definition, all languages are statically typed (by making that
"certain class" the set of all values). Moreover, this "definition",
when read the way you probably wanted it to be read, requires some
considerable stretch to accommodate existing static type systems such
as F_\omega.

Perhaps better: A language is statically typed if its definition
includes (or ever better: is based on) a static type system, i.e., a
static semantics with typing judgments derivable by typing rules.
Usually typing judgmets associate program phrases ("expressions") with
types given a typing environment.

How does your definition exclude the trivial type system in which the
only typing judgment states that every expression is acceptable?


Pascal
 
P

Pascal Costanza

Chris said:
Okay, fair enough. It's certainly possible to use the same sequence of
letters to mean two different things in different contexts. The problem
arises, then, when Torben writes:

: That's not really the difference between static and dynamic typing.
: Static typing means that there exist a typing at compile-time that
: guarantess against run-time type violations. Dynamic typing means
: that such violations are detected at run-time.

This is clearly not using the word "type" to mean two different things
in different contexts. Rather, it is speaking under the mistaken
impression that "static typing" and "dynamic typing" are varieties of
some general thing called "typing." In fact, the phrase "dynamically
typed" was invented to do precisely that. My argument is not really
with LISP programmers talking about types, by which they would mean
approximately the same thing Java programmers mean by "class." My point
here concerns the confusion that results from the conception that there
is this binary distinction (or continuum, or any other simple
relationship) between a "statically typed" and a "dynamically typed"
language.

There is an overlap in the sense that some static type systems cover
only types as sets of values whose correct use could as well be checked
dynamically.

Yes, it's correct that more advanced static type systems can provide
more semantics than that (and vice versa).


Pascal
 
C

Chris Smith

Pascal Costanza said:
How does your definition exclude the trivial type system in which the
only typing judgment states that every expression is acceptable?

It is not necessary to exclude that trivial type system. Since it is
useless, no one will implement it. However, if pressed, I suppose one
would have to admit that that definition includes a type system that is
just useless.

I do, though, prefer Pierce's definition:

A type system is a tractable syntactic method for proving the
absence of certain program behaviors by classifying phrases
according to the kinds of values they compute.

(Benjamin Pierce, Types and Programming Languages, MIT Press, pg. 1)

Key words include:

- tractable: it's not sufficient to just evaluate the program

- syntactic: types are tied to the kinds of expressions in the language

- certain program behaviors: while perhaps confusing out of context,
there is nowhere in the book a specification of which program
behaviors may be prevented by type systems and which may not. In
context, the word "certain" there is meant to make it clear that type
systems should be able to specifically identify which behaviors they
prevent, and not that there is some universal set.
 
M

Matthias Blume

Pascal Costanza said:
How does your definition exclude the trivial type system in which the
only typing judgment states that every expression is acceptable?

It does not.
 
J

Joe Marshall

Chris said:
Knowing that it'll cause a lot of strenuous objection, I'll nevertheless
interject my plea not to abuse the word "type" with a phrase like
"dynamically typed".

Allow me to strenuously object. The static typing community has its
own set of
terminology and that's fine. However, we Lisp hackers are not used to
this terminology.
It confuses us. *We* know what we mean by `dynamically typed', and we
suspect *you* do, too.

This cleaner terminology eliminates a lot of confusion.

Hah! Look at the archives.
This isn't just a matter of preference in terminology.
No?

If types DON'T mean a compile-time method for proving the
absence of certain program behaviors, then they don't mean anything at
all.

Nonsense.
 
C

Chris Smith

Joe Marshall said:
Allow me to strenuously object. The static typing community has its
own set of
terminology and that's fine. However, we Lisp hackers are not used to
this terminology.
It confuses us. *We* know what we mean by `dynamically typed', and we
suspect *you* do, too.

I know what you mean by types in LISP. The phrase "dynamically typed,"
though, was explicitly introduced as a counterpart to "statically
typed" in order to imply (falsely) that the word "typed" has related
meanings in those two cases. Nevertheless, I did not really object,
since it's long since passed into common usage, until Torben attempted
to give what I believe are rather meaningless definitions to those
words, in terms of some mythical thing called "type violations" that he
seems to believe exist apart from any specific type systems.
(Otherwise, how could you define kinds of type systems in terms of when
they catch type violations?)
Hah! Look at the archives.

I'm not sure what you mean here. You would like me to look at the
archives of which of the five groups that are part of this conversation?
In any case, the confusion I'm referring to pertains to comparison of
languages, and it's already been demonstrated once in the half-dozen or
so responses to this branch of this thread.
Nonsense.

Please accept my apologies for not making the context clear. I tried to
clarify, in my response to Pascal, that I don't mean that the word
"type" can't have any possible meaning except for the one from
programming language type theory. I should modify my statement as
follows:

An attempt to generalize the definition of "type" from programming
language type theory to eliminate the requirement that they are
syntactic in nature yields something meaningless. Any concept of
"type" that is not syntactic is a completely different thing from
static types.

Basically, I start objecting when someone starts comparing "statically
typed" and "dynamically typed" as if they were both varieties of some
general concept called "typed". They aren't. Furthermore, these two
phrases were invented under the misconception that that are. If you
mean something else by types, such as the idea that a value has a tag
indicating its range of possible values, then I tend to think it would
be less confusing to just say "type" and then clarify the meaning it
comes into doubt, rather than adopting language that implies that those
types are somehow related to types from type theory.
 
M

Marshall

Chris said:
Basically, I start objecting when someone starts comparing "statically
typed" and "dynamically typed" as if they were both varieties of some
general concept called "typed". They aren't. Furthermore, these two
phrases were invented under the misconception that that are. If you
mean something else by types, such as the idea that a value has a tag
indicating its range of possible values, then I tend to think it would
be less confusing to just say "type" and then clarify the meaning it
comes into doubt, rather than adopting language that implies that those
types are somehow related to types from type theory.

While I am quite sympathetic to this point, I have to say that
this horse left the barn quite some time ago.


Marshall

PS. Hi Chris!
 
C

Chris Smith

Marshall said:
While I am quite sympathetic to this point, I have to say that
this horse left the barn quite some time ago.

I don't think so. Perhaps it's futile to go scouring the world for uses
of the phrase "dynamic type" and eliminating them. It's not useless to
point out when the term is used in a particularly confusing way, though,
as when it's implied that there is some class of "type errors" that is
strictly a subset of the class of "errors". Terminology is often
confused for historical reasons, but incorrect statements eventually get
corrected.
PS. Hi Chris!

Hi! Where are you posting from these days?
 
D

Dimitri Maziuk

Yet Another Dan sez:

.... Requiring an array index to be an integer is considered a typing
problem because it can be checked based on only the variable itself,
whereas checking whether it's in bounds requires knowledge about the array.

You mean like
subtype MyArrayIndexType is INTEGER 7 .. 11
type MyArrayType is array (MyArrayIndexType) of MyElementType

Dima
 
M

Marshall

Chris said:
I don't think so. Perhaps it's futile to go scouring the world for uses
of the phrase "dynamic type" and eliminating them. It's not useless to
point out when the term is used in a particularly confusing way, though,
as when it's implied that there is some class of "type errors" that is
strictly a subset of the class of "errors". Terminology is often
confused for historical reasons, but incorrect statements eventually get
corrected.

That's fair.

One thing that is frustrating to me is that I really want to build
an understanding of what dynamic typing is and what its
advantages are, but it's difficult to have a productive discussion
on the static vs. dynamic topic. Late binding of every function
invocation: how does that work, what are the implications of that,
what does that buy you?

I have come to believe that the two actually represent
very different ways of thinking about programming. Which
goes a long way to explaining why there are such difficulties
communicating. Each side tries to describe to the other how
the tools and systems they use facilitate doing tasks that
don't exist in the other side's mental model.

Hi! Where are you posting from these days?

I'm mostly on comp.databases.theory, but I also lurk
on comp.lang.functional, which is an awesome group, and
if you're reading Pierce then you might like it too.


Marshall
 
C

Chris F Clark

Chris said:
I don't think so. Perhaps it's futile to go scouring the world for uses
of the phrase "dynamic type" and eliminating them. It's not useless to
point out when the term is used in a particularly confusing way, though,
as when it's implied that there is some class of "type errors" that is
strictly a subset of the class of "errors". Terminology is often
confused for historical reasons, but incorrect statements eventually get
corrected.

Ok, so you (Chris Smith) object to the term "dynamic type". From a
historical perspective it makes sense, perticular in the sense of
tags. A dynamic type system involves associating tags with values and
expresses variant operations in terms of those tags, with certain
disallowed combinations checked (dynamicly) at run-time. 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.

Type errors are the errors caught by ones personal sense of which
annotations are expressible, computable, and useful. Thus, each
person has a distinct sense of which errors can (and/or should) be
staticly caught.

A personal example, I read news using Emacs, which as most readers in
these newsgroups will know is a dialect of lisp that includes
primitives to edit files. Most of emacs is quite robust, perhaps due
to it being lisp. However, some commands (reading news being one of
them) are exceptionally fragile and fail in the most undebuggable
ways, often just complaining about "nil being an invalid argument" (or
"stack overflow in regular expression matcher".)

This is particularly true, when I am composing lisp code. If I write
some lisp code and make a typographical error, the code may appear to
run on some sample case and fail due to a path not explored in my
sample case when applied to real data.

I consider such an error to be a "type error" because I believe if I
used a languages that required more type annotations, the compiler
would have caught my typographical error (and no I'm not making a pun
on type and typographical). Because I do a lot of this--it is easy
enough for me to conjure up a small lisp macro to make some edit that
it is a primary tool in my toolkit, I wish I could make my doing so
more robust. It would not bother me to have to type more to do so. I
simply make too many stupid errors to use emacs lisp as effectively as
I would like.

Now, this has nothing to do with real lisp programming, and so I do
not wish to offend those who do that. However, I personally would
like a staticly typed way of writing macros (and more importantly of
annotating some of the existing emacs code) to remove some of the
fragilities that I experience. I'm not taking avantage of the
exploratory nature of lisp, except in the sense that the exploratory
nature has created lots of packages which mostly work most of the
time.

Now, I will return this group to its much more erudite discussion of
the issue.

Thank you,
-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)
------------------------------------------------------------------------------
 
J

Joe Marshall

Chris said:
I know what you mean by types in LISP. The phrase "dynamically typed,"
though, was explicitly introduced as a counterpart to "statically
typed" in order to imply (falsely) that the word "typed" has related
meanings in those two cases.

They *do* have a related meaning. Consider this code fragment:
(car "a string")

Obviously this code is `wrong' in some way. In static typing terms, we
could say that
we have a type error because the primitive procedure CAR doesn't
operate on strings.
Alternatively, we could say that since Lisp has one universal type (in
static type terms)
the code is correctly statically typed - that is, CAR is defined on all
input, but it's definition is to raise a runtime exception when passed
a string.

But regardless of which way you want to look at it, CAR is *not* going
to perform its usual computation and it is *not* going to return a
value. The reason behind this is that you cannot take the CAR of a
string. A string is *not* a valid argument to CAR. Ask anyone why and
they will tell you `It's the wrong type.'

Both `static typing' and `dynamic typing' (in the colloquial sense) are
strategies to detect this sort of error.
Nevertheless, I did not really object,
since it's long since passed into common usage,

Exactly. And you are far more likely to encounter this sort of usage
outside of a type theorist's convention.

until Torben attempted
to give what I believe are rather meaningless definitions to those
words, in terms of some mythical thing called "type violations" that he
seems to believe exist apart from any specific type systems.

It's hardly mythical. (car "a string") is obviously an error and you
don't need a static type system to know that.
I'm not sure what you mean here. You would like me to look at the
archives of which of the five groups that are part of this conversation?
In any case, the confusion I'm referring to pertains to comparison of
languages, and it's already been demonstrated once in the half-dozen or
so responses to this branch of this thread.

I mean that this has been argued time and time again in comp.lang.lisp
and probably the other groups as well. You may not like the fact that
we say that Lisp is dynamically typed, but *we* are not confused by
this usage. In fact, we become rather confused when you say `a
correctly typed program cannot go wrong at runtime' because we've seen
plenty of runtime errors from code that is `correctly typed'.
Please accept my apologies for not making the context clear. I tried to
clarify, in my response to Pascal, that I don't mean that the word
"type" can't have any possible meaning except for the one from
programming language type theory. I should modify my statement as
follows:

An attempt to generalize the definition of "type" from programming
language type theory to eliminate the requirement that they are
syntactic in nature yields something meaningless. Any concept of
"type" that is not syntactic is a completely different thing from
static types.

Agreed. That is why there is the qualifier `dynamic'. This indicates
that it is a completely different thing from static types.
Basically, I start objecting when someone starts comparing "statically
typed" and "dynamically typed" as if they were both varieties of some
general concept called "typed". They aren't.

I disagree. There is clearly a concept that there are different
varieties of data and they are not interchangable. In some languages,
it is up to the programmer to ensure that mistakes in data usage do not
happen. In other languages, the computer can detect such mistakes and
prevent them. If this detection is performed by syntactic analysis
prior to running the program, it is static typing. Some languages like
Lisp defer the detection until the program is run. Call it what you
want, but here in comp.lang.lisp we tend to call it `dynamic typing'.
Furthermore, these two
phrases were invented under the misconception that that are. If you
mean something else by types, such as the idea that a value has a tag
indicating its range of possible values, then I tend to think it would
be less confusing to just say "type" and then clarify the meaning it
comes into doubt, rather than adopting language that implies that those
types are somehow related to types from type theory.

You may think it would be less confusing, but if you look at the
archives of comp.lang.lisp you would see that it is not.

We're all rubes here, so don't try to educate us with your
high-falutin' technical terms.
 
M

Marshall

Joe said:
They *do* have a related meaning. Consider this code fragment:
(car "a string")
[...]
Both `static typing' and `dynamic typing' (in the colloquial sense) are
strategies to detect this sort of error.

The thing is though, that putting it that way makes it seems as
if the two approaches are doing the same exact thing, but
just at different times: runtime vs. compile time. But they're
not the same thing. Passing the static check at compile
time is universally quantifying the absence of the class
of error; passing the dynamic check at runtime is existentially
quantifying the absence of the error. A further difference is
the fact that in the dynamically typed language, the error is
found during the evaluation of the expression; in a statically
typed language, errors are found without attempting to evaluate
the expression.

I find everything about the differences between static and
dynamic to be frustratingly complex and subtle.

(To be clear, I do know that Joe understands these issues
quite well.)

So I kind of agree with Chris, insofar as I think the terminology
plays a role in obscuring rather than illuminating the differences.

I mean that this has been argued time and time again in comp.lang.lisp
and probably the other groups as well. You may not like the fact that
we say that Lisp is dynamically typed, but *we* are not confused by
this usage. In fact, we become rather confused when you say `a
correctly typed program cannot go wrong at runtime' because we've seen
plenty of runtime errors from code that is `correctly typed'.

Yes; as I said ealier, the horse has left the barn on this one.

The conversation I would *really* like to have is the one where we
discuss what all the differences are, functionally, between the two,
and what the implications of those differences are, without trying
to address which approach is "right" or "better", because those are
dependent on the problem domain anyway, and because I can
make up my own mind just fine about which one I prefer.

The comp.lang.functional and comp.lang.lisp people are probably
two of the smartest groups on usenet. (I do not consider myself
a member of either group.) You wouldn't *think* that conversation
would be *so* hard to have.


Marshall
 
C

Chris Smith

Joe Marshall said:
They *do* have a related meaning. Consider this code fragment:
(car "a string")

My feeling is that this code is obviously wrong. It is so obviously
wrong, in fact, that the majority of automated error detection systems,
if written for Lisp, would probably manage to identify it as wrong at
some point. This includes the Lisp runtime. So far, I haven't
mentioned types.
A string is *not* a valid argument to CAR. Ask anyone why and
they will tell you `It's the wrong type.'

Indeed, they will. We're assuming, of course that they know a little
Lisp... otherwise, it may be entirely reasonable for someone to expect
that (car "a string") is 'a' and (cdr "a string") is " string"... but
I'll ignore that, even though I haven't yet convinced myself that it's
not relevant to why this is colloquially considered a type error.

I believe that in this sense, the 'anyone' actually means "type" in the
sense that you mean "type". The fact that a static type system detects
this error is somewhat coincidental (except for the fact that, again,
any general error-detection scheme worth its salt probably detects this
error), and orthogonal to whether it is considered a type error by our
hypothetical 'anyone'.
Both `static typing' and `dynamic typing' (in the colloquial sense) are
strategies to detect this sort of error.

I will repeat that static typing is a strategy for detecting errors in
general, on the basis of tractable syntactic methods. There are some
types of errors that are easier to detect in such a system than
others... but several examples have been given of problems solved by
static type systems that are not of the colloquial "It's the wrong
type" variety that you mention here. The examples so far have included
detecting division by zero, or array bounds checking. Other type
systems can check dimensionality (correct units).

Another particularly interesting example may be the following from
Ocaml:

let my_sqrt x = if x < 0.0 then None else Some(sqrt(x));;

Then, if I attempt to use my_sqrt in a context that requires a float,
the compiler will complain about a type violation, since the type of the
expression is "float option". So this is a type error *in Ocaml*, but
it's not the kind of thing that gets intuitively classified as a type
error. In fact, it's roughly equivalent to a NullPointerException at
runtime in Java, and few Java programmers would consider a
NullPointerException to be somehow "actually a type error" that the
compiler just doesn't catch. In this case, when the error appears in
Ocaml, it appears to be "obviously" a type error, but that's only
because the type system was designed to catch some class of program
errors, of which this is a member.
It's hardly mythical. (car "a string") is obviously an error and you
don't need a static type system to know that.

Sure. The question is whether it means much to say that it's a "type
error". So far, I'd agree with either of two statements, depending on
the usage of the word "type":

a) Yes, it means something, but Torben's definition of a static type
system was wrong, because static type systems are not specifically
looking for type errors.

or

b) No, "type error" just means "error that can be caught by the type
system", so it is circular and meaningless to use the phrase in defining
a kind of type system.
I mean that this has been argued time and time again in comp.lang.lisp
and probably the other groups as well.

My apologies, then. It has not been discussed so often in any newsgroup
that I followed up until now, though Marshall has now convinced me to
read comp.lang.functional, so I might see these endless discussions from
now on.
In fact, we become rather confused when you say `a
correctly typed program cannot go wrong at runtime' because we've seen
plenty of runtime errors from code that is `correctly typed'.

Actually, I become a little confused by that as well. I suppose it
would be true of a "perfect" static type system, but I haven't seen one
of those yet. (Someone did email me earlier today to point out that the
type system of a specification language called LOTOS supposedly is
perfect in that sense, that every correctly typed program is also
correct, but I've yet to verify this for myself. It seems rather
difficult to believe.)

Unless I suddenly have some kind of realization in the future about the
feasibility of a perfect type system, I probably won't make that
statement that you say confuses you.
Agreed. That is why there is the qualifier `dynamic'. This indicates
that it is a completely different thing from static types.

If we agree about this, then there is no need to continue this
discussion. I'm not sure we do agree, though, because I doubt we'd be
right here in this conversation if we did.

This aspect of being a "completely different thing" is why I objected to
Torben's statement of the form: static type systems detect type
violations at compile time, whereas dynamic type systems detect type
violations at runtime. The problem with that statement is that "type
violations" means different things in the first and second half, and
that's obscured by the form of the statement. It would perhaps be
clearer to say something like:

Static type systems detect some bugs at compile time, whereas
dynamic type systems detect type violations at runtime.

Here's one interesting consequence of the change. It is easy to
recognize that static and dynamic type systems are largely orthogonal to
each other in the sense above. Java, for example (since that's one of
the newsgroups on the distribution list for this thread), restricting
the field of view to reference types for simplicity's sake, clearly has
both a very well-developed static type system, and a somewhat well-
developed dynamic type system. There are dynamic "type" errors that
pass the compiler and are caught by the runtime; and there are errors
that are caught by the static type system. There is indeed considerable
overlap involved, but nevertheless, neither is made redundant. In fact,
one way of understanding the headaches of Java 1.5 generics is to note
that the two different meanings of "type errors" are no longer in
agreement with each other!
We're all rubes here, so don't try to educate us with your
high-falutin' technical terms.

That's not my intention.
 
C

Chris Smith

I said:
Static type systems detect some bugs at compile time, whereas
dynamic type systems detect type violations at runtime.

PS: In order to satisfy the Python group (among others not on the cross-
post list), we'd need to include "duck typing," which fits neither of
the two definitions above. We'd probably need to modify the definition
of dynamic type systems, since most source tend to classify it as a
dynamic type system. It's getting rather late, though, and I don't
intend to think about how to do that.
 
R

Ron Garret

Marshall said:
The conversation I would *really* like to have is the one where we
discuss what all the differences are, functionally, between the two,
and what the implications of those differences are, without trying
to address which approach is "right" or "better", because those are
dependent on the problem domain anyway, and because I can
make up my own mind just fine about which one I prefer.

The comp.lang.functional and comp.lang.lisp people are probably
two of the smartest groups on usenet. (I do not consider myself
a member of either group.) You wouldn't *think* that conversation
would be *so* hard to have.

It's hard to have because there's very little to say, which leaves the
academics without enough to do to try to justify their existence. This
is the long and the short of it:

1. There are mismatches between the desired behavior of code and its
actual behavior. Such mismatches are generally referred to as "bugs" or
"errors" (and, occasionally, "features").

2. Some of those mismatches can be detected before the program runs.
Some can be detected while the program runs. And some cannot be
detected until after the program has finished running.

3. The various techniques for detecting those mismatches impose varying
degrees of burden upon the programmer and the user.

That's it. Everything else, including but not limited to quibbling over
the meaning of the word "type", is nothing but postmodernist claptrap.

IMHO of course.

rg
 
V

Vesa Karvonen

In comp.lang.functional Chris Smith said:
Knowing that it'll cause a lot of strenuous objection, I'll nevertheless
interject my plea not to abuse the word "type" with a phrase like
"dynamically typed". If anyone considers "untyped" to be perjorative,
as some people apparently do, then I'll note that another common term is
"type-free," which is marketing-approved but doesn't carry the
misleading connotations of "dynamically typed." We are quickly losing
any rational meaning whatsoever to the word "type," and that's quite a
shame.
[...]

FWIW, I agree and have argued similarly on many occasions (both on the
net (e.g. http://groups.google.fi/group/comp.programming/msg/ba3ccfde4734313a?hl=fi&)
and person-to-person). The widely used terminology (statically /
dynamically typed, weakly / strongly typed) is extremely confusing to
beginners and even to many with considerable practical experience.

-Vesa Karvonen
 
R

Rob Thorpe

Chris said:
I'm assuming you mean "class" in the general sense, rather than in the
sense of a specific construct of some subset of OO programming
languages.
Yes.

Now I define a class of values called "correct" values. I define these
to be those values for which my program will produce acceptable results.
Clearly there is a defined class of such values: (1) they are
immediately defined by the program's specification for those lines of
code that produce output; (2) if they are defined for the values that
result from any expression, then they are defined for the values that
are used by that expression; and (3) for any value for which correctness
is not defined by (1) or (2), we may define its "correct" values as the
class of all possible values.

I'm not talking about correctness, I'm talking about typing.
Now, by your definition, any language
which provides checking of that property of correctness for values is
latently typed.

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

I said nothing about the values producing correct outputs, or being
correct inputs. I only said that they have types.

What I mean is that each value in the language is defined by two peice
of information, its contents X and its type T.
Of course, there are no languages that assign this
specific class of values; but ANY kind of correctness checking on values
that a language does (if it's useful at all) is a subset of the perfect
correctness checking system above. Apparently, we should call all such
systems "latent type systems".

No, I'm speaking about type checking not correctness.
Can you point out a language that is not
latently typed?

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

If I tell a C program to print out a string but give it a number it
will give an error telling me that the types mismatch where the
variable the number is held in is used to assign to a variable that
must hold a string. Similarly if I have a lisp function that prints
out a string it will also fail when given a number, but it will fail at
a different point, it will fail when the type of the value is examined
and found to be incorrect.
I'm not trying to poke holes in your definition for fun. I am proposing
that there is no fundamental distinction between the kinds of problems
that are "type problems" and those that are not. Types are not a class
of problems; they are a class of solutions.

Exactly. Which is why they are only tangentially associated with
correctness.
Typing is a set of rules put in place to aid correctness, but it is not
a system that attempts to create correctness itself.
Languages that solve
problems in ways that don't assign types to variables are not typed
languages, even if those same problems may have been originally solved
by type systems.

Well, you can think of things that way. But to the rest of the
computing world languages that don't assign types to variables but do
assign them to values are latently typed.
Hence, they don't exist, and the definitions being used here are rather
pointless.

No they aren't, types of data exist even if there is no system in place
to check them. Ask an assembly programmer whether his programs have
string and integers in them and he will probably tell you that they do.
 
A

Andreas Rossberg

Chris said:
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.

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

- Andreas
 
P

Pascal Costanza

Marshall said:
The conversation I would *really* like to have is the one where we
discuss what all the differences are, functionally, between the two,
and what the implications of those differences are, without trying
to address which approach is "right" or "better", because those are
dependent on the problem domain anyway, and because I can
make up my own mind just fine about which one I prefer.

My current take on this is that static typing and dynamic typing are
incompatible, at least in their "extreme" variants.

The simplest examples I have found are this:

- In a statically typed language, you can have variables that contain
only first-class functions at runtime that are guaranteed to have a
specific return type. Other values are rejected, and the rejection
happens at compile time.

In dynamically typed languages, this is impossible because you can never
be sure about the types of return values - you cannot predict the
future. This can at best be approximated.


- In a dynamically typed language, you can run programs successfully
that are not acceptable by static type systems. 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.

(Even without the call to (eval (read)), in Common Lisp the call to
(slot-value p 'address) would raise an exception which gives the user a
chance to fix things and continue from the point in the control flow
where the exception was raised.)

I cannot imagine a static type system which has a chance to predict that
this program can successfully run without essentially accepting all
kinds of programs.

At least, development environments for languages like Smalltalk, Common
Lisp, Java, etc., make use of such program updates to improve
edit-compile-test cycles. However, it is also possible (and done in
practice) to use such program updates to minimize downtimes when adding
new features to deployed systems.


Pascal
 

Ask a Question

Want to reply to this thread or ask your own question?

You'll need to choose a username for the site, which only take a couple of moments. After that, you can post your question and our members will help you out.

Ask a Question

Members online

Forum statistics

Threads
473,744
Messages
2,569,483
Members
44,901
Latest member
Noble71S45

Latest Threads

Top