Re: [very] basic question
> 2. Are there accepted principles for the design of a 'good' type system
> in a language? For example, I've read that Haskell has a 'good' type
> system, while pascal's is limiting. What are the characteristics of
> the Haskell type system that make it 'good'?
Speaking informally, I'd say there are at least two properties of a type
system that make it 'good'. (I'm assuming, of course, that the type system is
correct to begin with, i.e. that only safe programs are well-typed.)
+ One is its expressiveness, i.e. its ability to accept programs written
in a 'natural' style.
A key feature, with respect to expressiveness, is polymorphism. Pascal
doesn't have it; Haskell has 'ML-style' parametric polymorphism, which
considerably extends its expressive power and reduces the need for code
+ The other is its simplicity. Simplicity is required for a type system
to be reasonably easy to use, and may yield the (surprising, but very
useful) property that 'well-typed programs are (often) correct' (i.e.
they don't just run without crashing, they actually do what's intended).
Note that this property is, in a way, contradictory with the previous
one. The idea is that, if the type system is too expressive, it may be
able to express a (contrived) proof that a program is safe, even though
the program doesn't work as the programmer expects. If, on the other hand,
the type system is simple enough, incorrect programs will often lead to
Examples of good balance between expressiveness and simplicity are
perhaps ML and Haskell. Extending these type systems with, say,
(equi-)recursive types augments their expressive power, but causes
many 'incorrect' (albeit safe) programs to become well-typed. Hence,
it is usually considered unwise to do so.
Another important feature of ML and Haskell is type inference, which helps
make the type system less obtrusive, by making fewer type annotations
required. Type inference often places strong restrictions on the design
of the type system, though, so whether it is a 'good' feature is open to