[Haskell-cafe] type inference and named fields

[Lennart Augustsson]

Jonathan Cast wrote:
> 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.

I'm very well aware that you cannot translate this to type correct
System F.  That doesn't mean it's necessarily unsafe.

I wasn't suggesting to change GHC nor Haskell, I was just pointing
out a similar problem.

> 
> 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.

There are no types around at run time so in case foo is being passed
a Right argument the representation of the result is identical to the
argument.  (OK, if you want to be very pedantic, this isn't necessarily
true for every possible implementation of Haskell, just all existing 
ones. :)

	-- Lennart