What is Expressiveness in a Computer Language

[Anton van Straaten]

Chris Smith wrote:
> What makes static type systems interesting is not the fact that these 
> logical processes of reasoning exist; it is the fact that they are 
> formalized with definite axioms and rules of inference, performed 
> entirely on the program before execution, and designed to be entirely 
> evaluatable in finite time bounds according to some procedure or set of 
> rules, so that a type system may be checked and the same conclusion 
> reached regardless of who (or what) is doing the checking.  All that, 
> and they still reach interesting conclusions about programs.  

There's only one issue mentioned there that needs to be negotiated 
w.r.t. latent types: the requirement that they are "performed entirely 
on the program before execution".  More below.

> If 
> informal reasoning about types doesn't meet these criteria (and it 
> doesn't), then it simply doesn't make sense to call it a type system 
> (I'm using the static terminology here).  It may make sense to discuss 
> some of the ways that programmer reasoning resembles types, if indeed 
> there are resemblances beyond just that they use the same basic rules of 
> logic.  It may even make sense to try to identify a subset of programmer 
> reasoning that even more resembles... or perhaps even is... a type 
> system.  It still doesn't make sense to call programmer reasoning in 
> general a type system.

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.  But "latent" means what 
it implies: someone who is more aware of types can do better at 
developing the latent types.

As a starting point, let's assume we're dealing with a disciplined 
programmer who (following the instructions found in books such as the 
one at htdp.org) reasons about types, writes them in his comments, and 
perhaps includes assertions (or contracts in the sense of "Contracts for 
Higher Order Functions[1]), to help check his types at runtime (and I'm 
talking about real type-checking, not just tag checking).

When such a programmer writes a type signature as a comment associated 
with a function definition, in many cases he's making a claim that's 
provable in principle about the inputs and outputs of that function.

For example, if the type in question is "int -> int", then the provable 
claim is that given an int, the function cannot return anything other 
than an int.  Voila, assuming we can actually prove our claim, then 
we've satisfied the requirement in Pierce's definition of type system, 
i.e. "proving the absence of certain program behaviors by classifying 
phrases according to the kinds of values they compute."

The fact that the proof in question may not be automatically verified is 
no more relevant than the fact that so many proofs in mathematics have 
not been automatically verified.  Besides, if the proof turns out to be 
wrong, we at least have an automated mechanism for finding witnesses to 
the error: runtime tag checks will generate an error.  Such detection is 
not guaranteed, but again, "proof" does not imply "automation".

What I've just described walks like a type and talks like a type, or at 
least it appears to do so according to Pierce's definition.  We can 
classify many terms in a given dynamically-typed program on this basis 
(although some languages may be better at supporting this than others).

So, on what grounds do you reject this as not being an example of a 
type, or at the very least, something which has clear and obvious 
connections to formal types, as opposed to simply being arbitrary 
programmer reasoning?

Is it the lack of a formalized type system, perhaps?  I assume you 
recognize that it's not difficult to define such a system.

Regarding errors, we haven't proved that the function in question can 
never be called with something other than an int, but we haven't claimed 
to prove that, so there's no problem there.  I've already described how 
errors in our proofs can be detected.

Another possible objection is that I'm talking about local cases, and 
not making any claims about extending it to an entire program (other 
than to observe that it can be done).  But let's take this a step at a 
time: considered in isolation, if we can assign types to terms at the 
local level in a program, do you agree that these are really types, in 
the type theory sense?

If you were to agree, then we could move on to looking at what it means 
to have many local situations in which we have fairly well-defined 
types, which may all be defined within a common type system.

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.  But the point is we would now 
have put our types into a formal context.

> In the same post here, you simultaneously suppose that there's something 
> inherently informal about the type reasoning in dynamic languages; and 
> then talk about the type system "in the static sense" of a dynamic 
> language.  How is this possibly consistent?

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.

However, that doesn't preclude type system being defined which can be 
used to reason locally about dynamic programs.  Some people actually do 
this, albeit informally.

>>So we actually have quite a bit of evidence about the presence of static 
>>types in dynamically-typed programs.
> 
> 
> No.  What we have is quite a bit of evidence about properties remaining 
> true in dynamically typed programs, which could have been verified by 
> static typing.

Using my example above, at least some of those properties would have 
been verified by manual static typing.  So those properties, at least, 
seem to be types, at least w.r.t. the local fragment they're proved within.

>>We're currently discussing something that so far has only been captured 
>>fairly informally.  If we restrict ourselves to only what we can say 
>>about it formally, then the conversation was over before it began.
> 
> 
> I agree with that statement.  However, I think the conversation 
> regarding static typing is also over when you decide that the answer is 
> to weaken static typing until the word applies to informal reasoning.  
> If the goal isn't to reach a formal understanding, then the word "static 
> type" shouldn't be used

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".

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.

> and when that is the goal, it still shouldn't 
> be applied to process that aren't formalized until they manage to become 
> formalized.

This comes back to the phrase I highlighted at the beginning of this 
message: "performed entirely on the program before execution". 
Formalizing local reasoning about types is pretty trivial, in many 
cases.  It's just that there are other cases where that's less 
straightforward.

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?  All the hard 
work we did figuring out the types, writing them down, writing 
assertions for them, and testing the program to look for violations 
evaporates into the epistemological black hole that exists outside the 
boundaries of formal type theory?

> 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 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".  But I think it was 
never likely to be the case that type theory would succeed in absconding 
with the only technically valid use of the English word "type". 
Although not for want of trying!

Besides, I think it's worth considering why Bertrand Russell used the 
term "types" in the first place.  His work had deliberate connections to 
the real world.  Type theory in computer science unavoidably has similar 
connections.  You could switch to calling it Zoltar Theory, and you'd 
still have to deal with the fact that a zoltar would have numerous 
connections to the English word "type".  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.

Anton

[1] 
http://people.cs.uchicago.edu/~robby/pubs/papers/ho-contracts-techreport.pdf