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.