Python from Wise Guy's Viewpoint

[Joachim Durchholz]

Pascal Costanza wrote:
> ....because static type systems work by reducing the expressive power of 
> a language. It can't be any different for a strict static type system. 
> You can't solve the halting problem in a general-purpose language.

The final statement is correct, but you don't need to solve the halting 
problem: it's enough to allow the specification of some easy-to-prove 
properties, without hindering the programmer too much.

Most functional languages with a static type system don't require that 
the programmer writes down the types, they are inferred from usage. And 
the type checker will complain as soon as the usage of some data item is 
inconsistent.
IOW if you write
   a = b + "asdf"
the type checker will infer that both a and b are strings; however, if 
you continue with
   c = a + b + 3
it will report a type error because 3 and "adsf" don't have a common 
supertype with a "+" operation.

It's the best of both worlds: no fuss with type declarations (which is 
one of the less interesting things one spends time with) while getting 
good static checking.
(Nothing is as good in practice as it sounds in theory, and type 
inference is no exception. Interpreting type error messages requires 
some getting used to - just like interpreting syntax error messages is a 
bit of an art, leaving one confounded for a while until one "gets it".)

> (Now you could argue that current sophisticated type systems cover 90% 
> of all cases and that this is good enough, but then I would ask you for 
> empirical studies that back this claim. ;)

My 100% subjective private study reveals not a single complaint about 
over-restrictive type systems in comp.lang.functional in the last 12 months.

Regards,
Jo