>> Nah. It's useful to know you haven't violated the type system, and 
>> that's decidable.
>
> I seem to remember that type systems had the same complexity as or might 
> even be Turing machines in themselves, but I assume you know better.

The way I heard it, it is undecidable whether an arbitrary program is 
"type-safe". (I.e., it never tries to perform an operation on an 
unsuitable type.) So various type systems have been invented where it is 
decidable whether a given program is "well-typed" (i.e., it fits the 
rules of the type system). Under this definition, certain programs which 
are type-safe are rejected as ill-typed because they violate some 
restriction of the type system.

In other words, the type system is an artiface invented to turn an 
undecidable problem into a decidable one.

For example:

   5 + (if 1 == 1 then 0 else "yellow")

This is type-safe (it produces the answer 5), but most type systems 
would reject this as ill-typed.

Of course, by the time you get to Haskell with a few language extensions 
turned on, the automatic type inferrence engine is basically a Prolog 
program that gets run at compile-time, and can take an unbounded amount 
of time (and space) to terminate...

Post a reply to this message