RE: Pattern Match Success Changes Types

[Koen Claessen]

Frank A. Christoph wrote:

 | With regard to merging Either instances, I agree with Simon that for most
 | programs this will not buy you much, but there are two common kinds of
 | programs where one could expect a significant effect on performance, just
 | because of sheer scale.

It is not only Either instances who suffer from this. Consider the
following definition of "map", which could be made by a naive user:

  map :: (a -> b) -> [a] -> [b]
  map f (x:xs) = f x : map f xs
  map f xs     = xs

Same problem here.

Stefan Kahrs <[EMAIL PROTECTED]> wrote:

 | >  demo1 :: (a -> b) -> Either a c -> Either b c
 | >  demo1 f (Left  a)   = Left (f a)
 | >  demo1 _ r@(Right c) = r
 | 
 | Well, one could argue that the type of r is
 |         forall a.Either a c
 | in which case there is no problem.

This should indeed do the trick, but I think it is way too difficult, if
not impossible. There is a reason that lambda-bound variables are not
generalized: because of decidability of type checking. But maybe it is
different with patterns, I don't know.

Regards,
Koen.

--
Koen Claessen,
[EMAIL PROTECTED],
http://www.cs.chalmers.se/~koen,
Chalmers University of Technology.