> Incidentally, I don't think it would be sensible to change
> the type system to allow the
>
> demo1 :: (a -> b) -> Either a c -> Either b c
> demo1 f (Left a) = Left (f a)
> demo1 _ r@(Right c) = r
>
> What type does r have? Either a c.
> What type does the result of the fn have? Either b c.
> Different types. It would be hard (I believe) to specify crisply
> when it was legitimate for two terms with different types to
> be as'd together.
Well, one could argue that the type of r is
forall a.Either a c
in which case there is no problem.
The tricky question is: what exactly is the argument
that permits us to abstract the type variable a?
Usually we don't perform any type abstractions during pattern matching.
One could argue that we didn't. All we did was exploiting a type isomorphism:
the type of Right is
forall a,b. a->Either b a
but this is isomorphic (in System F) to
forall a. a->(forall b.Either b a)
In other words, we would simply allow patterns to have polymorphic types
and only instantiate the quantifiers if we have to.
Moreover, when we instantiate polymorphism we could push quantifiers inwards
(whenever possible) instead of eliminating them.
Just an idea
Stefan
