[Prev][Next][Index][Thread]

Re: [very] basic question


Hi Scott,

> 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
   duplication.

 + 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
   type errors.

   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
debate.

Best regards,

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/