What is Expressiveness in a Computer Language

[Chris Smith]

Anton van Straaten <anton at appsolutions.com> wrote:
> I'm not trying to call programmer reasoning in general a type system. 
> I'd certainly agree that a programmer muddling his way through the 
> development of a program, perhaps using a debugger to find all his 
> problems empirically, may not be reasoning about anything that's 
> sufficiently close to types to call them that.

Let me be clear, then.  I am far less agreeable than you that this 
couldn't be called a type system.  One of my goals here is to try to 
understand, if we are going to work out what can and can't be called a 
type system in human thought, how we can possible draw a boundary 
between kinds of logic and say that one of them is a type system while 
the other is not.  I haven't seen much of a convincing way to do it.  
The only things that I can see rejecting out of hand are the empirical 
things; confidence gained through testing or observation of the program 
in a debugger.  Everything else seems to qualify, and that's the 
problem.

So let's go ahead and agree about everything up until...

[...]

> As an initial next step, we could simply rely on the good old universal 
> type everywhere else in the program - it ought to be possible to make 
> the program well-typed in that case, it would just mean that the 
> provable properties would be nowhere near as pervasive as with a 
> traditional statically-typed program.

It would, in fact, mean that interesting provable properties would only 
be provable if data can't flow outside of those individual small bits 
where the programmer reasoned with types.  Of course that's not true, or 
the programmer wouldn't have written the rest of the program in the 
first place.  If we define the universal type as a variant type 
(basically, tagged or something like it, so that the type can be tested 
at runtime) then certain statements become provable, of the form "either 
X or some error condition is raised because a value is inappropriate".  
That is indeed a very useful property; but wouldn't it be easier to 
simply prove it by appealing to the language semantics that say that "if 
not X, the operation raises an exception," or to the existence of 
assertions within the function that verify X, or some other such thing 
(which must exist, or the statement wouldn't be true)?

> But the point is we would now 
> have put our types into a formal context.

Yes, but somewhat vacuously so...

> The point about inherent informality is just that if you fully formalize 
> a static type system for a dynamic language, such that entire programs 
> can be statically typed, you're likely to end up with a static type 
> system with the same disadvantages that the dynamic language was trying 
> to avoid.

Okay, so you've forced the admission that you have a static type system 
that isn't checked and doesn't prove anything interesting.  If you 
extended the static type system to cover the whole program, then you'd 
have a statically typed language that lacks an implementation of the 
type checker.

I don't see what we lose in generality by saying that the language lacks 
a static type system, since it isn't checked, and doesn't prove anything 
anyway.  The remaining statement is that the programmer may use static 
types to reason about the code.  But, once again, the problem here is 
that I don't see any meaning to that.  It would basically mean the same 
thing as that the programmer may use logic to reason about code.  That 
isn't particularly surprising to me.  I suppose this is why I'm 
searching for what is meant by saying that programmers reason about 
types, and am having that conversation in several places throughout this 
thread... because otherwise, it doesn't make sense to point out that 
programmers reason with types.

> Well, I'm trying to use the term "latent type", as a way to avoid the 
> ambiguity of "type" alone, to distinguish it from "static type", and to 
> get away from the obvious problems with "dynamic type".

I replied to your saying something to Marshall about the "type systems 
(in the static sense) of dynamically-typed languages."  That's what my 
comments are addressing.  If you somehow meant something other than the 
static sense, then I suppose this was all a big misunderstanding.

> But I'm much less interested in the term itself than in the issues 
> surrounding dealing with "real" types in dynamically-checked programs - 
> if someone had a better term, I'd be all in favor of it.

I will only repeat again that in static type systems, the "type" becomes 
a degenerate concept when it is removed from the type system.  It is 
only the type system that makes something a type.  Therefore, if you 
want "real" types, then my first intuition is that you should avoid 
looking in the static types of programming languages.  At best, they 
happen to coincide frequently with "real" types, but that's only a 
pragmatic issue if it means anything at all.

> So when well-typed program fragments are considered as part of a larger 
> untyped program, you're suggesting that this so radically changes the 
> picture, that we can no longer distinguish the types we identified as 
> being anything beyond programmer reasoning in general?

Is this so awfully surprising, when the type system itself is just 
programmer reasoning?  When there ceases to be anything that's provable 
about the program, there also ceases to be anything meaningful about the 
type system.  You still have the reasoning, and that's all you ever had.  
You haven't really lost anything, except a name for it.  Since I doubt 
the name had much meaning at all (as explained above), I don't count 
that as a great loss.  If you do, though, then this simple demonstrates 
that you didn't really mean "type systems (in the static sense)".

> > Hopefully, this isn't perceived as too picky.  I've already conceded 
> > that we can use "type" in a way that's incompatible with all existing 
> > research literature.  
> 
> Not *all* research literature.  There's literature on various notions of 
> dynamic type.

I haven't seen it, but I'll take your word that some of it exists.  I 
wouldn't tend to read research literature on dynamic types, so that 
could explain the discrepancy.

> > I would, however, like to retain some word with 
> > actually has that meaning.  Otherwise, we are just going to be 
> > linguistically prevented from discussing it.
> 
> For now, you're probably stuck with "static type".

That's fine.  I replied to your attempting to apply "static type" in a 
sense where it doesn't make sense.

> In CS, we don't have the luxury 
> of using the classic mathematician's excuse when confronted with 
> inconvenient philosophical issues, of claiming that type theory is just 
> a formal symbolic game, with no meaning outside the formalism.

As it turns out, my whole purpose here is to address the idea that type 
theory for programming languages is limited to some subset of problems 
which people happen to think of as type problems.  If type theorists 
fourty years ago had limited themselves to considering what people 
thought of as types back then, we'd be in a considerably worse position 
today with regard to the expressive power of types in commonly used 
programming languages.  Hence, your implication that insisting on a 
formal rather than intuitive definition is opposed to the real-world 
usefulness of the field is actually rather ironic.  The danger lies in 
assuming that unsolved problems are unsolvable, and therefore defining 
them out of the discussion until the very idea that someone would solve 
that problem with these techniques starts to seem strange.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation