What is Expressiveness in a Computer Language
benjamin.franksen at bessy.de
Thu Jun 22 23:47:22 CEST 2006
George Neuner wrote:
> The point is really that the checks that prevent these things
[such as 'array index out of bounds']
> must be
> performed at runtime and can't be prevented by any practical type
> analysis performed at compile time. I'm not a type theorist but my
> opinion is that a static type system that could, a priori, prevent the
> problem is impossible.
It is not impossible. Dependent type systems can -- in principle -- do all
such things. Take a look at Epigram (http://www.e-pig.org/).
Systems based on dependent types such as Epigram are not yet mature enough
to be used for serious programming. However, they clearly show that these
things /are/ possible.
More information about the Python-list