What is Expressiveness in a Computer Language

[Pascal Costanza]

I reject this comparison. There's much more to it than that. The point
is that the reasoning which programmers perform when working with an
program in a latently-typed language bears many close similiarities to
the purpose and behavior of type systems.

This isn't an attempt to jump on any bandwagons, it's an attempt to
characterize what is actually happening in real programs and with real
programmers. I'm relating that activity to type systems because that is
what it most closely relates to.

[...]

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
the following two forms are equivalent:

(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]

Now compare this with the Scheme specification, especially this section:
http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs-Z-H-6.html#%_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.



Pascal

[1] Yet Common Lisp allows you to write beautiful code, more often than
not especially _because_ of these "weird" conflations, but that's a
different topic.

 

[Pascal Costanza]

Vesa Karvonen wrote:
...

To make the halting problem decidable one would have to do one of two
things: Depend on memory size limits, or have a language that really is
less expressive, at a very deep level, than any of the languages
mentioned in the newsgroups header for this message.

Not quite. See http://en.wikipedia.org/wiki/ACL2


Pascal

 

[Chris Uppal]

Chris Smith wrote:

[me:]

I am trying to understand how the above statement about dynamic types
actually says anything at all. So a dynamic type system is a system of
logic by which, given a program and a path of program execution up to
this point, verifies something. We still haven't defined "something",
though.

That was the point of my first sentence (quoted above). I take it, and I
assumed that you shared my view, that there is no single "the" type system --
that /a/ type system will yield judgements on matters which it has been
designed to judge. So unless we either nominate a specific type system or
choose what judgements we want to make (today) any discussion of types is
necessarily parameterised on the class(es) of <Judgements>. So, I don't --
can't -- say /which/ judgements my "dynamic type systems" will make. They may
be about nullablity, they may be about traditional "type", they may be about
mutability...

When we look at a specific language (and its implementation), then we can
induce the logic(s) that whatever dynamic checks it applies define.
Alternatively we can consider other "dynamic type systems" which we would like
to formalise and mechanise, but which are not built into our language of
choice.

We also haven't defined what happens if that verification
fails.

True, and a good point. But note that it only applies to systems which are
actually implemented in code (or which are intended to be so).

As a first thought, I suggest that a "dynamic type system" should specify a
replacement action (which includes, but is not limited to, terminating
execution). That action is taken /instead/ of the rejected one. E.g. we don't
actually read off the end of the array, but instead a signal is raised. (An
implementation might, in some cases, find it easier to implement the checks by
allowing the operation to fail, and then backtracking to "pretend" that it had
never happened, but that's irrelevant here). The replacement action must -- of
course -- be valid according to the rules of the type system.

Incidentally, using that idea, we get a fairly close analogy to the difference
between strong and weak static type systems. If the "dynamic type system"
doesn't specify a valid replacement action, or if that action is not guaranteed
to be taken, then it seems that the type system or the language implementation
is "weak" in very much the same sort of way as -- say -- the 'C' type system is
weak and/or weakly enforced.

I wonder whether that way of looking at it -- the "error" never happens since
it is replaced by a valid operation -- puts what I want to call dynamic type
systems onto a closer footing with static type systems. Neither allows the
error to occur.

(Of course, /I/ -- the programmer -- have made a type error, but that's
different thing.)

In other words, I think that everything so far is essentially just
defining a dynamic type system as equivalent to a formal semantics for a
programming language, in different words that connote some bias toward
certain ways of looking at possibilities that are likely to lead to
incorrect program behavior. I doubt that will be an attractive
definition to very many people.

My only objections to this are:

a) I /want/ to use the word "type" to describe the kind of reasoning I do (and
some of the mistakes I make)

b) I want to separate the systems of reasoning (whether formal or informal,
static or dynamic, implemented or merely conceptual, and /whatever/ we call 'em
;-) from the language semantics. I have no objection to <some type system>
being used as part of a language specification, but I don't want to restrict
types to that.

In static type system terminology, this quite emphatically does NOT
apply. There may, of course, be undetected bugs, but they are not type
errors. If they were type errors, then they would have been detected,
unless the compiler is broken.

Sorry, I wasn't clear. I was thinking here of my internal analysis (which I
want to call a type system too). Most of what I was trying to say is that I
don't expect a "dynamic type system" to be complete, any more than a static
one. I also wanted to emphasise that I am happy to talk about type systems
(dynamic or not) which have not been implemented as code (so they yield
judgements, and provide a framework for understanding the program, but nothing
in the computer actually checks them for me).

If you are trying to identify a set of dynamic type errors, in a way
that also applies to statically typed languages, then I will read on.

Have I answered that now ? /Given/ a set of operations which I want to forbid,
I would like to say that a "dynamic type system" which prevents them executing
is doing very much the same job as a static type system which stops the code
compiling.

Of course, we can talk about what kinds of operations we want to forbid, but
that seems (to me) to be orthogonal to this discussion. Indeed, the question
of dynamic/static is largely irrelevant to a discussion of what operations we
want to police, except insofar as certain checks might require information
which isn't available to a (feasible) static theorem prover.

-- chris

 

[Anton van Straaten]

I very much agree with the observation that every programmer performs
"latent typing" in his head
Great!

(although Pascal Constanza's seems to have
the opposite opinion).

I'll have to catch up on that.

But I also think that "latently typed language" is not a meaningful
characterisation. And for the very same reason! Since any programming
activity involves latent typing - naturally, even in assembler! - it
cannot be attributed to any language in particular, and is hence
useless to distinguish between them. (Even untyped lambda calculus
would not be a counter-example. If you really were to program in it,
you certainly would think along lines like "this function takes two
chuch numerals and produces a third one".)

Vesa raised a similar objection in his post 'Saying "latently typed
language" is making a category mistake'. I've made some relevant
responses to that post.

I agree that there's a valid point in the sense that latent types are
not a property of the semantics of the languages they're associated with.

But to take your example, I've had the pleasure of programming a little
in untyped lambda calculus. I can tell you that not having tags is
quite problematic. You certainly do perform latent typing in your head,
but without tags, the language doesn't provide any built-in support for
it. You're on your own.

I'd characterize this as being similar to other situations in which a
language has explicit support for some programming style (e.g. FP or
OO), vs. not having such support, so that you have to take steps to fake
it. The style may be possible to some degree in either case, but it's
much easier if the language has explicit support for it.
Dynamically-typed languages provide support for latent typing. Untyped
lambda calculus and assembler don't provide such support, built-in.

However, I certainly don't want to add to confusion about things like
this. I'm open to other ways to describe these things. Part of where
"latently-typed language" comes from is as an alternative to
"dynamically-typed language" -- an alternative with connotations that
I'm suggesting should be more compatible with type theory.

I hear you when you define latently typed languages as those that
support the programmer's latently typed thinking by providing dynamic
tag checks. But in the very same post (and others) you also explain in
length why these tags are far from being actual types. This seems a bit
contradictory to me.

I don't see it as contradictory. Tags are a mechanism. An individual
tag is not a type. But together, tags help check types. More below:

As Chris Smith points out, these dynamic checks are basically a
necessaity for a well-defined operational semantics. You need them
whenever you have different syntactic classes of values, but lack a
type system to preclude interference. They are just an encoding for
differentiating these syntactic classes. Their connection to types is
rather coincidential.

Oooh, I think I'd want to examine that "coincidence" very closely. For
example, *why* do we have different syntactic classes of values in the
first place? I'd say that we have them precisely to support type-like
reasoning about programs, even in the absence of a formal static type
system.

If you're going to talk about "syntactic classes of values" in the
context of latent types, you need to consider how they relate to latent
types. Syntactic classes of values relate to latent types in a very
similar way to that in which static types do.

One difference is that since latent types are not automatically
statically checked, checks have to happen in some other way. That's
what checks of tags are for.

Chris Smith's observation was made in a kind of deliberate void: one in
which the existence of anything like latent types is discounted, on the
grounds that they're informal. If you're willing to acknowledge the
idea of latent types, then you can reinterpret the meaning of tags in
the context of latent types. In that context, tags are part of the
mechanism which checks latent types.

Anton

 

[Andreas Rossberg]

'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

 

[Matthias Blume]

Not quite. See http://en.wikipedia.org/wiki/ACL2

What do you mean "not quite"? Of course, Patricia is absolutely
right. Termination-guaranteeing languages are fundamentally less
expressive than Turing-complete languages. ACL2 was not mentioned in
the newsgroup header.

 

[Pascal Costanza]

What do you mean "not quite"? Of course, Patricia is absolutely
right. Termination-guaranteeing languages are fundamentally less
expressive than Turing-complete languages. ACL2 was not mentioned in
the newsgroup header.

ACL2 is a subset of Common Lisp, and programs written in ACL2 are
executable in Common Lisp. comp.lang.lisp is not only about Common Lisp,
but even if it were, ACL2 would fit.


Pascal

 

[Jürgen Exner]

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

And what does this have to do with Perl? Are you an alter ego of Xha Lee who
spills his 'wisdom' across any newsgroup he can find?

jue

 

[Patricia Shanahan]

ACL2 is a subset of Common Lisp, and programs written in ACL2 are
executable in Common Lisp. comp.lang.lisp is not only about Common Lisp,
but even if it were, ACL2 would fit.

To prove Turing-completeness of ACL2 from Turing-completeness of Common
Lisp you would need to run the reduction the other way round, showing
that any Common Lisp program can be converted to, or emulated by, an
ACL2 program.

Patricia

 

[Matthias Blume]

ACL2 is a subset of Common Lisp, and programs written in ACL2 are
executable in Common Lisp. comp.lang.lisp is not only about Common
Lisp, but even if it were, ACL2 would fit.

So what?

Patricia said "less expressive", you said "subset". Where is the
contradiction?

Perhaps you could also bring up the subset of Common Lisp where the
only legal program has the form:

nil

Obviously, this is a subset of Common Lisp and, therefore, fits
comp.lang.lisp. Right?

Yes, if you restrict the language to make it less expressive, you can
guarantee termination. Some restrictions that fit the bill already
exist. IMHO, it is still wrong to say that "Lisp guaratees
termination", just because there is a subset of Lisp that does.

Matthias

PS: I'm not sure if this language guarantees termination, though.

 

[Pascal Costanza]

To prove Turing-completeness of ACL2 from Turing-completeness of Common
Lisp you would need to run the reduction the other way round, showing
that any Common Lisp program can be converted to, or emulated by, an
ACL2 program.

Sorry, obviously I was far from being clear. ACL2 is not
Turing-complete. All iterations must be expressed in terms of
well-founded recursion.


Pascal

 

[Chris Smith]

Vesa Karvonen wrote:
...

To make the halting problem decidable one would have to do one of two
things: Depend on memory size limits, or have a language that really is
less expressive, at a very deep level, than any of the languages
mentioned in the newsgroups header for this message.

Patricia, perhaps I'm misunderstanding you here. To make the halting
problem decidable is quite a different thing than to say "given a
program, I may be able to prove that it terminates" (so long as you also
acknowledge the implicit other possibility: I also may not be able to
prove it in any finite bounded amount of time, even if it does
terminate!)

The fact that the halting problem is undecidable is not a sufficient
reason to reject the kind of analysis that is performed by programmers
to convince themselves that their programs are guaranteed to terminate.
Indeed, proofs that algorithms are guaranteed to terminate even in
pathological cases are quite common. Indeed, every assignment of a
worst-case time bound to an algorithm is also a proof of termination.

This is, of course, a very good reason to reject the idea that the
static type system for any Turing-complete language could ever perform
this same kind analysis.

 

[Chris Smith]

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.

It's pretty clear to me that there are two different things here. There
is the set of reasoning that is done about programs by programmers.
This may or may not have some subset called "type reasoning", depending
on whether there's a real difference between type reasoning and any
other reasoning about program behavior, or it's just a word that we've
learned from early experience to use in certain rather arbitrary
contexts. In either case, then there are language features that look
sort of type-like which can support that same reasoning about program
behavior.

It is, to me, an interesting question whether those language features
are really intrinsically connected to that form of reasoning about
program behavior, or whether they are just one way of doing it where
others would suffice as well. Clearly, there is some variation in these
supporting language features between languages that have them... for
example, whether there are only a fixed set of type tags, or an infinite
(or logically infinite, anyway) set, or whether the type tags may have
other type tags as parameters, or whether they even exist as tags at all
or as sets of possible behaviors. Across all these varieties, the
phrase "latently typed language" seems to be a reasonable shorthand for
"language that supports the programmer in doing latent-type reasoning".
Of course, there are still problems here, but really only if you share
my skepticism that there's any difference between type reasoning and any
other reasoning that's done by programmers on their programs.

Perhaps, if you wanted to be quite careful about your distinctions, you
may want to choose different words for the two. However, then you run
into that same pesky "you can't choose other people's terminology" block
again.

A programmer, working in any language, whether typed or not, performs
informal reasoning. I think that is fair to say that there is a
correspondence between type theory and such informal reasoning. The
correspondence is like the correspondence between informal and formal
math.

I'd be more careful in the analogy, there. Since type theory (as
applied to programming languages, anyway) is really just a set of
methods of proving arbitrary statements about program behaviors, a
corresponding "informal type theory" would just be the entire set of
informal reasoning by programmers about their programs. That would
agree with my skepticism, but probably not with too many other people.

An example of a form of informal reasoning that (practically) every
programmer does daily is termination analysis.

Or perhaps you agree with my skepticism, here. This last paragraph
sounds like you're even more convinced of it than I am.

 

[Chris Uppal]

Sorry, obviously I was far from being clear. ACL2 is not
Turing-complete. All iterations must be expressed in terms of
well-founded recursion.

How expressive does that end up being for real problems ? I mean obviously in
some sense it's crippling, but how much of a restiction would that be for
non-accademic programming. Could I write an accountancy package in it, or an
adventure games, or a webserver, with not too much more difficulty than in a
similar language without that one aspect to its type system ?

Hmm, come to think of it those all hae endless loops at the outer level, with
the body of the loop being an event handler, so maybe only the handler should
be required to guaranteed to terminate.

-- chris

 

[Joe Marshall]

I want to make sure I understand. I can think of several things
you might mean by this. It could be:
1) I want to run my program, even though I know parts of it
are broken, because I think there are parts that are not broken
and I want to try them out.

I think I mean a little of each of these.

Nearly *every* program I have ever used is buggy, so this is actually a
normal state of affairs even when I'm not debugging or developing.

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.

This statement is interesting, because the conventional wisdom (at
least as I'm used to hearing it) is that it is best to catch bugs
at the *first* possible moment. But I think maybe we're talking
about different continua here. The last last last possible moment
is after the software has shipped to the customer, and I'm pretty
sure that's not what you mean. I think maybe you mean something
more like 2) above.

It is often the case that the proximate cause of a bug is nowhere near
where the fix needs to be applied. This is especially true with the
really hard bugs. A static type system will tell me that there (may)
exist a path through the code that results in an error, but the runtime
check that fails will provide a witness.

 

[Marshall]

David Hopwood wrote:

The term "dynamically typed" is well used and understood. The term
untyped is generally associated with languages that as you put it "have
no memory safety", it is a pejorative term. "Latently typed" is not
well used unfortunately, but more descriptive.

Most of the arguments above describe a static type system then follow
by saying that this is what "type system" should mean, and finishing by
saying everything else should be considered untyped. This seems to me
to be an effort to associate dynamically typed languages with this
perjorative term.

I can believe that someone, somewhere out there might have done
this, but I can't recall ever having seen it. In any event, the
standard
term for memory safety is "safety", not "untyped." Further, anyone
who was interested in actually understanding the issues woudn't
be doing what you describe.

And if you did find someone who was actively doing this I would
say "never attribute to malice what can adequately be explained
by stupidity."


Marshall

 

[Dr.Ruud]

Rob Thorpe schreef:

I would suggest that at least assembly should be referred to as
"untyped".

There are many different languages under the umbrella of "assembly", so
your suggestion is bound to be false.

 

[Marshall]

It does, because it is only a degenerate case. In general, you can have
something like

void f(int x)
{
const int foo = x+1;
//...
}

Now, foo is still immutable, it is a local, but it clearly also varies.

So what then is to be the definition of "variable" if it includes
things that can never vary, because they are only a degenerate
case? Shall it be simply a named value?


Marshall

 

[Joe Marshall]

Hear hear! This is an *excellent* thread. The evangelism is at
rock-bottom
and the open exploration of other people's way of thinking is at what
looks to me like an all-time high.

What are you, some sort of neo-static pseudo-relational
object-disoriented fascist?

 

[Dr.Ruud]

Marshall schreef:

It seems we have languages:
with or without static analysis
with or without runtime type information (RTTI or "tags")
with or without (runtime) safety
with or without explicit type annotations
with or without type inference

Wow. And I don't think that's a complete list, either.

Right. And don't forget that some languages are hybrids in any of those
areas.