Dave Bayer wrote:
I've enjoyed the recent typing discussions here. On one hand, there's little difference between using dynamic typing, and writing incomplete patterns in a strongly typed language. On the other hand, how is an incomplete pattern any different from code that potentially divides by zero? One quickly gets into decidability issues, dependent types, Turing-complete type systems.
True enough, in a sense, a dynamically typed language is like a statically typed language with only one type (probably several by distinguishing function types) and many incomplete pattern matches. So, you can embed a dynamically typed language into a strongly typed language without loosing static type checking. However, the other way round is impossible: virtually void of static type checking, the dynamic language is incapable of embedding a strongly typed language without loosing type safety. Thus, you still gain something with strong typing even with incomplete pattern matches. In fact, the programmer has the power to arrange things such that he gains extremely much. What about throwing out incomplete patterns completely? Well, this is a very mixed blessing. There are incomplete patterns and non-terminating programs, both commonly denoted with _|_. As long as you allow non-termination, you can't get rid of incomplete patterns. But enforcing termination everywhere can be very limiting: 1) The programmer has to detail in some form the proof that his program terminates. Arguably, he ought to do so anyway but he doesn't need to write his proof in a way that can be checked by a dumb computer. Take for example minimum = head . sort Here, the theorem that this program proves is obvious from the proof itself. But to make it checkable by a machine, I'm sure that further type annotations are needed that don't add additional insight anymore. 2) There are programs that terminate but cannot be stated in a given always-terminating language. Most likely, an interpreter for this language is one of those programs. Getting rid of incomplete patterns means to rule out terms that do not fulfill a given invariant. Dependent types are a good way too that, but again, you have issue 1). The proofs will only be tractable if it's possible to concentrate on the interesting invariants and drop the others. In the end, strongly normalizing languages and dependent types are an active research area for exactly these problems. In the end, I think that strong types is only one thing that makes Haskell programs work after compilation. The other ones are higher-order functions and *purity*. No type system can achieve what purity offers. Regards, apfelmus