[Haskell-cafe] Re: Best idiom for avoiding Defaulting warnings with ghc -Wall -Werror ??

[apfelmus]

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