What is Expressiveness in a Computer Language

[Anton van Straaten]

Marshall wrote:
> 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.

>>Of
>>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 
implementing AIs.

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.

Anton