[Haskell-cafe] type inference and named fields
jcast at ou.edu
Thu Jun 23 15:46:59 EDT 2005
Lennart Augustsson <lennart at augustsson.net> wrote:
> A somewhat similar problem exists even without fields:
> foo :: Either a b -> Either () b
> foo (Left _) = Left ()
> foo x@(Right _) = x
> Since Haskell type checking doesn't use the information gained
> by pattern matching to refine types we just have to accept that
> some perfectly safe programs don't type check.
Well, not perfectly safe. We already had this discussion (about ),
but to say it again: the value bound by any pattern has some particular
type. x above doesn't have type (Either a b) for arbitrary a and b, but
rather (Either a b) for some specific a and b. Unless that specific a
happens to be (), x doesn't have the correct type to be the rhs of foo.
It would require a radical change to GHC (moving away from System F as a
basis for the intermediate language Core) to implement a language in
which this wasn't true.
Here is (approximately) the Core translation of foo above:
> foo :: forall a b. Either a b -> Either () b
> foo = /\ a b -> \ e -> case e of
> Left _ -> Left @() @b ()
> Right _ -> e
You call this as (foo @a @b e), where e has type (Either a b).
So, the call (foo @a @b (Right @a @b x)) reduces (ignoring types) to
(Right @a @b x). This reduces a term of type (Either () b) to one of
type (Either a b). That's not type safe.
More information about the Haskell-Cafe