X-Comment1: #############################################################
X-Comment2: # uk.ac.glasgow.cs has changed to uk.ac.glasgow.dcs #
X-Comment3: # If this address does not work please ask your mail #
X-Comment4: # administrator to update your NRS & mailer tables. #
X-Comment5: #############################################################
Dan
I think that there are two things going on in your example which are
getting mixed up. Here's the example:
| 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.
...
| 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]
Now your suggestion is that (under the revised rule for case you
give) map' should be equivalent to:
map' f zs = let {nil = zs} in
case zs of
[] -> nil
(x:xs) -> f x : map' f xs
And your claim is that then you would get the expected type for map'
(ie the same as map). But you wouldn't! Just because nil is let-bound
doesn't mean that it is polymorphic! It is here bound to zs, which
is monomophic (usual Hindley-Milner lambda-binding rule), so you will
*still* get the restricted type you give above for map'.
| 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'}
My suggestion is that this would not make any difference to your example.
The reason your example goes wrong is because you name one of the arguments
(nil), and use that name in the result, thus forcing them to be of the same
type.
It is nevertheless true that there is a gratuitous loss of polymorphism
in the static semantics of case. Consider
case (\x.x, \y.y) of
(f,g) -> (f 'a', f True)
This will fail, because f behaves as if it was lambda-bound not let-bound.
So there's a lost opportunity here. We took the conservative line because
we couldn't convince ourselves of the correct typing rules for a polymorphic
version, and there didn't seem to be lots of programs which required
it. (This shortcoming is identified in the Preface.)
|
| 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.
Did you actually run across it in a real program?
Simon
