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

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