Python from Wise Guy's Viewpoint

[Pascal Costanza]

Andreas Rossberg wrote:
> Pascal Costanza wrote:
> 
>>
>> "less expressive power" means that there exist programs that work but 
>> that cannot be statically typechecked. These programs objectively 
>> exist. By definition, I cannot express them in a statically typed 
>> language.
>>
>> On the other hand, you can clearly write programs in a dynamically 
>> typed language that can still be statically checked if one wants to do 
>> that. So the set of programs that can be expressed with a dynamically 
>> typed language is objectively larger than the set of programs that can 
>> be expressed with a statically typed language.
> 
> Well, "can be expressed" is a very vague concept, as you noted yourself. 
>   To rationalize the discussion on expressiveness, there is a nice paper 
> by Felleisen, "On the Expressive Power of Programming Languages" which 
> makes this terminology precise.

I have skimmed through that paper. It states the following in the 
conclusion section:

"The most important criterion for comparing programming languages showed 
that an increase in expressive power may destroy semantic properties of 
the core language that programmers may have become accustomed to 
(Theorem 3.14). Among other things, this invalidation of operational 
laws through language extensions implies that there are now more 
distinctions to be considered for semantic analyses of expressions in 
the core language. On the other hand, the use of more expressive 
languages seems to facilitate the programming process by making programs 
more concise and abstract (Conciseness Conjecture). Put together, this 
result says that

* an increase in expressive power is related to a decrease of the set of 
``natural'' (mathematically appealing) operational equivalences."

This seems to be compatible with my point of view. (However, I am not 
really sure.)

> Anyway, you are right of course that any type system will take away some 
> expressive power (particularly the power to express bogus programs :-) 
> but also some sane ones, which is a debatable trade-off).

Thanks. ;)

> But you completely ignore the fact that it also adds expressive power at 
> another end! For one thing, by allowing you to encode certain invariants 
> in the types that you cannot express in another way. Furthermore, by 
> giving more knowledge to the compiler and hence allow the language to 
> automatize certain tedious things.

I think you are confusing things here. It gets much clearer when you 
separate compilation/interpretation from type checking, and see a static 
type checker as a distinct tool.

The invariants that you write, or that are inferred by the type checker, 
are expressions in a domain-specific language for static program 
analysis. You can only increase the expressive power of that 
domain-specific language by adding a more elaborate static type system. 
You cannot increase the expressive power of the language that it reasons 
about.

An increase of expressive power of the static type checker decreases the 
expressive power of the target language, and vice versa.

As a sidenote, here is where Lisp comes into the game: Since Lisp 
programs can easily reason about other Lisp programs, because there is 
no distinction between programs and data in Lisp, it should be pretty 
straightforward to write a static type checker for Lisp programs, and 
include them in your toolset.

It should also be relatively straightforward to make this a relatively 
flexible type checker for which you can increase/decrease the level of 
required conformance to the (a?) type system.

This would mean that you could have the benefits of both worlds: when 
you need static type checking, you can add it. You can even enforce it 
in a project, if the requirements are strict in this regard in a certain 
setting. If the requirements are not so strict, you can relax the static 
type soundness requirements, or maybe even go back to dynamic type checking.

In fact, such systems already seem to exist. I guess that's what soft 
typing is good for, for example (see MrFlow). Other examples that come 
to mind are Qi and ACL2.

Why would one want to switch languages for a single feature?

Note that this is just brainstorming. I don't know whether such an 
approach can really work in practice. There are probably some nasty 
details that are hard to solve.

> Overloading is one obvious example 
> that increases expressive power in certain ways and crucially relies on 
> static typing.

Overloading relies on static typing? This is news to me. What do you mean?

> So there is no inclusion, the "expressiveness" relation is unordered wrt 
> static vs dynamic typing.

No, I don't think so.


Pascal

-- 
Pascal Costanza               University of Bonn
mailto:costanza at web.de        Institute of Computer Science III
http://www.pascalcostanza.de  Römerstr. 164, D-53117 Bonn (Germany)