Re: antipathy to type systems

[Olivier Lefevre<address@hidden>]

>>> Shriram Krishnamurthi<sk@cs.brown.edu> 17/11/2003 01:39:13 >>>
I will add one comment to what Matthias wrote.  Many people in the
lightweight community seem to have a certain antipathy to type
systems.  I would class them into a few off-the-cuff categories:

I think there's a fifth category, made of people who have a limited 
understanding of types and no knee-jerk aversion to them but who
doubt that a type system exists that is both pleasantly expressive 
yet usable without a Ph.D. in type theory. The issue here is that the
complexity of type theory rears its head every time the checker 
throws an error: it can't be swept under the carpet. Yet if you can't
understand the error messages you have little chance of writing
a correct program, except by chance or by restricting yourself to
a less expressive subset of the type system, which defeats the
intent.

OTOH, as Shriram pointed out later, there is plenty more that go wrong
even in a well-typed system: think concurrency issues, for instance.
Yet some type advocay has a cargo cult feel to it, like types were the
be-all and end-all of program checking.

-- O.L.