Discussion:
What is Expressiveness in a Computer Language
(too old to reply)
Joachim Durchholz
2006-06-14 18:55:40 UTC
Permalink
For example,
if you have to code everything as natural numbers, untyped pure lambda
calculus or S-expressions, there is a good chance that you can get
nonsense past the compiler.
Also past peer review and/or debugging runs. And, most importantly, past
your own mental review processes.

Regards,
Jo
Marshall
2006-06-25 20:02:45 UTC
Permalink
A type system that required an annotation on all subprograms that do not
provably terminate, OTOH, would not impact expressiveness at all, and would
be very useful.
Interesting. I have always imagined doing this by allowing an
annotation on all subprograms that *do* provably terminate. If
you go the other way, you have to annotate every function that
uses general recursion (or iteration if you swing that way) and that
seems like it might be burdensome.
Not at all. Almost all subprograms provably terminate (with a fairly
easy proof), even if they use general recursion or iteration.
Well, um, hmmm. If a subprogram uses recursion, and it is not
structural recursion, then I don't know how to go about proving
it terminates. Are the proof-termination techniques I don't
know about?

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

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

For iteration? Okay, a bounded for-loop is probably easy,
but a while loop? What about a function that calculates
the next prime number larger than its argument? Do we
have to embed a proof of an infinity of primes somehow?
That seems burdensome.
If it were not the case that almost all functions provably terminate,
then the whole idea would be hopeless.
I agree!
If a subprogram F calls G, then
in order to prove that F terminates, we probably have to prove that G
terminates. Consider a program where only half of all subprograms are
annotated as provably terminating. In that case, we would be faced with
very many cases where the proof cannot be discharged, because an
annotated subprogram calls an unannotated one.
Right, and you'd have to be applying the non-terminating annotation
all over the place.
If, on the other hand, more than, say, 95% of subprograms provably
terminate, then it is much more likely that we (or the inference
mechanism) can easily discharge any particular proof involving more
than one subprogram. So provably terminating should be the default,
and other cases should be annotated.
Well, I can still imagine that the programmer doesn't care to have
non-termination examined for every part of his code. In which case,
he would still be required to add annotations even when he doesn't
care about a particular subprograms lack of a termination proof.

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

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


Marshall
David Hopwood
2006-06-21 23:01:36 UTC
Permalink
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.
Well, it strikes me that some of what the dynamic camp likes
is the actual *absence* of declared types, or the necessity
of having them.
So why aren't they happy with something like, say, Alice ML, which is
statically typed, but has a "dynamic" type and type inference? I mean
this as a serious question.
At the very least, requiring types vs. not requiring
types is mutually exclusive.
Right, but it's pretty well established that languages that don't
require type *declarations* can still be statically typed.
--
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
Marshall
2006-06-22 16:55:59 UTC
Permalink
In this simple example,
the static case is better, but this is not free, and the cost
of the static case is evident elsewhere, but maybe not
illuminated by this example.
Ugh, please forgive my ham-fisted use of the word "better."
Let me try again:

In this simple example, the static case is provides you with
a guarantee of type safety, but this is not free, and the
cost of the static case may be evident elsewhere, even
if not illuminated by this example.


Marshall
David Hopwood
2006-06-25 21:36:10 UTC
Permalink
Huh? There is a huge, fundamental difference: namely whether a type
system is sound or not. A soundness proof is obligatory for any serious
type theory, and failure to establish it simply is a bug in the theory.
So you claim Java and Objective C are "simply bugs in the theory."
Java's type system was unsound for much of its life. I think that supports
the point that it's inadequate to simply "wish and hope" for soundness,
and that a proof should be insisted on.
--
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
Joe Marshall
2006-06-20 17:09:01 UTC
Permalink
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.
I think we do agree.

The issue of `static vs. dynamic types' comes up about twice a year in
comp.lang.lisp It generally gets pretty heated, but eventually people
come to understand what the other person is saying (or they get bored
and drop out of the conversation - I'm not sure which). Someone always
points out that the phrase `dynamic types' really has no meaning in the
world of static type analysis. (Conversely, the notion of a `static
type' that is available at runtime has no meaning in the dynamic
world.) Much confusion usually follows.

You'll get much farther in your arguments by explaining what you mean
in detail rather than attempting to force a unification of teminology.
You'll also get farther by remembering that many of the people here
have not had much experience with real static type systems. The static
typing of C++ or Java is so primitive that it is barely an example of
static typing at all, yet these are the most common examples of
statically typed languages people typically encounter.
David Hopwood
2006-06-21 04:29:40 UTC
Permalink
[...] NOW that being said, I think
that the reason I like Haskell, a very strongly typed language, is that
because of it's type system, the language is able to do things like
lazy evaluation, [...]
Lazy evaluation does not depend on, nor is it particularly helped by
static typing (assuming that's what you mean by "strongly typed" here).

An example of a non-statically-typed language that supports lazy evaluation
is Oz. (Lazy functions are explicitly declared in Oz, as opposed to Haskell's
implicit lazy evaluation, but that's not because of the difference in type
systems.)
--
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
David Hopwood
2006-06-24 23:06:58 UTC
Permalink
2) I want to run my program, even though it is broken, and I
want to run right up to a broken part and trap there, so I can
use the runtime facilities of the language to inspect what's
going on.
I do this quite often. Sometimes I'll develop `in the debugger'. I'll
change some piece of code and run the program until it traps. Then,
without exiting the debugger, I'll fix the immediate problem and
restart the program at the point it trapped. This technique takes a
bit of practice, but if you are working on something that's complex and
has a lot of state, it saves a lot of time because you don't have to
reconstruct the state every time you make a change.
The problem with this is that from that point on, what you're running
is neither the old nor the new program, since its state may have been
influenced by the bug before you corrected it.

I find it far simpler to just restart the program after correcting
anything. If this is too difficult, I change the design to make it
less difficult.
Wow, interesting.
(I say the following only to point out differing strategies of
development, not to say one or the other is right or bad or
whatever.)
I occasionally find myself doing the above, and when I do,
I take it as a sign that I've screwed up. I find that process
excruciating, and I do everything I can to avoid it. Over the
years, I've gotten more and more adept at trying to turn
as many bugs as possible into type errors, so I don't have
to run the debugger.
Now, there might be an argument to be made that if I had
been using a dynamic language, the process wouldn't be
As a strawman: suppose there are two broad categories
of mental strategies for thinking about bugs, and people
fall naturally into one way or the other, the way there
are morning people and night people. One group is
drawn to the static analysis, one group hates it.
One group hates working in the debugger, one group
is able to use that tool very effectively and elegantly.
Anyway, it's a thought.
I don't buy this -- or at least, I am not in either group.

A good debugger is invaluable regardless of your attitude to type
systems. Recently I was debugging two programs written to do similar
things in the same statically typed language (C), but where a debugger
could not be used for one of the programs. It took maybe 5 times
longer to find and fix each bug without the debugger, and I found it
a much more frustrating experience.
--
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
Pascal Costanza
2006-06-27 20:57:34 UTC
Permalink
Clearly, in this example, the program
is invoking an operation (division) on values that are not appropriate
(zero for the second argument). Hence, if your definition really is a
definition, then this must qualify.
Here, you are asking more from dynamic type systems than any existing
type system provides. The definition of what is considered to be a type
error and what not is always part of the specification of a type system.
No, I'm not. Were we to follow this path of definition, it would not
require that dynamic type systems catch ALL type errors; only that they
catch some. Not that it matters, though. I am analyzing the logical
consequences of your own definition. If those logical consequences were
impossible to fulfill, that would be an even more convincing reason to
find a new definition. Concepts of fairness don't enter into the
equation.
Yes it does. All static type systems define only a strict subset of all
possible errors to be covered, and leave others as runtime errors. The
same holds for dynamic type systems.
If you want to make a statement instead of the sort you've implied
above... namely that a type error is *any* error that's raised by a type
system, then that's fine. It certainly brings us closer to static
types. Now, though, the task is to define a type system without making
a circular reference to types. You've already rejected the statement
that all runtime errors are type errors, because you specifically reject
the division by zero case as a type error for most languages. What is
that distinction?
I don't need such a distinction. I can just define what is covered by a
type system and what is not. All type systems work that way.
You've got to define something... or, I suppose, just go on using words
without definitions. You claimed to give a definition, though.
I have been led by others to believe that the right way to go in the
dynamic type sense is to first define type errors, and then just call
anything that finds type errors a type system. That would work, but it
would require a type error. You seem to want to push that work off of
the word "type error" and back onto "type system", but that requires
that you define what a type system is.
I didn't know I was supposed to give a definition.
Incidentally, in the case of static type systems, we define the system
(for example, using the definition given from Pierce many times this
thread), and then infer the definition of types and type errors from
there. Because a solid definition has been given first for a type
system without invoking the concepts of types or type errors, this
avoids being circular.
Do you mean this one? "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." This isn't really such a
strong definition because it shifts the problem of what exactly a type
system is to finding a definition for the word "kind".

But if this makes you happy, here is an attempt:

"A dynamic type system is a tractable syntactic method for proving the
absence of certain program behaviors by classifying values according to
their kinds."

Basically, this correlates with the typical approach of using tags to
indicate the type/kind/class of values. And indeed, this is what dynamic
type systems typically do: they check tags associated with values. Other
kinds of runtime errors are not raised because of such checks, but
because of other reasons. Therefore, there is naturally a distinction
between runtime errors that are type errors and those that are not.

I am not convinced that this definition of mine is a lot clearer than
what I have said before, but I am also not convinced that Pierce's
definition is any clearer either. It is merely a characterization of
what static type systems do.

The preciseness comes into play when actually defining a type system:
then you have to give definitions what the errors at runtime are that
you want to prove absent by way of the static type system, give the
typing rules for the type system, and then prove soundness by showing
that the typing rules correlate precisely to the runtime errors in the
first stage. Since you have to map two different views of the same thing
to each other you have to be precise in giving definitions that you can
then successfully use in your proofs.

In dynamic type system, this level of precision is not necessary because
proving that dynamic type errors is what the dynamic type system catches
is trivially true, and most programmers don't care that there is a
distinction between runtime type errors and runtime "other" errors. But
this doesn't mean that this distinction doesn't exist.


Pascal
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
Raffael Cavallaro
2006-06-16 15:37:45 UTC
Permalink
On 2006-06-16 11:29:12 -0400, Raffael Cavallaro
In software like this it isn't worth satisfying a static type checker
because you don't get much of the benefit
anywaytext?Dx?description?text?Dx?fromname
as being able to run and test portions of a program before other parts
are written (forward references to as yet nonexistent functions).
I don't what bizarre key combination I accidentally hit here, but the
original read:

In software like this it isn't worth satisfying a static type checker
because you don't get much of the benefit anyway and it means forgoing
such advantages of dynamic typing as being able to run and test
portions of a program before other parts are written (forward
references to as yet nonexistent functions).
Anton van Straaten
2006-06-25 07:38:53 UTC
Permalink
But since the relevant feature that the languages in question possess is
dynamic tagging, it is more precise and accurate to use that term to
describe them.
So you're proposing to call them dynamically-tagged languages?
Also, dynamic tagging is only a minor help in this respect, as evidenced
by the fact that explicit tag tests are quite rarely used by most programs,
if I'm not mistaken.
It sounds as though you're not considering the language implementations
themselves, where tag tests occur all the time - potentially on every
operation. That's how "type errors" get detected. This is what I'm
referring to when I say that dynamic tags support latent types.

Tags are absolutely crucial for that purpose: without them, you have a
language similar to untyped lambda calculus, where "latent type errors"
can result in very difficult to debug errors, since execution can
continue past errors and produce completely uninterpretable results.
IMHO, the support does not go far enough for it to be
considered a defining characteristic of these languages.
Since tag checking is an implicit feature of language implementations
and the language semantics, it certainly qualifies as a defining
characteristic.
When tag tests are used implicitly by other language features such as
pattern matching and dynamic dispatch, they are used for purposes that are
equally applicable to statically typed and non-(statically-typed) languages.
A fully statically-typed language doesn't have to do tag checks to
detect static type errors.

Latently-typed languages do tag checks to detect latent type errors.

You can take the preceding two sentences as a summary definition for
"latently-typed language", which will come in handy below.
or that languages
that use dynamic tagging are "latently typed". This simply is not a
property of the language (as you've already conceded).
Right. I see at least two issues here: one is that as a matter of
shorthand, compressing "language which supports latent typing" to
"latently-typed language" ought to be fine, as long as the term's
meaning is understood.
If, for the sake of argument, "language which supports latent typing" is
to be compressed to "latently-typed language", then statically typed
languages must be considered also latently typed.
See definition above. The phrase "language which supports latent
typing" wasn't intended to be a complete definition.
After all, statically typed languages support expression and
verification of the "types in the programmer's head" at least as well
as non-(statically-typed) languages do. In particular, most recent
statically typed OO languages use dynamic tagging and are memory safe.
And they support comments ;-)
But they don't use tags checks to validate their static types.

When statically-typed languages *do* use tags, in cases where the static
type system isn't sufficient to avoid them, then indeed, those parts of
the program use latent types, in the exact same sense as more fully
latently-typed languages do. There's no conflict here, it's simply the
case that most statically-typed languages aren't fully statically typed.
This is not, quite obviously, what most people mean when they say
that a particular *language* is "latently typed". They almost always
mean that the language is dynamically tagged, *not* statically typed,
and memory safe. That is how this term is used in R5RS, for example.
The R5RS definition is compatible with what I've just described, because
the parts of a statically-typed language that would be considered
latently-typed are precisely those which rely on dynamic tags.
But beyond that, there's an issue here about the definition of "the
language". When programming in a latently-typed language, a lot of
action goes on outside the language - reasoning about static properties
of programs that are not captured by the semantics of the language.
This is true of programming in any language.
Right, but when you compare a statically-typed language to an untyped
language at the formal level, a great deal more static reasoning goes on
outside the language in the untyped case.

What I'm saying is that it makes no sense, in most realistic contexts,
to think of untyped languages as being just that: languages in which the
type of every term is simply a tagged value, as though no static
knowledge about that value exists. The formal model requires that you
do this, but programmers can't function if that's all the static
information they have. This isn't true in the case of a fully
statically-typed language.
This means that there's a sense in which the language that the
programmer programs in is not the same language that has a formal
semantic definition. As I mentioned in another post, programmers are
essentially mentally programming in a richer language - a language which
has informal (static) types - but the code they write down elides this
type information, or else puts it in comments.
If you consider stuff that might be in the programmer's head as part
of the program, where do you stop? When I maintain a program written
by someone I've never met, I have no idea what was in that programmer's
head. All I have is comments, which may be (and frequently are,
unfortunately) inaccurate.
You have to make the same kind of inferences that the original
programmer made. E.g. when you see a function that takes some values,
manipulates them using numeric operators, and returns a value, you have
to either figure out or trust the comments that the function accepts
numbers (or integers, floats etc.) and returns a number.

This is not some mystical psychological quality: it's something that
absolutely must be done in order to be able to reason about a program at
all.
(Actually, it's worse than that -- if I come back to a program 5 years
later, I probably have little idea what was in my head at the time I
wrote it.)
But that's simply the reality - you have to reconstruct: recover the
latent types, IOW. There's no way around that!

Just to be concrete, I'll resurrect my little Javascript example:

function timestwo(x) { return x*2 }

Assume I wrote this and distributed it in source form as a library, and
now you have to maintain it. How do you know what values to call it
with, or what kind of values it returns? What stops you from calling it
with a string?

Note that according the formal semantics of an untyped language, the
type of that function is "value -> value".

The phrase "in the programmer's head" was supposed to help communicate
the concept. Don't get hung up on it.
We have to accept, then, that the formal semantic definitions of
dynamically-checked languages are incomplete in some important ways.
Referring to those semantic definitions as "the language", as though
that's all there is to the language in a broader sense, is misleading.
Bah, humbug. The language is just the language.
If you want to have this discussion precisely, you have to do better
than that. There is an enormous difference between the formal semantics
of an untyped language, and the (same) language which programmers work
with and think of as "dynamically typed".

Use whatever terms you like to characterize this distinction, but you
can't deny that the distinction exists, and that it's quite a big,
important one.
In this context, the term "latently-typed language" refers to the
language that a programmer experiences, not to the subset of that
language which is all that we're typically able to formally define.
I'm with Marshall -- this is way too mystical for me.
I said more in my reply to Marshall. Perhaps I'm not communicating
well. At worst, what I'm talking about is informal. It's easy to prove
that you can't reason about a program if you don't know what types of
values a function accepts or returns - which is what an untyped formal
model gives you.

Anton
Andreas Rossberg
2006-06-23 13:11:49 UTC
Permalink
Well, it seems to me that you are /assuming/ a notion of what kinds of
logic can be called type (theories), and I don't share your
assumptions. No offence intended.
OK, but can you point me to any literature on type theory that makes a
different assumption?
'Fraid not. (I'm not a type theorist -- for all I know there may be lots, but
my suspicion is that they are rare at best.)
I would suspect the same :-). And the reason is that "type" has a
well-established use in theory. It is not just my "assumption", it is
established practice since 80 or so years. So far, this discussion has
not revealed the existence of any formal work that would provide a
theory of "dynamic types" in the sense it is used to characterise
"dynamically typed" languages.

So what you are suggesting may be an interesting notion, but it's not
what is called "type" in a technical sense. Overloading the same term
for something different is not a good idea if you want to avoid
confusion and misinterpretations.
But, as a sort of half-way, semi-formal, example: consider the type environment
in a Java runtime. The JVM does formal type-checking of classfiles as it loads
them. In most ways that checking is static -- it's treating the bytecode as
program text and doing a static analysis on it before allowing it to run (and
rejecting what it can't prove to be acceptable by its criteria). However, it
isn't /entirely/ static because the collection of classes varies at runtime in
a (potentially) highly dynamic way. So it can't really examine the "whole"
text of the program -- indeed there is no such thing. So it ends up with a
hybrid static/dynamic type system -- it records any assumptions it had to make
in order to find a proof of the acceptability of the new code, and if (sometime
in the future) another class is proposed which violates those assumptions, then
that second class is rejected.
Incidentally, I know this scenario very well, because that's what I'm
looking at in my thesis :-). All of this can easily be handled
coherently with well-established type machinery and terminology. No need
to bend existing concepts and language, no need to resort to "dynamic
typing" in the way Java does it either.
In code which will be executed at instant A
obj aMessage. "type correct"
obj anotherMessage. "type incorrect"
In code which will be executed at instant B
obj aMessage. "type incorrect"
obj anotherMessage. "type correct"
I don't see how a logic with no temporal element can arrive at all four those
judgements, whatever it means by a union type.
I didn't say that the type system cannot have temporal elements. I only
said that a type itself cannot change over time. A type system states
propositions about a program, a type assignment *is* a proposition. A
proposition is either true or false (or undecidable), but it is so
persistently, considered under the same context. So if you want a type
system to capture temporal elements, then these must be part of a type
itself. You can introduce types with implications like "in context A,
this is T, in context B this is U". But the whole quoted part then is
the type, and it is itself invariant over time.

- Andreas
Rob Thorpe
2006-06-20 14:57:41 UTC
Permalink
"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.
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.
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.
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.
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.
Chris Smith
2006-06-26 18:53:42 UTC
Permalink
Of course zero is not appropriate as a second argument to the division
operator! I can't possibly see how you could claim that it is. The
only reasonable statement worth making is that there doesn't exist a
type system in widespread use that is capable of checking this.
...and this is typically not even checked at the stage where type tags
are checked in dynamically-typed languages. Hence, it is not a type
error. (A type error is always what you define to be a type error within
a given type system, right?)
Sure, it's not a type error for that language.
Note, this example was in response to David's reply that my definition
turns every runtime error into a type error. That's not the case, and
that's all I want to say.
But your definition does do that. Your definition of a type error was
when a program attempts to invoke an operation on values that are not
appropriate for this operation. Clearly, in this example, the program
is invoking an operation (division) on values that are not appropriate
(zero for the second argument). Hence, if your definition really is a
definition, then this must qualify.
However, it sounds as
if you're claiming that it wouldn't be possible for the type system to
do this?
No. I only need an example where a certain error is not a type error in
_some_ language. I don't need to make a universal claim here.
Definitions are understood to be statements of the form "if and only
if". They assert that /everything/ that fits the definition is
describable by the word, and /everything/ that doesn't is not
describable by the word. If that's not what you meant, then we are
still in search of a definition.

If you want to make a statement instead of the sort you've implied
above... namely that a type error is *any* error that's raised by a type
system, then that's fine. It certainly brings us closer to static
types. Now, though, the task is to define a type system without making
a circular reference to types. You've already rejected the statement
that all runtime errors are type errors, because you specifically reject
the division by zero case as a type error for most languages. What is
that distinction?
--
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation
Pascal Costanza
2006-06-28 16:14:20 UTC
Permalink
Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.
The whole point of static type systems is to make sure that there are
things that one cannot do. So the fact that there are such things are
not an argument per se against static types.
I am not arguing against static type systems. I am just responding to
the question what the things are that you cannot do in statically typed
languages.
[ ... ]
Beyond that, I am convinced that the ability to update a running
system without the need to shut it down can be an important asset.
And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed.
Maybe. The interesting question then is whether you can express the
kinds of dynamic updates that are relevant in practice. Because a static
type system always restricts what kinds of runtime behavior you can
express in your language. I am still skeptical, because changing the
types at runtime is basically changing the assumptions that the static
type checker has used to check the program's types in the first place.

For example, all the approaches that I have seen in statically typed
languages deal with adding to a running program (say, class fields and
methods, etc.), but not with changing to, or removing from it.
Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it.
...and this creates problems with moving data from one version of a
program to the next.
How does this "create" such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the "replace the code" model
along with a "translate the data where necessary at the time of
replacement". Translating the data, i.e., re-establishing the
invariants expected by the updated/replaced code, seems much harder
(to me) in the case of self-modifying code. Erlang got this one
right.
...and the "translate the date where necessary" approach is essentially
triggered by a dynamic type test (if value x is of an old version of
type T, update it to reflect the new version of type T [1]). QED.


Pascal

[1] BTW, that's also the approach taken in CLOS.
--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/
Paul McGuire
2006-06-09 15:07:23 UTC
Permalink
<I've removed the massive cross-posting - I wouldn't presume this message is
all that interesting to folks in those other NG's, and I'm sure they'd be
saying, "who the heck is Paul McGuire, and who gives a @#*$! what he
thinks?">

"Joe Marshall" <eval.apply at gmail.com> wrote in message
Expressiveness isn't necessarily a good thing. For instance, in C, you
can express the
addresses of variables by using pointers. You cannot express the same
thing in Java, and
most people consider this to be a good idea.
For those who remember the bad old days of COBOL, its claim to fame was that
it was more like English prose, with the intent of making a programming
language that was as readable as English, assuming that this was more
"expressive", and not requiring as much of a mental mapping exercise for
someone trying to "read" a program. Even the language terminology itself
strived for this: statements were "sentences"; blocks were "paragraphs".
The sentence model may have ended up being one of COBOL's Achilles Heel's -
the placement of terminating periods for an IF THEN ELSE block was crucial
for disambiguating which ELSE went with which IF. Unfortunately, periods
are one of the least visible printed characters, and an extra or missing
period could cause hours of extra debugging.

(Of course, at the time of COBOL's inception, the only primary languages to
compare with were assembly or FORTRAN-60, so this idea wasn't totally
unfounded.)

-- Paul
Joachim Durchholz
2006-06-25 17:52:30 UTC
Permalink
Another observation: type safeness is more of a spectrum than a clearcut
distinction. Even ML and Pascal have ways to circumvent the type system,
No. I'm not sure about Pascal,
You'd have to use an untagged union type.
It's the standard maneuver in Pascal to get unchecked bitwise
reinterpretation.
Since it's an undefined behavior, you're essentially on your own, but in
practice, any compilers that implemented a different semantics were
hammered with bug reports until they complied with the standard - in
this case, an unwritten (and very unofficial) one, but a rather
effective one.
but (Standard) ML surely has none.
NLFFI?
Same with Haskell as defined by its spec.
Um... I'm not 100% sure, but I dimly (mis?)remember having read that
UnsafePerformIO also offered some ways to circumvent the type system.

(Not that this would be an important point anyway.)
OCaml has a couple of clearly
marked unsafe library functions, but no unsafe feature in the language
semantics itself.
If there's a library with not-typesafe semantics, then at least that
language implementation is not 100% typesafe.
If all implementations of a language are not 100% typesafe, then I
cannot consider the language itself 100% typesafe.

Still, even Pascal is quite a lot "more typesafe" than, say, C.
and even C is typesafe unless you use unsafe constructs.
Tautology. Every language is "safe unless you use unsafe constructs".
No tautology - the unsafe constructs aren't just typewise unsafe ;-p

That's exactly why I replaced Luca Cardelli's "safe/unsafe"
"typesafe/not typesafe". There was no definition to the original terms
attached, and this discussion is about typing anyway.
(Unfortunately, you can hardly write interesting programs in any safe
subset of C.)
Now that's a bold claim that I'd like to see substantiated.
IOW from a type-theoretic point of view, there is no real difference
between their typesafe and not typesafe languages in the "statically
typed" column; the difference is in the amount of unsafe construct usage
in practial programs.
Huh? There is a huge, fundamental difference: namely whether a type
system is sound or not.
I think you're overstating the case.

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

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

Regards,
Jo
David Hopwood
2006-06-26 22:40:10 UTC
Permalink
While this effort to salvage the term "type error" in dynamic
languages is interesting, I fear it will fail. Either we'll all have
to admit that "type" in the dynamic sense is a psychological concept
with no precise technical definition (as was at least hinted by
Anton's post earlier, whether intentionally or not) or someone is
going to have to propose a technical meaning that makes sense,
independently of what is meant by "type" in a static system.
What about this: You get a type error when the program attempts to
invoke an operation on values that are not appropriate for this
operation.
Examples: adding numbers to strings; determining the string-length of a
number; applying a function on the wrong number of parameters; applying
a non-function; accessing an array with out-of-bound indexes; etc.
This makes essentially all run-time errors (including assertion failures,
etc.) "type errors". It is neither consistent with, nor any improvement
on, the existing vaguely defined usage.
Nope. This is again a matter of getting the levels right.
Consider division by zero: appropriate arguments for division are
numbers, including the zero. The dynamic type check will typically not
check whether the second argument is zero, but will count on the fact
that the processor will raise an exception one level deeper.
That is an implementation detail. I don't see its relevance to the above
argument at all.
This is maybe better understandable in user-level code. Consider the
class Person {
String name;
int age;
void buyPorn() {
if (< this.age 18) throw new AgeRestrictionException();
...
}
}
The message p.buyPorn() is a perfectly valid message send and will pass
both static and dynamic type tests (given p is of type Person in the
static case). However, you will still get a runtime error.
Your definition above was "You get a type error when the program attempts
to invoke an operation on values that are not appropriate for this operation."

this.age, when less than 18, is a value that is inappropriate for the buyPorn()
operation, and so this satisfies your definition of a type error. My point was
that it's difficult to see any kind of program error that would *not* satisfy
this definition.
--
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
David Hopwood
2006-06-24 22:00:54 UTC
Permalink
I think that we're finally getting to the bottom of things. While
reading your reponses something became very clear to me: latent-typing and
latent-types are not a property of languages. Latent-typing, also known as
informal reasoning, is something that all programmers do as a normal part
of programming. To say that a language is latently-typed is to make a
category mistake, because latent-typing is not a property of languages.
I disagree with you and agree with Anton. Here, it is helpful to
understand the history of Scheme a bit: parts of its design are a
reaction to what Schemers perceived as having failed in Common Lisp (and
other previous Lisp dialects).
One particularly illuminating example is the treatment of nil in Common
Lisp. That value is a very strange beast in Common Lisp because it
stands for several concepts at the same time: most importantly the empty
list and the boolean false value. Its type is also "interesting": it is
both a list and a symbol at the same time. It is also "interesting" that
its quoted value is equivalent to the value nil itself. This means that
(if nil 42 4711)
(if 'nil 42 4711)
Both forms evaluate to 4711.
It's also the case that taking the car or cdr (first or rest) of nil
doesn't give you an error, but simply returns nil as well.
The advantage of this design is that it allows you to express a lot of
code in a very compact way. See
http://www.apl.jhu.edu/~hall/lisp/Scheme-Ballad.text for a nice
illustration.
The disadvantage is that it is mostly impossible to have a typed view of
nil, at least one that clearly disambiguates all the cases. There are
also other examples where Common Lisp conflates different types, and
sometimes only for special cases. [1]
http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs-Z-H-6.html#%25_sec_3.2
This clearly deviates strongly from Common Lisp (and other Lisp
dialects). The emphasis here is on a clear separation of all the types
specified in the Scheme standard, without any exception. This is exactly
what makes it straightforward in Scheme to have a latently typed view of
programs, in the sense that Anton describes. So latent typing is a
property that can at least be enabled / supported by a programming
language, so it is reasonable to talk about this as a property of some
dynamically typed languages.
If anything, I think that this example supports my and Vesa's point.
The example demonstrates that languages
*that are not distinguished in whether they are called latently typed*
support informal reasoning about types to varying degrees.
--
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
Marshall
2006-06-23 17:15:56 UTC
Permalink
But, as a sort of half-way, semi-formal, example: consider the type environment
in a Java runtime. The JVM does formal type-checking of classfiles as it loads
them. In most ways that checking is static -- it's treating the bytecode as
program text and doing a static analysis on it before allowing it to run (and
rejecting what it can't prove to be acceptable by its criteria). However, it
isn't /entirely/ static because the collection of classes varies at runtime in
a (potentially) highly dynamic way. So it can't really examine the "whole"
text of the program -- indeed there is no such thing. So it ends up with a
hybrid static/dynamic type system -- it records any assumptions it had to make
in order to find a proof of the acceptability of the new code, and if (sometime
in the future) another class is proposed which violates those assumptions, then
that second class is rejected.
I have to object to the term "hybrid".

Java has a static type system.
Java has runtime tags and tag checks.

The two are distinct, and neither one is less than complete, so
I don't think "hybrid" captures the situation well.


Marshall

Continue reading on narkive:
Loading...