Original-Via: uk.ac.nsf; Sat, 9 Nov 91 15:06:07 GMT
Original-Sender: [EMAIL PROTECTED]
I'm sorry if this is old news, but I just ran across what seems to be
a gratuitous loss of polymorphism in the transformational
specification of as-pattern binding in Haskell 1.1.
The problem is the lambda-expression in rule (d) for case expressions:
(d) case e0 of {x@p -> e; _ -> e'}
= let {y = e0}
in case y of {p -> (\ x -> e) y ; _ -> e'}
^^^^^^^^^^
This has the result that a case expression that uses an as-pattern to
match a constructor which doesn't depend on all the type variables in
its type can lose polymorphism.
Example (contrived, but accurate):
Usual definition of map:
map f [] = []
map f (x:xs) = f x : map f xs
Inferred type: map :: (a -> b) -> [a] -> [b]
Alternative definition of map:
map' f nil@[] = nil
map' f (x:xs) = f x : map f xs
Inferred type: map' :: (a -> a) -> [a] -> [a]
The problem is that the variable `nil' is lambda-bound, so its two
occurrences are constrained to be of the same type, which implies, via
the rule that all branches of a case have the same type, that the
source and target types of f are the same.
I don't understand why the transformation rule could not have been
(d') case e0 of {x@p -> e; _ -> e'}
= let {y = e0}
in case y of {p -> let x = y in e ; _ -> e'}
or even
(d'') case e0 of {x@p -> e; _ -> e'}
= let {x = e0}
in case y of {p -> e ; _ -> e'}
This is a minor point, to be sure; but it was very surprising to me
when it caused me problems in perfectly normal-looking code.
-- Dan Rabin
