What is Expressiveness in a Computer Language

[Anton van Straaten]

rossberg at ps.uni-sb.de wrote:
> 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