What is Expressiveness in a Computer Language

[Andreas Rossberg]

Chris Uppal wrote:
>>>
>>>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