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

[Olaf Klinke]

On Tue, 2020-09-08 at 16:12 +0000, Richard Eisenberg wrote:
> 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.

The definition of Y is the one given by Ignat in his OP of this thread,
which essentially is Y ~ Data.Functor.Identity. We know very well that 

λ x. x {runIdentity = "c"} :: ∀ α. Identity α -> Identity String

is indeed independent of α and in this special case the compiler seems
to infer this [*]. But first-year CS students learn that any non-
trivial property of a program is undecidable, whence I'm hesitating to
blame GHC for not giving Ignat the behaviour he expects.   

Probable explanation: It *is* a free theorem that for any concrete type
T, any function 

f ::  ∀ α. α -> T

can not possibly use its argument and hence must be constant, if type
families are not involved. So my question is whether this free theorem
still holds when α is wrapped in any one-parameter type constructor.
Ignat's OP involved a constraint, too, and I see that this complicates
matters. Consider

foo ::  ∀ α. (Show α, Default α) => Identity α
foo = Identity def
notConstant = (runIdentity . fmap show) foo :: String

which at first glance looks like one could apply the free theorem but
the value clearly depends on the choice of α. GHCi in fact accepts this
expression and substitutes α = () when asked to print notConstant, but
GHC rightfully rejects the program. 

Olaf

[*] The following compiles: 

import Data.Functor.Identity
main = print . 
    runIdentity $
    (Identity undefined) {runIdentity = "c"}

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