[Haskell-cafe] type inference and named fields
Jonathan Cast
jcast at ou.edu
Sun Jun 26 18:56:46 EDT 2005
Daniel Brown <danb at cs.utexas.edu> wrote:
> Jonathan Cast wrote:
> > Lennart Augustsson <lennart at augustsson.net> wrote:
> >>
> >>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.
>
> I see that the argument to foo has type `Either a b` (unquantified),
> but why can't x, bound to the value that matches the pattern, have the
> type of the pattern?
Because it's bound to a value of the type of the argument, not of the
type of the pattern. What about the function
> bar :: alpha -> beta
> bar x = x
? The pattern here is x, and its type is (x :: forall tau. tau). But,
I think it axiomatic that typing rules have to forbid functions like
bar.
> In this case, that would let `x :: forall x. Either x b`, which
> unifies with `Either () b`.
Jon Cast
More information about the Haskell-Cafe
mailing list