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.

On Thu, Sep 10, 2020 at 11:45:45AM +0500, Ignat Insarov wrote:

Thank you all kind folks who responded.

I think a leap of reasoning has occurred and I would like to ask you all to slow down and notice it.

Record update is special syntax.

It is not a function. It is not as general as a function. It is not perceived nor written as a function. Ain't no lambda in it.

You may say that it desugars to a function. But as a user of the language, I am unconcerned: desugar another way then!

Surely a function of type `C α ⇒ Y α → Y String` may assign different strings to `y`, by consulting methods of `C`. But a record update cannot! Neither the value `y₀` nor the type variable α are ever in the scope of the update expression.

Why do you say it has anything to do with record update being special? The same problem occurs with a true function: Prelude> data Y a = Y { y :: a } Prelude> let defaultY = Y { y = mempty } Prelude> let setYc y = y { y = "c" } Prelude> :t defaultY defaultY :: Monoid a => Y a Prelude> :t setYc setYc :: Y a -> Y [Char] Prelude> :t setYc defaultY <interactive>:1:7: error: • Ambiguous type variable ‘a0’ arising from a use of ‘defaultY’ prevents the constraint ‘(Monoid a0)’ from being solved. Probable fix: use a type annotation to specify what ‘a0’ should be. These potential instances exist: instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’ instance Monoid Ordering -- Defined in ‘GHC.Base’ instance Semigroup a => Monoid (Maybe a) -- Defined in ‘GHC.Base’ ...plus 7 others (use -fprint-potential-instances to see them all) • In the first argument of ‘setYc’, namely ‘defaultY’ In the expression: setYc defaultY

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.

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

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.

Here's an example where the previous value matters: λ> data Y a = Y { y :: !a } deriving Show λ> defaultY :: Monoid a => Y a ; defaultY = Y undefined λ> monoUpdate :: Y a -> a -> Y a; monoUpdate r a = r { y = a } λ> monoUpdate defaultY "c" *** Exception: Prelude.undefined CallStack (from HasCallStack): error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err undefined, called at <interactive>:2:44 in interactive:Ghci2 [ The construction of "defaultY { y = "c" }" begins with a construction of "defaultY" that may fail. ] Now imagine that some Monoid instances have "mempty = undefined", and others do not. Making the constructor strict, When the struct record is strict in the updated field, (e.g. with StrictData), the initial value is constructed strictly, even with optimisation. For example the below compiled with "ghc -O2" still throws an exception when executed: {-# LANGUAGE StrictData #-} module Main (main) where data Y a = Y { y :: a } deriving Show defaultY :: Monoid a => Y a; defaultY = Y undefined monoUpdate :: Y a -> a -> Y a; monoUpdate r a = r { y = a } main :: IO () main = print $ monoUpdate defaultY "c" Turning off "StrictData" makes it go. So I think there's even less room here for special logic. The type ambiguity must be resolved, allowing defaultY to be constructed. -- Viktor.