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

[Richard Eisenberg]

Hi Olaf,

I could understand this question better with a concrete definition of what Y is. Sometimes, the value of (defaultY { y = "c"}) really does depend on `a`. But maybe I'm misunderstanding your intent.

Richard

> On Sep 7, 2020, at 3:25 PM, Olaf Klinke <olf at aatal-apotheke.de> wrote:
> 
> I take it that in the expression
> 
> (defaultY ∷ ∀ α. Monoid α ⇒ Y α) {y = "c"}
> 
> the compiler is not smart enough to infer that the concrete value of α
> is irrelevant for the outcome and therefore rejects the program. The
> obligation here is to prove that the function
> 
> λ x. x {y = "c"} :: ∀ α. Y α -> Y String
> 
> is constant across all possible values of α, which I guess is
> undecidable for general one-parameter types? Or is there a free theorem
> saying that whenever a function has this general type signature, then
> the α cannot possibly be used? This certainly fails if Y has more type
> parameters that remain constant in the expression: A type class could
> distinguish the extra type parameters even if at the value level the
> result is constant across all α.
> 
> Olaf
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.