CC @adamgundry

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 #-}

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?

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

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.

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.

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

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

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?

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

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.

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.

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.

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.

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

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.

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

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.

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

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.

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 !

@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' ;-).

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.

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.

@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

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?

So if you desire, you can make a new proposal, amending this (unimplemented one) that splits the classes.

Ok. I prefer this approach, but if it doesn't end up being implemented, then I'll try to improve the approach taken by this proposal and if all works out, I'll make another proposal.

So if you desire, you can make a new proposal, amending this (unimplemented one) that splits the classes.

#286

I wrote a blog post on various options regarding type-changing update, including a novel solution.

@effectfully Impressive, the circular trick is nice!

Also you should note that SameModulo approach forces to s and t to unify
(modulo a field). That is the right thing to do for lawful lenses.

So i think what you do, phrased as FunDep would be

class HasField name t s b a => HasField name s t a b | name s -> a, name t -> b where field :: Lens s t a b

And instances should only case on s:

instance (t ~ Proxy y, a ~ (), b ~ ()) => HasField "proxy" (Proxy x) t a b where field = lens (const ()) (\_ _ -> Proxy)
instance (t ~ (a', b), x ~ a, y ~ a') => HasField "_1" (a, b) t x y where field = _1

Prelude Optics Data.Proxy> :t set (field @"proxy") () (Proxy :: Proxy Int)
set (field @"proxy") () (Proxy :: Proxy Int)
  :: forall k2 (y :: k2). Proxy y

Prelude Optics Data.Proxy>  :t over (field @"_1" % field @"_1") length (("abc", True), 'd')
over (field @"_1" % field @"_1") length (("abc", True), 'd')
  :: ((Int, Bool), Char)

I didn't try the type-changing type-family update though.

When I tried to implement the polymorphic variant of this proposal, this is
what the simplest (IMO) source Haskell variant looked like ofwhat GHC could do
while solving for an instance.

When it sees hasField, it would

1. require that name argument is statically known.
2. check whether s parameter has known TyCon and proceed to step 4.
3. otherwise whether t parameter has known TyCon and proceed to step 4.
4. calculate all other types from known name and (s or t).
5. emit enough new wanted constraints so the produced field accessor is well-typed

This would avoid seemingly circular definition, as GHC is free to look at the structure of s and t and make a choice: luxury we cannot do in the source language.
But I hope that in the type-checker one could construct both of mutually recursive dictionaries, and avoid potential blow-up on a polymorpic recursion.

That's a direct extension of what is now done for current class HasField name r a where getField :: r -> a:

1. require that name argument is statically known.
2. require that r has known TyCon, say it's R.
3. take apply it to fresh variables to get R x y :: Type
4. calculate the type of name field for R x y, say it will be z.
5. Give a field selector R x y -> z casted to r -> a. Here r will unify with R x y (as x and y are fresh, and R is a TyCon of r), but z might not with a.

And some technicalities due to types with multiple constructors, for example.

To say it directly: TypeFamilies based approaches are much trickier to implement in the GHCs type-checker.

However, it's possible to get better inference with fun-deps. And it's quite simple one, a working example:

% ghci
GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
Loaded package environment from /home/phadej/.ghc/x86_64-linux-8.6.5/environments/default
Prelude> :set -XTemplateHaskell -XOverloadedLabels -XDataKinds -XFlexibleInstances -XFlexibleContexts -XMultiParamTypeClasses -XGADTs -XUndecidableInstances  
Prelude> import Optics
Prelude Optics> data User = User { userEmail :: String, userName :: String }
Prelude Optics> ; $(makeFieldLabels ''User)

Prelude Optics> over #email _ (User "john@gmail.com" "John")

<interactive>:5:13: error:
    • Found hole: _ :: [Char] -> [Char]
    • In the second argument of ‘over’, namely ‘_’

Prelude Optics> :t \f -> over #email f (User "john@gmail.com" "John")
\f -> over #email f (User "john@gmail.com" "John")
  :: ([Char] -> [Char]) -> User

Prelude Optics> :t over (_1 % _1) length (("abc", True), 'd')
over (_1 % _1) length (("abc", True), 'd') :: ((Int, Bool), Char)

See Structure of LabelOptic instances section in https://hackage.haskell.org/package/optics-core-0.2/docs/Optics-Label.html

The phantom arguments don't work though. I didn't try type-changing type-family update though.

@phadej that's a ton of helpful info, thank you. I'll reference your reply in the post.

So i think what you do, phrased as FunDep would be

class HasField name t s b a => HasField name s t a b | name s -> a, name t -> b where field :: Lens s t a b

And instances should only case on s:

Yeah, this does look equivalent as you're basically encoding the Get type family using fundeps. I kind of like type families more (they're first class unlike fundeps and we can share the same type family across different type classes, if we want to add HasPrism, etc), but it's no big deal and if fundeps are more suitable from the implementation perspective, then they should be chosen.

But I hope that in the type-checker one could construct both of mutually recursive dictionaries, and avoid potential blow-up on a polymorpic recursion.

I think it would be hard to make an instance with polymorphic recursion by accident? And does the blow up-mean that the compiler will just give up after a certain amount of attempts to resolve the constraints? If not, can we do a silly thing and add an additional n parameter that causes a TypeError when n is 0 and becomes n - 1 when instance resolution moves to the premise?

To say it directly: TypeFamilies based approaches are much trickier to implement in the GHCs type-checker.

Sorry, I don't get it. Why? The algorithms you outlined all seem to resolve s and t first (one of which has to be statically known) and name must be already known. Once you've resolved all of those, computing a and b is a matter of reducing a non-stuck type family. What am I missing?

However, it's possible to get better inference with fun-deps. And it's quite simple one, a working example:

That's impressive, but how did you manage to achieve that? Looking at

instance (a ~ String, b ~ String) => LabelOptic "name" A_Lens Human Human a b where
  labelOptic = lensVL $ \f s -> (\v -> s { humanName = v }) <$> f (humanName s)

I do not see how that can lead to working type inference. Could you please explain?

You've shown the bottom-up type inference. Does the top-down one also work? I.e. what I write as

-- Found type wildcard ‘_’ standing for ‘User’
test1 :: _ -> User
test1 user = user & lens @"name" .~ "new name"

in the post.

Prelude Optics> :t over (_1 % _1) length (("abc", True), 'd')
over (_1 % _1) length (("abc", True), 'd') :: ((Int, Bool), Char)

I've only provided this example to show that the new approach doesn't break here unexpectedly. They all seem to perform equally well in the polymorphic case.

I think it would be hard to make an instance with polymorphic recursion by accident?

In short: by accident is less strong than never.
We also have to be sure that GHC always ties the knot (and never diverges as it thinks we need UndecidableSuperClasses).

UndecidableInstances when user defines their instances is "fine", as it is
user themselves pointing the gun at their foot. But UndecidableSuperClasses
when defining the class itself is different, we should verify that user cannot
ever turn the gun barrel onto their foot, accidentally or not. If they really
want, they should turn off some safety features; library writes shouldn't do
that.

I don't know what GHC does, whether it gives up or loops. (Probably gives up, but that would be a bug IMO).

I do not see how that can lead to working type inference. Could you please explain?

That's explained in Structure of LabelOptic instances https://hackage.haskell.org/package/optics-core-0.2/docs/Optics-Label.html

By leaving a and b free in the instance definitions, they don't need to be known before the instance can match.

You've shown the bottom-up type inference. Does top-down also work? I.e. what I write as...

Looks like it works:

-- I tell only the result type:
*Main> :t \user -> set #name "new name" user :: User
\user -> set #name "new name" user :: User :: User -> User

Sorry, I don't get it. Why?

Maybe I'm wrong, I never tried to resolve type families equalities in the type-checker (plugins). If you can assert that indeed Get (R x y) ~ z, then things will work out. I don't know how that axiom will propagate (if it needs to).

they're first class unlike fundeps and we can share the same type family across different type classes, if we want to add HasPrism, etc

LabelOptic is also parametrised by OpticKind,

                   -- this one ---v                     v--- and it depends on name and s, e.g.
class LabelOptic (name :: Symbol) k s t a b | name s -> k a, name t -> k b, name s b -> t, name t a -> s where

This prohibits you from having field (Lens) and constructor (Prism) of the same name, but they are distinct anyway.
That restriction is a good thing, it "merges" namespaces, reducing potential confusion.

One class to rule them all.

The type family approach has a downside: user can define type instance Get, without also defining the SameModule instance. One can argue that Get should be in the type class (unrestricted open type families are code smell, aren't they?); and then your argument about reuse doesn't apply.
I'm not sure whether @goldfirere still thinks as in https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/:

A radical proposal

1. Remove unassociated open type families. They’re quite awkward anyway – either they should be closed and define some sort of concrete function, or they will need a class constraint nearby to be useful.

I don't think anything changed in that regard since 2015

I tried to (trivially) break undecidable instances, but obviously it doens't work.

class HasField (name :: Symbol) t s b a => HasField name s t a b
    | name s -> a
    , name t -> b
  where

-- identity
newtype Foo a = Foo a

instance (t ~ Foo (Maybe x), a ~ x, b ~ Maybe x) => HasField "foo" (Foo x) t a b where

errors with

Loop.hs:24:10: error:
    • Occurs check: cannot construct the infinite type:
        x ~ Maybe (Maybe x)

1. s = Foo x, t = Foo (Maybe x); flip
2. s = Foo (Maybe x), t = Foo (Maybe (Maybe x)) =/= Foo x

SameModule resist in the same way

instance (t ~ Foo (Maybe x)) => SameModulo "foo" (Foo x) t where

errors with

Loop.hs:31:10: error:
    • Occurs check: cannot construct the infinite type:
        x ~ Maybe (Maybe x)

I hope there's a simple argument that you cannot escape that loop,
I just don't see it now.

If it's unescapable, that's good :)

In fact, I have written type-classes which are specialised versions of:

class Convert a b | a -> b, b -> a where
    convertTo   :: a -> b
    convertFrom :: b -> a

But then I can rewrite them as

class Convert b a => Convert a b where
    convert :: a -> b

in cases where having one name for convert is better.
(strict/lazy vs. some kind of toggle would be tempting, but there having different names is better).

In short: by accident is less strong than never.
We also have to be sure that GHC always ties the knot (and never diverges as it thinks we need UndecidableSuperClasses).

UndecidableInstances when user defines their instances is "fine", as it is
user themselves pointing the gun at their foot. But UndecidableSuperClasses
when defining the class itself is different, we should verify that user cannot
ever turn the gun barrel onto their foot, accidentally or not. If they really
want, they should turn off some safety features; library writes shouldn't do
that.

Agreed.

By leaving a and b free in the instance definitions, they don't need to be known before the instance can match.

Yeah, I understand the trick and I use it pretty often. What I don't understand is how it helps in this case. So consider this example

*Main> :t \user -> set #name "new name" user :: User
\user -> set #name "new name" user :: User :: User -> User

Things that are known to the compiler:

name ~ "name"
t ~ User
b ~ String

None of these fundeps

name s -> k a
name t -> k b
name s b -> t
name t a -> s

allow to resolve a and s from the constraints above. It feels like somehow there is an additional sneaky constraint that either unifies a with b or s with t.

Ok, I'll play with that myself.

If you can assert that indeed Get (R x y) ~ z

By the time when you start unifying z with a, you already resolved everything in R x y by unifying it with r and so Get (R x y) can just compute, you shouldn't need to propagate the constraint.

But I have no idea how Haskell's type checker works, that's just my intuition developed while programming in Agda and writing unifiers.

Anyway, fundeps are fine, it's not very important here whether fundeps or type families are used.

One class to rule them all.

Nice.

unrestricted open type families are code smell, aren't they?

Maybe, but I had a lot of trouble with associated type families not computing because of unresolved constraints or whatever. Making those type families unrestricted often helped, so now I just use them by default.

I tried to (trivially) break undecidable instances, but obviously it doens't work.

Maybe is rigid, maybe having a type family in place of it would break everything. Or growing a kind instead of a type. I'll play with that also.

and so Get (R x y) can just compute, you shouldn't need to propagate the constraint.

You need to implement that computation in the type-checker, as the goal (of this proposal) is to automatically create required instance dictionaries / type family equations on the fly. In GHC type families are (to some approximation, my best understanding) a list of equations, and we'd need to populate that list. User defined type-families are finite (and usually small) list of equations, but e.g. (+) :: Nat -> Nat -> Nat is resolved by generating new equations as one need them on the fly. Thus e.g.

*Main> :kind! forall x. x + 0
forall x. x + 0 :: Nat
= x
*Main> :kind! forall x. 0 + x
forall x. 0 + x :: Nat
= x

work. As inside GHC we actually can backtrack, for example, but if we tried to do similar thing in source language:

type family Plus ... where
  Plus 0 x = x
  Plus x 0 = x

then that won't reduce in Plus x 0 case, as it would be stuck on x. Open type families are additionally required to be non-overlapping, so "if any matches, it's the one". (IIRC).

Continuing to HasLens, we can cheat there a lot too, e.g. define it only as:

class HasLens name s t a b where
    ...

without any fundeps, but resolve it in a way it had. I.e. create additional equality constraints to be satisfied. And we can (should!?) do the best possible thing, incl. possibly doing something which isn't really implementable in the source GHC Haskell, but still has definable algorithm (as my described, first look at s then at t, is a bit like + example). But we probably should have some fundeps / super-classes / type families / ..., so user defined instances would be useful too (and GHC's type-checker could do something by itself with them).

Note, we are talking about GHCs type checker. "Haskell" don't even have MPTCs :) I think that's

Okay, I think I know why inference works with fundeps. So we have the following fundeps:

x s -> a
x t -> b
x s b -> t
x t a -> s

but when we define an instance like

instance (a ~ String, b ~ String) => HasLens "name" User User a b where
    lensAt _ f (User email name) = User email <$> f name

these two fundeps:

x s b -> t
x t a -> s

essentially become

x s -> t
x t -> s

because the instance head says that the instance matches any a and b whatsoever and so nothing really depends on them and an attempt to define an additional instance like

instance (a ~ String, b ~ ()) => HasLens "name" User () a b where
    lensAt _ f (User email name) = f name

results in Functional dependencies conflict between instance declarations. I.e. we are able to infer that if a User is being updated, then the result is also a User.

I did not expect that! Should have checked before writing my post.

Ok, thanks a lot @phadej, I'll reflect in the post that the solution presented there is worse than the already known fundep solution.

For the record, LabelOptic is @arybczak creation; I'm just a messenger!

Hm, in fact yes, functional dependencies can't handle phantom types and type families unlike the SameModulo approach. None of these work (as the optics-core docs indicate):

data Ph (bs :: [Bool]) = Ph { foo :: Int }

instance (a ~ Int, b ~ Int) => HasLens "foo" (Ph bs) (Ph bs') a b where
    lensAt _ f (Ph i) = Ph <$> f i

type family Goo (a :: k)
data Tf (a :: k) = Tf { bar :: Goo a }

instance (a ~ Goo x, b ~ Goo x') => HasLens "foo" (Tf (x :: k)) (Tf (x' :: k')) a b where
    lensAt _ f (Tf x) = Tf <$> f x

Back to editing the post...

I updated the post reflecting the comments made by @phadej (thank you!).

Main things relevant to this discussion are:

• the SameModulo approach doesn't require UndecidableSuperClasses (and even UndecidableInstances, which are required by the fundeps approach to have decent type inference) as we can simply define the main class as

class SameModulo (x :: k) s t where
    lensAt :: (SameModulo x t s, a ~ Get x s, b ~ Get x t) => Proxy# x -> Lens s t a b

and everything will still work

• the fundeps approach doesn't work with phantom types and type families (in certain cases), but there is a simple workaround now described in the post:

data Ph (x :: k) (bs :: [Bool]) = Ph { foo :: Int }

instance (a ~ Tagged ('(,) x bs) Int, b ~ Tagged ('(,) x' bs') Int) =>
            HasLens "foo" (Ph (x :: k) bs) (Ph (x' :: k') bs') a b where
    lensAt _ f (Ph i) = Ph . unTagged <$> f (Tagged i)

ph :: Lens (Ph (a :: k) bs) (Ph (a' :: k') bs') Int Int
ph = lens @"foo" . coerced

• the fundeps approach gives rise to very satisfying type inference
• I'm still opposed to the monomorphic solution accepted by the committee, but less so now, because it can be directly extended to the one with functional dependencies
• I don't think that the new experimental solution is worth the trouble of adopting it right away. The functional dependencies one is battle-tested as it's used by many libraries and it does the job properly, so I think it's the one that should be implemented in GHC

I'm still opposed to the monomorphic solution accepted by the committee, but less so now, because it can be directly extended to the one with functional dependencies

Could you say a bit more about this? I'm not sure exactly what you mean. (I haven't been following very closely).

I'm still opposed to the monomorphic solution accepted by the committee, but less so now, because it can be directly extended to the one with functional dependencies

Could you say a bit more about this? I'm not sure exactly what you mean. (I haven't been following very closely).

Currently what is accepted is

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

This doesn't support type-changing update, e.g. you can write ("abc", True) & lens @"_1" .~ length (where lens is defined in terms of hasField), because length here maps String to Int, which is type-changing and thus is not allowed.

However making the class support type-changing update is only a matter of turning it into (which indeed can be done later, but I'm not sure why do it later, when you can just do it now)

class HasField x s t a b | x s -> a, x t -> b, x s b -> t, x t a -> s where
  hasField :: s -> (b -> t, a)

and I'm not aware of any disadvantages that this definition has over the monomorphic version.

I still think that the decision to accept the proposal was premature. @ekmett has a good argument in favor of separating HasLens into two classes. And there were other arguments and an entire separate proposal on that.

So when you say "it can be directly extended to the one with functional dependencies" by "it can be" you mean "it can be by breaking the currently accepted API", right?

So when you say "it can be directly extended to the one with functional dependencies" by "it can be" you mean "it can be by breaking the currently accepted API", right?

Yes (by breaking it either by unaccepting it or in a separate proposal).

I said it before, but it's worth repeating, The kind argument in LabelOptic makes it essentially into N different (indexed by kind) classes; which however share the namespace of "fields". So there you have full flexibility of offering only getters (or only setters) or full lens. It's only up to enumerating possible kinds.

@phadej

This prohibits you from having field (Lens) and constructor (Prism) of the same name, but they are distinct anyway.
That restriction is a good thing, it "merges" namespaces, reducing potential confusion.

I'm not fully convinced on this one.

One useful aspect of separating the namespaces is it allows for pass-through instances.

For example if you have some sort of generic sum type like Either a b or Variant r, then with separate namespaces you can automatically propagate instances for fields that all constructors share.

The dual of the above would be defining constructors for generic products if every member of the product shares that constructor. This seems unlikely to be particularly useful but it's worth mentioning.

I also think it would be rather confusing to not use separate namespaces in the case of newtypes. If I have newtype Identity a = Identity { unIdentity :: a }, then would I expect to have both Identity and unIdentity as fields/lenses? They would of course both be identical in behavior.

If I see:

#Just 5

foo.bar

I would not expect bar and Just to be looking in the same namespace personally.

But runIdentity and say mkIdentity (smart constructor) are in the same namespace!

-- technically both are Isos, but for an example sake they aren't

-- generated with makeFieldLabels
instance LabelOptic "runIdentity" A_Lens (Identity a) (Identity b) a b where
     labelOptic = ...

-- generated with makePrismLabels
instance LabelOptic "_Identity" A_Prism (Identity a) (Identity b) a b where
    labelOptic = ...

See also #270 (Note: #Just is invalid label, IIRC there was issue about that)

@phadej

Sure. But this is not confusing right now because they have very different types:

mkIdentity :: a -> Identity a
runIdentity :: Identity a -> a

In this case they would both have the exact same type.

This would mean I could do:

x = #runIdentity 5
y = x.mkIdentity

Which would be rather confusing.

And yeah I know #Just is an invalid label, but it seems like the proposal to fix it will probably be accepted.