[Haskell-cafe] Cannot update a field in a record with a polymorphic type.

[Viktor Dukhovni]

On Thu, Sep 10, 2020 at 11:03:59AM +0100, Tom Ellis wrote:

> On Thu, Sep 10, 2020 at 02:47:23PM +0500, Ignat Insarov wrote:
> > What I meant to express is that this problem _does not need to occur_
> > with record updates, even though they are presently being desugared to
> > functions. In other words, I propose that record updates _are_ special
> > — or _should be_ special, in any case.
> 
> Ah, I see.  You are saying that record updates can have a special
> typing rule because we have extra information that tells us that the
> type of the result cannot depend on the type of what was previously
> there.

That could be a surprising situation, there'd be things one could do
with the record update setters, that one could not do with Lens setters.

The work-around is to no define a type-preserving setter:

    monoUpdate :: Y a -> a -> Y a
    monoUpdate r a = r { y = a }

and use it to construct values of Y from a polymorphic seed.  One
might even note that:

    defaultY :: Monoid a => Y a
    defaultY = Y mempty

is a itself not a record, because it does not have a concrete type.  It
is a polymorphic nullary function that can produce a record, given a
context in which the desired type is apparent (can be inferred).
Therefore,

    defaultY { y = "c" }

is not an update of an existing input record, but rather it is an
(attempted) update of a new record, to be created there and then via a
call to the defaultY "factory".  But that call does not provide a
context to determine the type (and thus value) of defaultY.

Yes, we reason that it couldn't matter, but the compiler has limited
resources, and there's only so much inference that is compatible with
not slowing down compile times beyond their their current heft.  The
kind of inference needed to conclude that the type does not matter is
not built-in.

So, to me, needing to assign an explicit type in this corner case is
just an ordinary cost of doing functional programming (rooted in the
pure lambda calculus, where its functions all the way down).

I found it's initially somewhat unintuitive behaviour actually rather
educational.  Taking the time to understand it clarified some key
ideas.

-- 
    Viktor.