Anton van Straaten said:
The problem is that there are no useful sound definitions for the type
systems (in the static sense) of dynamically-typed languages. Yet, we
work with type-like static properties in those languages all the time,
as I've been describing.
I honestly don't find it very compelling that there are similarities
between the kinds of reasoning that goes on in static type systems
versus those used by programmers in dynamically typed languages.
Rather, of course there are similarities. It would be shocking if there
were not similarities. These similarities, though, have nothing to with
the core nature of types.
Basically, there are ways to reason about programs being correct.
Static type systems describe their reasoning (which is always axiomatic
in nature) by assigning "types" to expressions. Programmers in
dynamically typed languages still care about the correctness of their
programs, though, and they find ways to reason about their programs as
well. That reasoning is not completely axiomatic, but we spend an
entire lifetime applying this basic logical system, and it makes sense
that programmers would try to reason from premises to conclusions in
ways similar to a type system. Sometimes they may even ape other type
systems with which they are familiar; but even a programmer who has
never worked in a typed language would apply the same kind of logic as
is used by type systems, because it's a form of logic with which
basically all human beings are familiar and have practiced since the age
of three (disclaimer: I am not a child psychologist).
On the other hand, programmers don't restrict themselves to that kind of
pure axiomatic logic (regardless of whether the language they are
working in is typed). The also reason inductively -- in the informal
sense -- and are satisfied with the resulting high probabilities. They
generally apply intuitions about a problem statement that is almost
surely not written clearly enough to be understood by a machine. And so
forth.
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. 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.
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?
We know that we can easily take dynamically-typed program fragments and
assign them type schemes, and we can make sure that the type schemes
that we use in all our program fragments use the same type system.
Again, it would be surprising if this were not true. If programmers do,
in fact, tend to reason correctly about their programs, then one would
expect that there are formal proofs that could be found that they are
right. That doesn't make their programming in any way like a formal
proof. I tend to think that a large number of true statements are
provable, and that programmers are good enough to make a large number of
statements true. Hence, I'd expect that it would be possible to find a
large number of true, provable statements in any code, regardless of
language.
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.
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; and when that is the goal, it still shouldn't
be applied to process that aren't formalized until they manage to become
formalized.
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. 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.
