> The nice thing about Monads+the do-notation is that  it gives you a natural
> hook to catch pattern match failures! We must nurture every chance we have
> to improve staticness of typing. I don't agree with your argument that
> because pattern match failure in function definitions is not catched by the
> type-checker justifies dropping that extra safety for pattern matching in
> the do-notation.

The problem of failing pattern matching can be handled in a different way.
have a look at Elegant 
(http://www.research.philips.com/generalinfo/special/elegant/elegant.html).

Here, constructors are types, more precesiely, they are sub-types.
Thus in 

  List a = Null | Cons a (List a)

List is a type, Null a sub-type of List and Cons a sub-type of List.

The function

  head (Cons a _) = a

is treated by the type checker as a partial function, only defined for
the sub-type Cons and not for the whole type List.
The type checker will issue compile-time warnings and run-time checks for
any caller of head that does not ensure statically that the argument is
of type Cons. These warnings could be errors if you want even more safety.

The type checker is not so smart that it can treat every pattern as a type.
It rounds patterns to the nearest higher super-type. Thus the type of

  foo (Cons a Null) = a

is just Cons a -> a.

But in this case, the type checker will issue a compile time warning that
the type of foo is incomplete. It misses the case (Cons a _). 
Note that it does not enforce the case (Null), it allows foo to be partial, 
but not too partial.

Observe that pattern matching now has become equivalent to run-time 
type-analysis.

Both features (checking on coercions to sub-types and missing patterns)
have proven to be very convient and remove allmost all run-time errors in this
category, unless the programmer has ingnored a static warning.
A counter example is the list-indexing function, which is partial but can
not be proven correct at compile time (maybe with dependant types ...).

Is this something for Haskell-3? :-)

> As Koen said, some of the proposed type weakenings (unoverloading
> list-comprehensions, junking MonadZero) are partly motived by the fact that
> the type checker gives bad error messages. Well, I rather have bad error
> messages from the type checker than good error messages at run-time! Perl,
> Tcl, Visual Basic, Phyton, etc are great languages from this perspective,
> their type checker *never* complains.

Agreed Erik. Solve the problem in the proper way: improve the error messages.

> Strong typing is what distinguishes Haskell from the muck, let's be proud of
> it. I cannot believe that the Dutch are the only prim and proper
> programmers! Or maybe I concentrate too much on type safety to the detriment
> of simplicity and pragmatism. In any case, we must be fully aware of the
> fact that we trade the one for the other.

I think treating constructors as sub-types makes things both more simple and
more safe. But well, I'm Dutch too :-).

Lex


Reply via email to