Cannot update a field in a record with a polymorphic type.
Hello. I have a problem trying to do something very simple. Consider this conversation with GHC: λ data Y α = Y {y ∷ α} λ defaultY = Y {y = mempty} λ :type defaultY defaultY :: Monoid α => Y α λ :type defaultY {y = "c"} ∷ Y String <interactive>:1:1: error: • Ambiguous type variable ‘α0’ arising from a use of ‘defaultY’ prevents the constraint ‘(Monoid α0)’ from being solved. Probable fix: use a type annotation to specify what ‘α0’ 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 expression: defaultY In the expression: defaultY {y = "c"} :: Y String Why does this not work?
On Sun, 6 Sep 2020, Ignat Insarov wrote:
I have a problem trying to do something very simple.
Consider this conversation with GHC:
λ data Y α = Y {y ∷ α} λ defaultY = Y {y = mempty} λ :type defaultY defaultY :: Monoid α => Y α λ :type defaultY {y = "c"} ∷ Y String
<interactive>:1:1: error: • Ambiguous type variable ‘α0’ arising from a use of ‘defaultY’ prevents the constraint ‘(Monoid α0)’ from being solved. Probable fix: use a type annotation to specify what ‘α0’ 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 expression: defaultY In the expression: defaultY {y = "c"} :: Y String
Why does this not work?
I think it should work: :type (defaultY::Y [()]) {y = "c"} The problem is, that GHCi cannot infer the type of defaultY, because the update changes the type. By adding the type annotation Y String at the end, you only tell GHCi what it already knows, namely, that the result of the update has type Y String. But there is no way to infer what the type of 'mempty' must have been before the update.
On Sun, Sep 06, 2020 at 02:47:58PM +0500, Ignat Insarov wrote:
Consider this conversation with GHC:
λ data Y α = Y {y ∷ α} λ defaultY = Y {y = mempty} λ :type defaultY defaultY :: Monoid α => Y α λ :type defaultY {y = "c"} ∷ Y String
The mistake is to think that the expression: record { field = value } modifies *that* input record. But in fact, it should be clear that it produces a *new* record (Haskell values are immutable). If the record type is polymorphic: data Record a = Record { field :: a } deriving Show we can write: update :: Record a -> b -> Record b update record b = record { field = b } which produces an output whose type is different from the input. We thus observe: Prelude> data Record a = Record { field :: a } deriving Show Prelude> :{ Prelude| update :: Record a -> b -> Record b Prelude| update record b = record { field = b } Prelude| :} Prelude> let x = Record 1 Prelude> x Record {field = 1} Prelude> let y = update x "foo" Prelude> y Record {field = "foo"} This is why the type annotation on the output (easily inferred) is not sufficient, and it is the input "defaultY" that needs an explicit type. You can of course write a type-preserving setter: monoUpdate :: Record a -> a -> Record a monoUpdate record a = record { field = a} with monoUpdate, your example works: Prelude> let defaultR = Record mempty Prelude> :{ Prelude| monoUpdate :: Record a -> a -> Record a Prelude| monoUpdate record a = record { field = a} Prelude| :} Prelude> monoUpdate defaultR "c" Record {field = "c"} the type morphing behaviour of field update setters can admittedly be surprising at first encounter. -- Viktor.
Thank you Henning and Viktor. Indeed the update of the field goes through if its type is specified beforehand. But I am still not at peace. Consider: λ :type (defaultY ∷ ∀ α. Monoid α ⇒ Y α) {y = "c"} …Error… λ :type (defaultY ∷ Y ( )) {y = "c"} (defaultY ∷ Y ( )) {y = "c"} :: Y [Char] So, polymorphic types are not good enough to update. But see further: λ data Z α = Z {z₁, z₂ ∷ α} λ defaultZ = Z {z₁ = mempty, z₂ = mempty} λ :type (defaultZ ∷ ∀ α. Monoid α ⇒ Z α) {z₁ = "c"} (defaultZ ∷ ∀ α. Monoid α ⇒ Z α) {z₁ = "c"} :: Z [Char] — So when I have two fields it is suddenly fine to update a polymorphic field! I can infer that there is an invisible stage in the type checking process where all expressions must receive a final monomorphic type. I also understand that the surviving field `z₂` serves as a witness of the type `defaultZ` must have been specialized to: `"c" ∷ String` ⇒ `z₂ ∷ String` ⇒ `z₁ ∷ String`, and so type checking can succeed. But still, is this behaviour not obviously wrong? If a value of the transient instantiation of `defaultY` _(that exists only in the moment before its field is updated)_ is never observed, why does it need to be monomorphized? Why not be lazy about it?
On Sun, Sep 6, 2020, 7:24 AM Ignat Insarov
If a value of the transient instantiation of `defaultY` _(that exists only in the moment before its field is updated)_ is never observed, why does it need to be monomorphized? Why not be lazy about it?
You could just as well ask why ‘(== [])’ or ‘(== Nothing)’ require an ‘Eq’ constraint even though it will provably never be used. The reason, of course, is that the typechecker is only using purely local reasoning—yes, if you inlined that function far enough into any use site, it would lead to showing the ‘Eq’ redundant; and here, if you examined the update as a whole, you would find the type of the subterm is redundant as well. The same is true for typeclasses generally—instead of having bounded polymorphism, we could just substitute types and see what happens, like C++ templates do, but having the requirements stated in the type improves the predictability of whether something will typecheck, and improves the quality of error messages when it doesn’t. Basically, we accept that types will always be an *approximation* of terms. You can draw the line at different points—with refinement types, you can reason about the particular values or ranges of integers, for instance, instead of the coarse-grained ‘Int’. But all solutions that give you finer granularity also have tradeoffs in terms of ergonomics and predictability. Haskell has largely chosen to draw the line at “syntax-directed” as our criterion for how checking ought to work, assigning a type to every subterm in the same way, without context. This has turned out to be pretty usable in practice, even if there are some frustrating circumstances like this where you as a human can plainly *see* a fact that the typechecker cannot.
On Sun, 6 Sep 2020, Ignat Insarov wrote:
So, polymorphic types are not good enough to update. But see further:
λ data Z α = Z {z₁, z₂ ∷ α} λ defaultZ = Z {z₁ = mempty, z₂ = mempty} λ :type (defaultZ ∷ ∀ α. Monoid α ⇒ Z α) {z₁ = "c"} (defaultZ ∷ ∀ α. Monoid α ⇒ Z α) {z₁ = "c"} :: Z [Char]
— So when I have two fields it is suddenly fine to update a polymorphic field!
Z has only one type parameter. If you change the type of z1, you also change the type of z2. In your example with z1="c" you set the type of z1 to String, but you also claim that the result is consistently typed, thus z2 must also have type String. Since z2 was not touched, it must have the same type in defaultZ. Thus GHCi can infer the type parameter of defaultZ.
participants (4)
-
Henning Thielemann -
Ignat Insarov -
Jon Purdy -
Viktor Dukhovni