Add setField to HasField
This ticket is to track the implementation of https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-record-set-field.rst as modified by https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0583-hasfield-redesign.rst.
HasField
constraints are solved.
Review: how Have a look at Note [HasField instances]
in GHC.Tc.Instance.Class.
First, suppose that we have a data type decl:
data T a b = MkT { wombat :: ty }
So (even with DuplicateRecordFields) there is a record selctor
$sel_T_wombat :: forall a b. T a b -> ty
This is generated in GHC.Tc.TyCl.Utils, once and for all at T's definition site.
mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)]
Notice that this generates LHsBind GhcRn
code, which is then typechecked.
Now suppose that somewhere, far away from T's definitiion (in a module importing T's definition, say),
we use dot-notation r.wombat
. That generates a Wanted constraint:
[W] d :: HasField "wombat" rec_ty fld_ty
Then Note [HasField instances]
describes how we solve such constraints, on the fly.
We solve it like this:
d := $sel_T_wombat @alpha @beta |> (co1 ; co2)
where we have instantiated the record selector with fresh unification variables alpha
and beta
,
and (assuming ty' = ty{alpha/a, beta/b}
co1 :: (HasField "wombat" (T alpha beta) ty') ~# (T alpha beta -> ty')
co2 :: (T alpha beta -> ty') ~# (rec_ty -> fld_ty)
Here co1
is the newytpe axiom for the HasField
class and co2
is gotten sipmly
by emitting a new Wanted constraint for it.
All this is done by matchHasField
.
SetField
constraints
How to solve OK, what about SetField
constraints?
type SetField :: forall {k} {r_rep} {a_rep} . k -> TYPE r_rep -> TYPE a_rep -> Constraint
class SetField x r a | x r -> a where
modifyField :: (a -> a) -> r -> r
setField :: a -> r -> r
Remember from the class decle we already get a data type like this
type SetField :: forall {k} {r_rep} {a_rep} . k -> TYPE r_rep -> TYPE a_rep -> Constraint
data SetFeld x r a = C:SetField { modifyField :: (a->a) -> r -> r
, setField :: a -> r -> r }
Moreover, when we have a data type decl
data T a b = MkT { wombat :: ty }
we will need to generate (presumably also in mkRecSelBinds
):
$modify_T_wombat :: forall a b. (ty->ty) -> T a b -> T a b
$set_T_wombat :: forall a b. ty -> T a b -> T a b
Hmm. Maybe we should actually generate (again one and for all, at T's defn)
$fSetField_T_wombat :: forall a b. SetField "wombat" (T a b) ty
$fSetField_T_wombat = /\a b. C:SetField ($modify_T_wombat @a @b) ($set_T_wombat @a @b)
Now we have [W] d :: SetField x r a
we want to generate something like:
d := $fSetField_T_wombat @alpha @beta |> co
where co :: (SetField "wombat" alpha beta) ~ (SetField "wombat" rec_ty fld_ty)
and again we solve co
by emitting a new Wanted.
Not so hard.
Summary
- Enhance
mkRecSelBinds
to emit these$fSetField_T_wombat
definitions. - Add a new
matchSetField
function inGHC.Tc.Instance.Class
which operates rather likeHasField
.
Some old notes, retained for completeness
I've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for HasField
be generated?
To recap, recall that at present, HasField x r a
is coercible to r -> a
so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.
With the proposal, HasField x r a
will instead be represented as r -> (a -> r, a)
where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type data T = MkT { foo :: Int, bar :: Bool }
we need to generate
\ r x -> case r of MkT {foo = _, bar = bar} -> MkT { foo = x, bar = bar }
The most obvious approach is to generate well-typed Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a HasField
constraint is solved.
Would it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the type-checker. However, this would add some overhead for every field, even if HasField
was not subsequently used, and would require some naming scheme for update functions.
Or are there other options? Is there some way to solve a HasField
constraint and construct its dictionary by emitting renamed syntax for subsequent type-checking, such that subsequently solving similar constraints will use the same dictionary?
Trac metadata
Trac field | Value |
---|---|
Version | 8.7 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | NeilMitchell, simonpj |
Operating system | |
Architecture |