New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

record-set-field proposal #158

Merged
merged 5 commits into from Jan 22, 2019

Conversation

Projects
None yet
@ndmitchell
Copy link
Contributor

ndmitchell commented Aug 10, 2018

This is a proposal to add the function setField to the built-in typeclass
HasField, allowing type-based resolution of field names in record update functions.

Rendered

ndmitchell added some commits Aug 10, 2018

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Aug 10, 2018

@int-index

This comment has been minimized.

Copy link
Contributor

int-index commented Aug 10, 2018

A lens written directly can be more efficient than a lens written with get and set if element access is costly (e.g. in a Map). So I think the lens should be a part of the typeclass.

{-# MINIMAL getField, setField | fieldLens #-}
@int-index

This comment has been minimized.

Copy link
Contributor

int-index commented Aug 10, 2018

I also think that being able to set a field is a stronger condition (and not always needed) than being able to get it. Why not put it into a subclass?

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Aug 10, 2018

@int-index what type are you suggesting for fieldLens? If going into a different class then HasField is probably misnamed and should be GetField class. Being able to set a field is a different condition, not a stronger condition - you could imagine setField-only instances.

@adamgundry

This comment has been minimized.

Copy link
Contributor

adamgundry commented Aug 10, 2018

Thanks for writing this up @ndmitchell!

Perhaps GHC should simply provide separate HasField (aka GetField) and SetField classes, since those are the things that need to be solved by built-in magic? We could leave it up to (lens) libraries to offer a definition of fieldLens, possibly via another class and/or using HasField/SetField superclasses, since (a) it depends on the lens representation and (b) is only more efficient when you give a manual implementation rather than the HasField/SetField automatically-generated version.

@int-index

This comment has been minimized.

Copy link
Contributor

int-index commented Aug 10, 2018

what type are you suggesting for fieldLens?

type Lens' s a = forall f. Functor f => (a -> f a) -> (s -> f s)
fieldLens :: HasField lbl s a => Lens' s a

Being able to set a field is a different condition, not a stronger condition

I'm not sure. I expect setField to satisfy

getField @lbl (setField @lbl a s) = a

but there's no way to state that without getField, making const id a valid implementation of setField for any type.

We could leave it up to (lens) libraries to offer a definition of fieldLens, possibly via another class

I guess the problem with this is that HasLens becomes a stronger constraint than GetField + SetField. In a context where only GetField and SetField are available, there's incentive to forego adding an additional constraint and to use the (potentially inefficient) lens built from getField + setField.

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Aug 10, 2018

@int-index the idea here is to add the minimum stuff into GHC itself, in that sense it seems like two separate GetField and SetField classes is ideal. My guess is the Lens library would add a class:

class IsLens (lbl :: Symbol) r a | r -> a where
    myLens :: Lens' r a
    default myLens :: (GetField lbl r a, SetField lbl r a) => Lens' r a

But that's what Lens would add, and other libraries could feel free to go off in a different direction.

@adamgundry if we go for two classes, my preference would be to rename the first, since it's not heavily used yet, and the lack of symmetry is disturbing.

@winterland1989

This comment has been minimized.

Copy link

winterland1989 commented Aug 10, 2018

@ndmitchell What about adding both GetField and SetField as the superclass of HasField? i.e.

class GetField (x :: k) r a | x r -> a where
  getField :: r -> a

class SetField (x :: k) r a | x r -> a where
  setField :: a -> r -> r

class (GetField x r a, SetField x r a) => HasField x r a where
  -- simple van Laarhoven lens, e.g. view field @"foo" bar ...
  field :: Functor f => (a -> f a) -> (r -> f r)

I believe current code should continue to work if GetField is a superclass of new HasField.

@nomeata

This comment has been minimized.

Copy link
Contributor

nomeata commented Aug 10, 2018

This proposal does not affect record update syntax, right?

The OverloadedRecordFiels proposal describes how HasField constraints are magically solved. Shouldn't this be updated as well?

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Aug 10, 2018

@winterland1989 no, anyone defining custom HasField instances would break. But I think baking van Laarhoven lenses into GHC core libraries is the wrong thing to do - that's somewhere to leave for libraries to innovate. I don't see breaking HasField as a particularly big deal given how new it was, but if that's a hard constraint, we would just leave GetField named HasField.

@nomeata this proposal does not affect record update syntax. The way HasField constraints are magically solved does not change at all, just the dictionary they produce has an extra field. Therefore, no change. (If we go ahead with splitting the class into two I'll note that both pieces should have the magic solving behaviour.)

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Aug 10, 2018

Thanks for the comments - I've updated the proposal, primarily to split the type class in two, and capture some of the alternatives that were mentioned.

@ekmett

This comment has been minimized.

Copy link

ekmett commented Aug 11, 2018

Note: Back when @adamgundry was working on the original records proposal the idea we floated was to have a SetField class that could allow type changing. This handled everything needed to allow a proper type changing lens, but is slightly messier than the SetField you have here as it has an extra type parameter:

This yields

class SetField (x :: k) s t b | x s b -> t, x t -> b where
  setField :: b -> s -> t

which enables you to build

field :: (HasField x s a, SetField x s t b) => Lens s t a b

in full generality.

This leaves only the concerns about higher rank fields, and situations like data Foo a = Foo { bar, quux :: a } where foo { bar = baz, quux = quaffle } can do a type changing reassignment, while the lenses above can't be used for that, but there is a separate fix that could be concocted for that.

As an aside, I find the notion of a separate HasField offered above to be a bit of a mess, because it means you now have the tension between using the minimal requirements to get a lens SetField + GetField and using HasField which might offer you an ever so slightly more efficient lens, with no real good reason to select one or the other that is obvious to users.

@adamgundry

This comment has been minimized.

Copy link
Contributor

adamgundry commented Aug 12, 2018

On type-changing vs. non-type-changing SetField, I think this is a straightforward complexity trade-off. The type-changing version works, but it has various awkward corner cases (this page refers to an old design using type families, and I haven't worked through any differences caused by using functional dependencies instead, but the general issue holds). Thus I think there is an argument to simply offer the non-type-changing version, and suggest the use of other solutions for more complex updates.

situations like data Foo a = Foo { bar, quux :: a } where foo { bar = baz, quux = quaffle } can do a type changing reassignment, while the lenses above can't be used for that, but there is a separate fix that could be concocted for that.

@ekmett would you mind expanding on this "separate fix" a bit? The only workaround I'm aware of requires generalising the datatype e.g. to data Foo a1 a2 = Foo { bar :: a1, quux :: a2 }, and I don't see how to turn that into something GHC can reasonably do automatically.

As an aside, I find the notion of a separate HasField offered above to be a bit of a mess, because it means you now have the tension between using the minimal requirements to get a lens SetField + GetField and using HasField which might offer you an ever so slightly more efficient lens, with no real good reason to select one or the other that is obvious to users.

Well, at least lens (getField @"foo") (setField @"foo") is rather more long-winded than field @"foo", and it is fairly obvious that a lens is being constructed from a getter/setter pair rather than having the possibility of doing something more clever. Moreover, the latter can potentially be more efficient only when a user-supplied HasField instance creates a "virtual field" for a type, i.e. one that doesn't correspond to a field of a datatype, which is a comparatively unusual case.

@tejon

This comment has been minimized.

Copy link

tejon commented Aug 12, 2018

Moreover, the latter can potentially be more efficient only when a user-supplied HasField instance creates a "virtual field" for a type, i.e. one that doesn't correspond to a field of a datatype, which is a comparatively unusual case.

Unusual in current Haskell, but e.g. in C# it's a named feature with syntactic sugar ("properties"). It's already idiomatic to hide constructors and provide safe builder functions in Haskell. I think that if safe virtual-field lenses are currently rare, it might be more an issue of awareness and/or convenience than anything else. Providing a mechanism for them in base helps address both.

That being said, I completely understand the current hesitance to embrace lenses in base at all. That remains the strongest argument, IMO.

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Aug 13, 2018

@ekmett good points, and one that points towards a more complex solution, with a fair bit more alternatives to consider. My inclination is that it is better to go for something simple, which doesn't preclude adding more complex alternatives later, rather than to avoid adding anything because it could be generalised. It's quite possible a separate HasLens type class could be valuable, which more closely mirrored what lens required.

@tejon I appreciate the desire for virtualising fields, but that's somewhat orthogonal - this proposal and the existing getField are about making records available like they are today. As it stands today, they are hard to use, and this work is meant to make that easier. They also have problems with evolution, but we aren't aiming to solve those simultaneously.

@winterland1989

This comment has been minimized.

Copy link

winterland1989 commented Aug 14, 2018

@winterland1989 no, anyone defining custom HasField instances would break. But I think baking van Laarhoven lenses into GHC core libraries is the wrong thing to do - that's somewhere to leave for libraries to innovate. I don't see breaking HasField as a particularly big deal given how new it was, but if that's a hard constraint, we would just leave GetField named HasField.

I would argue that there're very few people defining custom HasField instances since it's intended to be a magic typeclass whose instances are provided by the compiler, at least it's much fewer than people actually using HasField class.

For baking van Laarhoven lenses, we shall bring a discussion on that but IIRC the community is leaning towards including it. e.g. http://r6.ca/blog/20120623T104901Z.html

Imagine this alternative history of Haskell. It is 1996, and the Haskell committee is about to introduce record syntax into Haskell 1.3. However, a (very) young Twan van Laarhoven joins the Haskell committee with fresh ideas. Instead of introducing field names as projection functions pi1 :: Pair a b -> a and pi2 :: Pair a b -> b, he pursuade them to give field names the following unusual definitions instead.

It's a pity not to include it given how simple and elegant the type is.

@AntC2

This comment has been minimized.

Copy link

AntC2 commented Aug 14, 2018

The function updateField can be recovered using setField and getField, but setField is simpler, so we prefer it.

I'm not sure that's the right choice: for a deeply-nested field, getField climbs down the structure to get the current value, brings it back so you can update it; then climbs down again to set. So the argument for making updateField the primitive is that it's more efficient. (And it's easy to define setField as updateField (const newValue).)

Is implementing only setField significantly "simpler" than implementing updateField?

BTW I agree with not binding Lenses into Haskell base. Contra @winterland1989, I imagine an alternative history of Haskell in which TRex became the record syntax. (They work well in Hugs, and knock spots of anything in GHC.) Or there were several ideas swirling around in 1996.

@danidiaz

This comment has been minimized.

Copy link

danidiaz commented Aug 14, 2018

@winterland1989 I would argue that there're very few people defining custom HasField instances since it's intended to be a magic typeclass whose instances are provided by the compiler, at least it's much fewer than people actually using HasField class.

I believe that one of the attractives of HasField-like typeclasses—beyond solving the field overloading issue—is incorporating field name information into the conventional typeclass machinery. I do plan to use custom HasField instances, for example to maintain backward compatibility when the internal fields change. They might also be useful in combination with -XDefaultSignatures and -XDerivingVia "if the record has a field named such-and-such with such-and-such-type, then I can define the following typeclass..."

@AntC2 BTW I agree with not binding Lenses into Haskell base. Contra @winterland1989, I imagine an alternative history of Haskell in which TRex became the record syntax.

I would argue that van Laarhoven lenses fit better with current Haskell, where Applicative and Traversable have become mainstays.

@int-index

This comment has been minimized.

Copy link
Contributor

int-index commented Aug 14, 2018

I would argue that van Laarhoven lenses fit better with current Haskell, where Applicative and Traversable have become mainstays.

Agreed. traverse is a van Laarhoven optic.

I'm not sure that's the right choice: for a deeply-nested field, getField climbs down the structure to get the current value, brings it back so you can update it; then climbs down again to set. So the argument for making updateField the primitive is that it's more efficient.

Well, following this line of reasoning, what if the update is effectful? That is, we need to climb down the structure to get the current value, apply a -> IO a to it, and get back an updated structure (in IO).

Then the primitive should be:

updateFieldIO :: HasField fld s a => (a -> IO a) -> (s -> IO s)

but of course, there's no reason to limit ourselves to IO, it can be any functor, thus

updateFieldF :: (HasField fld s a, Functor f) => (a -> f a) -> (s -> f s)

and that's a van Laarhoven lens. We can get updateField from it by assuming f ~ Identity.

@adamgundry

This comment has been minimized.

Copy link
Contributor

adamgundry commented Aug 15, 2018

@int-index that's a helpful line of reasoning, thanks.

I've been talking this over with some of my colleagues at Well-Typed (special thanks to @edsko and @bgamari), and have come round to the idea of using the van Laarhoven representation in the payload of a SetField constraint, i.e. something like this:

class HasField x r a => SetField (x :: k) r a | x r -> a where
  updateFieldF :: Functor f => (a -> f a) -> (r -> f r)

(modulo name bikeshedding, the question of whether to support type-changing update, and whether we want to make this part of HasField or separate),

The point is that the use of the van Laarhoven representation can be regarded as an implementation detail (albeit one that will be particularly convenient for users of the lens package). The expectation is that libraries offering lenses would write wrappers around updateFieldF to adapt them to their particular use case; in the case of lens this wrapper might be as simple as a change of name. This wouldn't really be base embracing van Laarhoven lenses, rather it would be exploiting them as a convenient implementation technique.

I still think the cases in which making use of this representation really gives an efficiency benefit will be comparatively rare, as they necessarily involve custom SetField instances. That said, it doesn't really hurt to provide the generality. The situation is somewhat analogous with the fact that the existing HasField class is polymorphic in the kind of labels k, even though GHC itself always uses Symbol, because some people want to give custom instances that are more general.

@simonpj

This comment has been minimized.

Copy link
Contributor

simonpj commented Aug 16, 2018

Having HasField as a superclass of SetField (rather than a more symmetrical arrangement) makes sense to me: it's hard to imagine being able to set a field without also being able to get it.

I defer to others on the type of set/update.

I agree that it's not worth adding a lot of complexity to support type-changing update. If the mono-typed version is simpler, let's do that.

Are you sure we want to use functional dependencies here? Its there a reason not to use type families? The latter gives you fewer type parameters, and generally more equality evidence is available.

@winterland1989

This comment has been minimized.

Copy link

winterland1989 commented Aug 16, 2018

I've been talking this over with some of my colleagues at Well-Typed (special thanks to @edsko and @bgamari), and have come round to the idea of using the van Laarhoven representation in the payload of a SetField constraint, i.e. something like this:

class HasField x r a => SetField (x :: k) r a | x r -> a where
 updateFieldF :: Functor f => (a -> f a) -> (r -> f r)

This is sweet !

@AntC2

This comment has been minimized.

Copy link

AntC2 commented Aug 18, 2018

@danidiaz, sorry I can't resist this pun

I would argue that van Laarhoven lenses fit better with current Haskell, ...

I think you're talking eyewash: no reason I can see why Lenses couldn't be defined over TRex style records. The library of optics would be 'OpTRex' ;-).

@Jashweii

This comment has been minimized.

Copy link

Jashweii commented Aug 20, 2018

For type-changing updates, what about combining multiple fields into a sub-record or tuple?

data FooBar a = FooBar { _foo :: a, _bar :: a }
foo, bar :: Lens (FooBar a) (FooBar a) a a
foo_and_bar :: Lens (FooBar a) (FooBar b) (a, a) (b, b)
-- x { foo = ... } -- uses foo
-- x { bar = ... } -- uses bar
-- x { foo = ..., bar = ... } -- uses foo_and_bar, possibly type-changing
foo = foo_and_bar._1
bar = foo_and_bar._2

Perhaps with some magic setFields class? This could have problems when combining compiler and user defined fields; it would be much more complicated to support.

Edit: I just found a section of a blogpost from 2012 suggesting this:

However it is not possible to compose the polymorphic van Laarhoven lenses field1 and field2 to do this. As consolation, it is possible to hand create a van Laarhoven lens to do the update.

It might be possible to create syntax that derives these complex lenses just in time from a sequence of field names.

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Sep 7, 2018

Trying to summarise back towards a conclusion. I think it's important to understand the motivation for these primitives - they are a way to make use Records that is wired into the compiler. They are not intended as an end user API, but something with which such an API can be built. Think C FFI calls, simple, direct, which are then wrapped with all the user richness people expect (likely in many different ways, including by the Lens library).

Q: Should we allow type changing lenses? No - this results in additional implementation complexity. Let's aim to get something through, rather than nothing, and a future dedicated soul can extend it.

Q: Should we have HasField as a supertype of SetField? My view is no - that makes it a nicer concept to use directly and state laws about, but those aren't necessary to wire into primitives. However, I'm flexible.

Q: Should we make it possible to define updates where the set/get pair can be more efficient? For actual records, it's unnecessary, since the operations are cheap anyway. But since we allow users to write HasField/SetField instances, there may be some non-trivial cost to finding a given key, which can be shared with setting it. I am on the fence.

Q: If we do make set/get more efficient, how should we do it? One way is to define it as a van Laarhoven lens. Another is to define:

class SetField (x :: k) r a | x r -> a where
  -- | Update function to set a field in the record.
  setField :: r -> (a, a -> r)

I prefer the simpler one, because of the simplicity.

If the operation is generalised to be a superset of HasField then it seems that making HasField a superclass or merging the new setField into HasField would be a reasonable thing to do. Is anyone aware of things where we expect fields to be get-only? And are they really fields in the sense the API imagines.

@Jashweii

This comment has been minimized.

Copy link

Jashweii commented Sep 9, 2018

@ndmitchell

Is anyone aware of things where we expect fields to be get-only? And are they really fields in the sense the API imagines.

My first thought was summaries (e.g. a list stored with its length or total*), but, on second thought, why it would matter that these are get-only fields and not just regular functions? I think this applies in general - what's the difference between a get-only field and a regular function? Namespacing**?
So I'd support HasField and SetField being one class, or at least that HasField should require SetField***. On a related note, if we choose to have van Laarhoven lenses, we should have functions for working with them - I think the most useful would be %~ and foldMapOf.

data LenList a = LenList { list :: [a], len :: Int }
-- invariant: len == length . list; len is O(1)

* with dependent or refinement types, this may be another aspect of type-changing update
** if someone wanted e.g. to pattern match LenList { len = n } ->, they could instead propose extending record pattern matching to arbitrary functions
*** regarding efficiency, we could have specialisable methods for update or lensy version with this

@adamgundry

This comment has been minimized.

Copy link
Contributor

adamgundry commented Sep 18, 2018

On a related note, if we choose to have van Laarhoven lenses, we should have functions for working with them - I think the most useful would be %~ and foldMapOf.

I disagree. The choice of representation is intended to be an internal implementation detail, so we should expose getField/setField from base and otherwise leave it up to libraries to package things up however they choose.

More generally, it would be good to make progress here. I'm relatively ambivalent as to the exact answers to @ndmitchell's questions, but let's try to reach some sort of consensus and submit this to the committee. Or at least we could clarify the options remaining, as we could then ask the committee to make a decision between them.

It seems to me that the main point of contention is whether a SetField dictionary should contain a set function (as currently specified in the proposal), or a lens (and if so, whether to use a van Laarhoven lens or a simpler lens representation). I've tried to summarise the options currently on the table, with their pros and cons:

  1. setField :: a -> r -> r
    • very simple
    • getting and setting are orthogonal
    • updates of virtual fields may need to deconstruct r twice
  2. getSetField :: r -> (a, a -> r)
    • relatively simple
    • allows virtual fields to deconstruct r only once
  3. updateFieldF :: forall f . Functor f => (a -> f a) -> r -> f r
    • more complex
    • comparatively heavyweight to generate, relies on optimizer doing more
    • allows virtual fields to deconstruct r only once
    • fits in with lens ecosystem
    • composes nicely

What have I missed?

@yav

This comment has been minimized.

Copy link
Contributor

yav commented Dec 22, 2018

@gridaphobe currently equality constraints have no run-time evidence associated with them. With your proposal this is not the case anymore (i.e., where would we get the HasField evidence from?). This seems like a big change that I don't think is justified by what we are discussing here. Is FieldType "x" r ~ a any better than HasField "x" r a?

It seems to me that the simplest way forward would be to leave the records as they are, and fix GHC to better support FDs (e.g., as in "Elaboration on Functional Dependencies"). This is almost equivalent to simply adding the equality superclass constraint manually, except now GHC knows that the type function used as evidence for the FD is "internal" to GHC, and so it shouldn't show up in errors or inferred types.

@int-index

This comment has been minimized.

Copy link
Contributor

int-index commented Dec 22, 2018

I like the 2-parameter design for its conceptual simplicity. However, there are two things to keep in mind.

1. Type-changing updates.

The current proposal is

class HasField x r a | x r -> a where
  hasField :: r -> (a -> r, a)

with type-changing updates, it would become

class HasField x r r' a a' | x r -> a, x r' -> a', x r a' -> r' where
  hasField :: r -> (a' -> r', a)

How would one go about encoding these (more complex) functional dependencies as type families?

2. Overlapping instances.

Type families also rule out overlapping/overlappable user-defined HasField instances. For example, these two could be useful:

instance {-# OVERLAPPABLE #-}
  TypeError (ShowType r :<>: Text "has no field named" :<>: Text x) =>
  HasField (x :: Symbol) r a

instance {-# OVERLAPPABLE #-}
  TypeError (ShowType r :<>: Text "has no field" :<>: ShowType x) =>
  HasField (x :: k) r a

Functional dependencies give us more flexibility in defining HasField instances. This is direct consequence of what @simonpj notes above:

a type family really is qualitatively more expressive because it is reflected in type-equality evidence whereas functional dependencies (at least as currently implemented) merely guide unification.

Indeed, functional dependencies merely guide unification, that's what makes overlappable/overlapping with fundeps possible. If fundeps produced type-equality evidence, we'd be in trouble, we could conjure up unsafeCoerce from incoherent (or overlapping+orphan) instances.

This decision boils down to the expressive power distribution that we want: more flexibility at definition site or type equality evidence at use sites.

@AntC2

This comment has been minimized.

Copy link

AntC2 commented Dec 23, 2018

IIRC, the reason for 3 parameters (whether FunDep or type family) was to more easily support in future syntactic sugar in record constraints. I think that's here at Syntactic sugar for Has. Perhaps @adamgundry could remind us what became of that thinking.

Desugarring that syntax to 2-parameter class/type functions would be OK. But ensugarring would need traversing the whole set of constraints and matching up possibly many HasFields and FieldTypes.

@AntC2

This comment has been minimized.

Copy link

AntC2 commented Dec 23, 2018

@simonpj muttering about functional dependencies

I see nothing that amounts to "muttering" in those messages (perhaps I'm more used to working with FunDep code than Simon chooses to). But it's only a message: if it's unclear or poorly phrased, it's easy to change; perhaps Simon would like to propose new wording? Perhaps if the message relates specifically to the HasField class, it could be customised?

@yav fix GHC to better support FDs

@simonpj functional dependencies (at least as currently implemented) merely ...

Indeed. It's GHC's current implementation of FunDeps that I see as the main difficulty here. There's a pile of tickets complaining about incoherence and surprises for newbies in GHC (nothing to do with any records proposal). Hugs has in general a stronger implementation -- Incoherent is not allowed; orphan instances can't happen. AFAICT GHC's implementation has received no attention since before 2006 -- in particular it ignores the theory in the FDs via CHRs paper. In @simonpj's own words, parts of GHC's behaviour are "bogus".

At Simon's request here I'm trying to keep track of the "pile"; and propose a way forward that would better integrate with overlapping, per @int-index.

I'm finding Simon's tone wrt FunDeps none too respectful of the many Haskellers who prefer FunDeps to Type Families (as is well documented), despite the weaknesses in current implementation. Of course under the hood I see the benefit of keeping the two aligned. Overlapping instances and the need to create HasField/FieldType instances on the fly are going to be problematic for TFs(?)

@simonpj

This comment has been minimized.

Copy link
Contributor

simonpj commented Dec 24, 2018

I apologise for that -- it was not my intent, and I will try to be more careful in the future.

I would be genuinely delighted to see functional dependencies better handled by GHC. But I think we lack a settled consensus on exactly how to do so. For example, Vladislav helpfully points out above that fundeps as a way to "guide unification", rather than as providing equality evidence, is a strength as well as a weakness. I don't know whether the consensus would be to continue with fundeps as guiding unification (this is what happens in Hugs, and GHC today) or to use them to encode type families (see the examples above, and the "Elaborating Functional Dependencies" paper) would be the best path.

Anthony makes a helpful start in comment:2 of Trac #15632. Turning that into a GHC proposal, and pushing it through to agreement, would be a good first step. Then someone might have the confidence to implement the agreed path.

@gridaphobe

This comment has been minimized.

Copy link
Contributor

gridaphobe commented Dec 24, 2018

@yav

currently equality constraints have no run-time evidence associated with them. With your proposal this is not the case anymore (i.e., where would we get the HasField evidence from?). This seems like a big change that I don't think is justified by what we are discussing here. Is FieldType "x" r ~ a any better than HasField "x" r a?

Good point!

Like @int-index, I like the two-parameter class for its conceptual simplicity. In particular, I like how it lets us talk independently about the existence of a field (HasField fld r) and the type of the field (FieldType fld r ~ a). In the three-parameter classes these two concepts are jumbled together.

That being said, it is nice that we can currently rely on equality constraints not incurring any runtime cost. I agree that we shouldn't throw that away without good reason, and this issue is probably not a good enough reason.

Of the three-parameter classes, I also prefer the one with fundeps. The three-parameter type family encoding feels quite awkward with the equality constraint in the instance head.

@danidiaz

This comment has been minimized.

Copy link

danidiaz commented Dec 25, 2018

If I wanted to use a record type as a sort of type-level map, to transform a type-level list of field names (that would be required to exist in the record) into a type-level list of field types, which approach would suit me best?

With the two-parameter typeclass it seems relatively easy to express constraints like "each of the symbols in this type-level list are field names in r". How would it work with the three-parameter typeclass, with or without fundeps?

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Dec 28, 2018

The proposal (and more importantly, the original HasField proposal that was previously accepted) allows both user defined instances, and also manufactures instances at use-time when required. My understanding (and I'm far from the expert here) is that because fun-deps only guide unification, and don't generate evidence, they can be part of overlapping type classes, so there is no required correctness check if a user defines a HasField instance.

However, if we used a type families, then we would have to check the user supplied instances in conjunction with the use-time generated instances, formed a coherent set. That either requires generating the instances upfront (a big change and one that violates the ability to hide fields) or modifying the type family correctness criteria (which sounds fiddly and dangerous). As a result, fun-deps are a much safer alternative. Is that correct @adamgundry ?

I don't know whether to ... continue with fundeps as guiding unification ... or to use them to encode type families

People have type families, and they're great. But many of the tricks people use complex type classes to pull of would be unsound with type families, because they overlap all over the place.

@adamgundry

This comment has been minimized.

Copy link
Contributor

adamgundry commented Dec 29, 2018

Am I right in understanding that the consensus is to stick with the fundeps version of HasField, for the time being? That doesn't preclude other more general improvements to fundeps or type families that might change things, but I don't think we should hold up this proposal on as-yet-unspecified future changes.

IIRC, the reason for 3 parameters (whether FunDep or type family) was to more easily support in future syntactic sugar in record constraints. I think that's here at Syntactic sugar for Has. Perhaps @adamgundry could remind us what became of that thinking.

That's an advantage of having three parameters, yes. The syntactic sugar fell by the wayside as not high enough priority to try to get through the proposals process, as the benefit is small and it would steal syntax that might be useful elsewhere.

The proposal (and more importantly, the original HasField proposal that was previously accepted) allows both user defined instances, and also manufactures instances at use-time when required. My understanding (and I'm far from the expert here) is that because fun-deps only guide unification, and don't generate evidence, they can be part of overlapping type classes, so there is no required correctness check if a user defines a HasField instance.

However, if we used a type families, then we would have to check the user supplied instances in conjunction with the use-time generated instances, formed a coherent set. That either requires generating the instances upfront (a big change and one that violates the ability to hide fields) or modifying the type family correctness criteria (which sounds fiddly and dangerous). As a result, fun-deps are a much safer alternative. Is that correct @adamgundry ?

Yes. We currently impose some restrictions on the HasField instances that can be defined (so the overlapping instances @int-index mentioned are forbidden). But that is "merely" to avoid fun-dep violations / incoherence. With type families, we'd need to impose suitable restrictions on FieldType instances or risk type soundness. As you imply, there is also the question of how to specify the reduction behaviour of FieldType: we solve HasField constraints only if the corresponding selector function is in scope, to provide for representation hiding, and we would probably want something similar for FieldType. So overall I'd rather not go for the FieldType approach unless we have compelling reasons for it.

@yav

This comment has been minimized.

Copy link
Contributor

yav commented Dec 29, 2018

@ndmitchell anything that FDs do that would be unsound with type families is just abusing the current GHC implementation of FDs. I would hope that the generated instances could in principle have evidence, even if we don't generate any right now. Otherwise, the design of the system is rather suspect, as we really have no good way to reason about the inferred types.

@AntC2

This comment has been minimized.

Copy link

AntC2 commented Dec 30, 2018

@yav anything that FDs do that would be unsound with type families ...

Again you seem to be 'bagging' FDs. AFAICT nobody's been able to produce unsoundness with FDs -- even with Overlapping/Incoherent instances, orphans, Undecidable. You do get strange behaviour/perplexing errors/programs that fail to compile/surprises. You don't get unsoundness as in a segfault (it at least needs unsafeCoerce for that). Or if you have an example, please add it to one of the (by now many) tickets.

The 'problem' seems to be that System FC does not provide a hook to hang appropriate evidence. Then

  • absence of evidence (in the System FC sense)

  • is not evidence of absence (of soundness).

Decent record-alike systems in Haskell have only been possible by using overlaps and FunDeps -- dating back to HList 2004. Then I don't think we should hobble this proposal because System FC is not fit for purpose.

is just abusing the current GHC implementation of FDs.

GHC's current implementation is nothing to be proud of; it's just plain wrong. I see nothing in the above comments that's trying to abuse it. Rather, they're using FDs in a well-disciplined way for which most (not all) of the principles were stated in 2006. And HList 2004 was a practical illustration.

@yav

This comment has been minimized.

Copy link
Contributor

yav commented Jan 2, 2019

@AntC2 I didn't mean to be "bagging" on fun-deps---I am quite a fan of them! The point I was trying to make is the "fun-deps" that violate the "functional" property are, well, not functional---just like type level functions, I would expect same inputs to imply same outputs. I agree that with GHC's current implementation the program will not seg-fault even if we didn't check fun-deps at all, however I don't think that's sufficient for good language design. In particular, relying on "fun-deps" that are not functional really has no specification, as far as I am aware. In short, we I think we might be in "violent agreement" here :)

Either way, we seem to have gone off into the weeds a little---I feel that this whole discussion is a bit orthogonal to the original concern that this proposal is meant to address. @simonpj, while it would be nice to combine all breaking changes into a single proposal, do you think we could proceed with the class as is, and leave the change to type-families for a separate proposal?

@ndmitchell

This comment has been minimized.

Copy link
Contributor Author

ndmitchell commented Jan 9, 2019

I suggest this proposal stay as it is, with functional dependencies, because:

  • @simonpj said he's fine with fundeps for now.
  • It's orthogonal to this proposal.
  • The change isn't as simple as it appears at first glance.

Assuming no objections in the next day or two, I'll ask the committee to consider this proposal.

@yav

This comment has been minimized.

Copy link
Contributor

yav commented Jan 9, 2019

@ndmitchell the proposal is already under committee consideration

@yav

This comment has been minimized.

Copy link
Contributor

yav commented Jan 22, 2019

OK, after some discussion the committee has decided to accept this proposal, and I've marked it as such.

@nomeata nomeata merged commit 7550848 into ghc-proposals:master Jan 22, 2019

nomeata added a commit that referenced this pull request Jan 22, 2019

@AntC2

This comment has been minimized.

Copy link

AntC2 commented Jan 23, 2019

Ah, I've been meaning to suggest adding a requirement from the discussion that doesn't appear in the written-up proposal.

Replying to @yav Steering committee discussion

I am also not sure why one would use overlapping things for records---wouldn't that imply that a record has the same field multiple times somehow?

No that's not the use case. (I agree there wouldn't be much sense in that.) @int-index's suggestion comment here is clear, I think. It's for improved error messages:

  • in record-accessing code, the most likely error is 'field not found in record'.
  • But you'll get a load of follow-on errors: couldn't determine field type/no instance Show for field type/couldn't determine type of expression that uses that field/etc.
  • If we only have a bare HasField/SetField constraint, the 'field not found' error message will be an unresolved overloading buried in a load of cruft. So the suggestion is to provide OVERLAPPABLE fall-back instances that will give more of a clue
   instance {-# OVERLAPPABLE #-}                           -- most likely the label is a Symbol
     TypeError (ShowType r :<>: Text "has no field named" :<>: Text x) =>
     HasField (x :: Symbol) r a

   instance {-# OVERLAPPABLE #-}
     TypeError (ShowType r :<>: Text "has no field" :<>: ShowType x) =>
     HasField (x :: k) r a

There might even be OVERLAPPABLE instances custom for non-appearing fields of specific record types.

@yav It would be extremely odd to accept a "functional" dependency that is not functional.

The resulting set of instances (i.e. with auto-gen'd most-specific HasField for each label that does appear in each record type) is "functional" in the same way these are "functional":

f (Just 'c') = "most overlapping"
f (Just  x ) = "middling"
f x          = "most overlappable"

But note those equations are only "functional" if they appear in exactly that order. Any other and GHC complains [-Woverlapping-patterns] Pattern match is redundant -- note the word 'overlapping'.

@yav supposed overlap provided by functional dependencies that would be unsound with type families.

You're not getting it: just because GHC/System FC can't generate evidence doesn't mean the program theory is unsound. (Goedel's theory, or something.)

@adamgundry

This comment has been minimized.

Copy link
Contributor

adamgundry commented Jan 29, 2019

@AntC2 I think the most direct way to achieve what you're after with the OVERLAPPABLE instances would be for GHC to detect unsolved HasField constraints and report them specially in its error-reporting logic. This shouldn't be difficult to arrange.

For the record, I've raised #16232 to track the implementation of this proposal.

judah added a commit to google/proto-lens that referenced this pull request Jan 31, 2019

Merge lens-labels into proto-lens.
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
wrapped/unwrapped labels.  After this change, we only
provided the "unwrapped" lenses (a la `lens`, `lens-family`, etc).

- `Lens.Labels` -> `Data.ProtoLens.Fields`
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`

Also rename `HasLens` to `HasField` to track the recent
GHC proposal:
(ghc-proposals/ghc-proposals#158
package

judah added a commit to google/proto-lens that referenced this pull request Jan 31, 2019

Merge lens-labels into proto-lens.
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
wrapped/unwrapped labels.  After this change, we only
provided the "unwrapped" lenses (a la `lens`, `lens-family`, etc).

- `Lens.Labels` -> `Data.ProtoLens.Fields`
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`

Also rename `HasLens` to `HasField` to track the recent
GHC proposal:
(ghc-proposals/ghc-proposals#158
package

judah added a commit to google/proto-lens that referenced this pull request Jan 31, 2019

Merge lens-labels into proto-lens.
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
regular lenses and the newtypes in `Lens.Labels` -- which, again,
aren't widely used.

- `Lens.Labels` -> `Data.ProtoLens.Fields`
    - Defines the `HasField` class.
    - Also defines a new `field` function that works with
      `TypeApplications`.
    - Removes the `LensFn` newtype and related functions.
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
    - Defines the orphan `IsLabel` instance.
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`
    - Defines prisms and related functions.

Also rename `HasLens` to `HasField` to track the recent
GHC proposal:
(ghc-proposals/ghc-proposals#158
package

judah added a commit to google/proto-lens that referenced this pull request Jan 31, 2019

Merge lens-labels into proto-lens.
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
regular lenses and the newtypes in `Lens.Labels` -- which, again,
aren't widely used.

- `Lens.Labels` -> `Data.ProtoLens.Fields`
    - Defines the `HasField` class.
    - Also defines a new `field` function that works with
      `TypeApplications`.
    - Removes the `LensFn` newtype and related functions.
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
    - Defines the orphan `IsLabel` instance.
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`
    - Defines prisms and related functions.

Also rename `HasLens` to `HasField` to track the recent GHC proposal:
(ghc-proposals/ghc-proposals#158

judah added a commit to google/proto-lens that referenced this pull request Jan 31, 2019

Merge lens-labels into proto-lens.
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
regular lenses and the newtypes in `Lens.Labels` -- which, again,
aren't widely used.

- `Lens.Labels` -> `Data.ProtoLens.Fields`
    - Defines the `HasField` class.
    - Also defines a new `field` function that works with
      `TypeApplications`.
    - Removes the `LensFn` newtype and related functions.
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
    - Defines the orphan `IsLabel` instance.
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`
    - Defines prisms and related functions.

Also rename `HasLens` to `HasField` to track the recent GHC proposal:
(ghc-proposals/ghc-proposals#158

Also bump proto-lens-protobuf-types to version 0.5 since it's
now more dependent on the new version of proto-lens.

judah added a commit to google/proto-lens that referenced this pull request Jan 31, 2019

Merge lens-labels into proto-lens.
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
regular lenses and the newtypes in `Lens.Labels` -- which, again,
aren't widely used.

- `Lens.Labels` -> `Data.ProtoLens.Fields`
    - Defines the `HasField` class.
    - Also defines a new `field` function that works with
      `TypeApplications`.
    - Removes the `LensFn` newtype and related functions.
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
    - Defines the orphan `IsLabel` instance.
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`
    - Defines prisms and related functions.

Also rename `HasLens` to `HasField` to track the recent GHC proposal:
(ghc-proposals/ghc-proposals#158

Also bump proto-lens-protobuf-types to version 0.5 since it's
now more dependent on the new version of proto-lens.

judah added a commit to google/proto-lens that referenced this pull request Feb 1, 2019

Merge lens-labels into proto-lens. (#309)
The separate "lens-labels" package hasn't been used outside of
proto-lens.  There's also a confusing distinction between
regular lenses and the newtypes in `Lens.Labels` -- which, again,
aren't widely used.

- `Lens.Labels` -> `Data.ProtoLens.Fields`
    - Defines the `HasField` class.
    - Also defines a new `field` function that works with
      `TypeApplications`.
    - Removes the `LensFn` newtype and related functions.
- `Lens.Labels.Unwrapped` -> `Data.ProtoLens.Labels`
    - Defines the orphan `IsLabel` instance.
- `Lens.Labels.Prism` -> `Data.ProtoLens.Prism`
    - Defines prisms and related functions.

Also rename `HasLens` to `HasField` to track the recent GHC proposal:
(ghc-proposals/ghc-proposals#158

Also bump proto-lens-protobuf-types to version 0.5 since it's
now more dependent on the new version of proto-lens.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment