What is Expressiveness in a Computer Language
Anton van Straaten
anton at appsolutions.com
Sun Jun 25 10:10:34 CEST 2006
> Chris F Clark wrote:
>>I'm particularly interested if something unsound (and perhaps
>>ambiguous) could be called a type system. I definitely consider such
>>things type systems.
> I don't understand. You are saying you prefer to investigate the
> unsound over the sound?
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.
If you want to talk about those properties as though they were types,
one of the options is what Chris Clark described when he wrote "I reason
about my program using types which I can (at least partially) formalize,
but for which there is no sound axiomatic system."
>>However, I like my definitions very general and
>>vague. Your writing suggests the opposite preference.
> Again, I cannot understand this. In a technical realm, vagueness
> is the opposite of understanding. To me, it sounds like you are
> saying that you prefer not to understand the field you work in.
The issue as I see it is simply that if we're going to work with
dynamically-typed programs at all, our choices are limited at present,
when it comes to formal models that capture our informal static
reasoning about those programs. In statically-typed languages, this
reasoning is mostly captured by the type system, but it has no formal
description for dynamically-typed languages.
>>To me if
>>something works in an analogous way to how a known type system, I tend
>>to consider it a "type system". That probably isn't going to be at
>>all satisfactory to someone wanting a more rigorous definition.
> Analogies are one thing; definitions are another.
A formal definition is problematic, precisely because we're dealing with
something that to a large extent is deliberately unformalized. But as
Chris Clark pointed out, "these types are locally sound, i.e. I can
prove properties that hold for regions of my programs." We don't have
to rely entirely on analogies, and this isn't something that's entirely
fuzzy. There are ways to relate it to formal type theory.
>>course, to my mind, the rigorous definitions are just an attempt to
>>capture something that is already known informally and put it on a
>>more rational foundation.
> If something is informal and non-rational, it cannot be said to
> be "known."
As much as I love the view down into that abyss, we're nowhere near
being in such bad shape.
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.
We know that we can assign type schemes to entire dynamically-typed
programs, and we can even automate this process, although not without
some practical disadvantages.
So we actually have quite a bit of evidence about the presence of static
types in dynamically-typed programs.
Besides, we should be careful not to forget that our formal methods are
incredibly weak compared to the power of our intelligence. If that were
not the case, there would be no advantage to possessing intelligence, or
We are capable of reasoning outside of fully formal frameworks. The
only way in which we are able to develop formal systems is by starting
with the informal.
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.
More information about the Python-list