GHC support for the new "record" package

[Adam Gundry]

On 22/01/15 21:07, Edward Kmett wrote:
> On Thu, Jan 22, 2015 at 4:31 AM, Adam Gundry <adam at well-typed.com
> <mailto:adam at 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/CoherentPrototype.hs#L274-279
https://github.com/adamgundry/records-prototype/blob/master/CoherentPrototype.hs#L75-90

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/