Cannot update a field in a record with a polymorphic type.

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
15 messages Options
Reply | Threaded
Open this post in threaded view
|

Cannot update a field in a record with a polymorphic type.

Ignat Insarov
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?
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Henning Thielemann

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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Viktor Dukhovni
In reply to this post by Ignat Insarov
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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Ignat Insarov
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?
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Jon Purdy
On Sun, Sep 6, 2020, 7:24 AM Ignat Insarov <[hidden email]> wrote:
 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.



_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Henning Thielemann
In reply to this post by Ignat Insarov

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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Olaf Klinke
In reply to this post by Ignat Insarov
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Richard Eisenberg-5
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 <[hidden email]> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Ignat Insarov
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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Tom Ellis-5
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
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Ignat Insarov
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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Tom Ellis-5
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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

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

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

That could be a surprising situation, there'd be things one could do
with the record update setters, that one could not do with Lens setters.

The work-around is to no define a type-preserving setter:

    monoUpdate :: Y a -> a -> Y a
    monoUpdate r a = r { y = a }

and use it to construct values of Y from a polymorphic seed.  One
might even note that:

    defaultY :: Monoid a => Y a
    defaultY = Y mempty

is a itself not a record, because it does not have a concrete type.  It
is a polymorphic nullary function that can produce a record, given a
context in which the desired type is apparent (can be inferred).
Therefore,

    defaultY { y = "c" }

is not an update of an existing input record, but rather it is an
(attempted) update of a new record, to be created there and then via a
call to the defaultY "factory".  But that call does not provide a
context to determine the type (and thus value) of defaultY.

Yes, we reason that it couldn't matter, but the compiler has limited
resources, and there's only so much inference that is compatible with
not slowing down compile times beyond their their current heft.  The
kind of inference needed to conclude that the type does not matter is
not built-in.

So, to me, needing to assign an explicit type in this corner case is
just an ordinary cost of doing functional programming (rooted in the
pure lambda calculus, where its functions all the way down).

I found it's initially somewhat unintuitive behaviour actually rather
educational.  Taking the time to understand it clarified some key
ideas.

--
    Viktor.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Cannot update a field in a record with a polymorphic type.

Viktor Dukhovni
In reply to this post by Tom Ellis-5
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.
_______________________________________________
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.