Re: GHC support for the new "record" package

On 22/01/15 21:07, Edward Kmett wrote:

On Thu, Jan 22, 2015 at 4:31 AM, Adam Gundry mailto:adam@well-typed.com> wrote:

Actually, the simplifications I recently came up with could allow us to make uses of the field work as van Laarhoven lenses, other lenses *and* selector functions. In practice, however, I suspect this might lead to somewhat confusing error messages, so it might not be desirable.

Interesting. Have you actually tried this with a composition of your simplified form, because I don't see how that can work.

When we tried this before we showed that there was a fundamental limitation in the way the functional dependencies had to flow information down the chain, also, "foo.bar.baz" has very different interpretations, between the lens and normal accessors, and both are producing functions, so its hard to see how this doesn't yield overlapping instance hell.

Apparently, composition works fine with both interpretations. Have a look here: https://github.com/adamgundry/records-prototype/blob/master/CoherentPrototyp... https://github.com/adamgundry/records-prototype/blob/master/CoherentPrototyp... The key idea is to define class IsRecordField (n :: Symbol) p where field :: proxy n -> p as the interpretation of fields, and notice that the two instances we want IsRecordField n (r -> t ) IsRecordField n ((a -> f b) -> (s -> f t) do not "morally" overlap, because in the first case r will always be a record datatype, and in the second case it is a function. Thus we can distinguish them using a closed type family. However, now that I look back, I notice that I'm using a suspicious functional dependency that doesn't look as if it should satisfy the liberal coverage condition, even though it is accepted by 7.8.3. So perhaps I'm too optimistic; and in any case, the types involved may be too confusing for use in practice. Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/