What is Expressiveness in a Computer Language

[Anton van Straaten]

Joachim Durchholz wrote:
> Anton van Straaten schrieb:
> 
>> Marshall wrote:
>>
>>> Can you be more explicit about what "latent types" means?
>>
>>
>> Sorry, that was a huge omission.  (What I get for posting at 3:30am.)
>>
>> The short answer is that I'm most directly referring to "the types in 
>> the programmer's head".
> 
> 
> Ah, finally that terminology starts to make sense to me. I have been 
> wondering whether there's any useful difference between "latent" and 
> "run-time" typing. (I tend to avoid the term "dynamic typing" because 
> it's overloaded with too many vague ideas.)

Right, that's the reason for using a different term.  Runtime and 
dynamic types are both usually associated with the idea of tagged 
values, and don't address the types of program phrases.

>> there are usually many possible static type schemes that can be 
>> assigned to a given program.
> 
> 
> This seems to apply to latent types as well.

That's what I meant, yes.

> Actually the set of latent types seems to be the set of possible static 
> type schemes.
> Um, well, a superset of these - static type schemes tend to be slightly 
> less expressive than what the programmer in his head. (Most type schemes 
> cannot really express things like "the range of this index variable is 
> such-and-so", and the boundary to general assertions about the code is 
> quite blurry anyway.)

Yes, although this raises the type theory objection of how you know 
something is a type if you haven't formalized it.  For the purposes of 
comparison to static types, I'm inclined to be conservative and stick to 
things that have close correlates in traditional static types.

>> There's a close connection between latent types in the sense I've 
>> described, and the "tagged values" present at runtime.  However, as 
>> type theorists will tell you, the tags used to tag values at runtime, 
>> as e.g. a number or a string or a FooBar object, are not the same 
>> thing as the sort of types which statically-typed languages have.
> 
> 
> Would that be a profound difference, or is it just that annotating a 
> value with a full type expression would cause just too much runtime 
> overhead?

It's a profound difference.  The issue is that it's not just the values 
that need to be annotated with types, it's also other program terms.  In 
addition, during a single run of a program, all it can ever normally do 
is record the types seen on the path followed during that run, which 
doesn't get you to static types of terms.  To figure out the static 
types, you really need to do static analysis.

Of course, static types give an approximation of the actual types of 
values that flow at runtime, and if you come at it from the other 
direction, recording the types of values flowing through terms on 
multiple runs, you can get an approximation to the static type.  Some 
systems use that kind of thing for method lookup optimization.

> In your terminology:
> 
>> So, where do tagged values fit into this?  Tags help to check types at 
>> runtime, but that doesn't mean that there's a 1:1 correspondence 
>> between tags and types.
> 
> 
> Would it be possible to establish such a correspondence, would it be 
> common consensus that such a system should be called "tags" anymore, or 
> are there other, even more profound differences?

There's a non 1:1 correspondence which I gave an example of in the 
quoted message.  For 1:1 correspondence, you'd need to associate types 
with terms, which would need some static analysis.  It might result in 
an interesting program browsing and debugging tool...

Anton