can/should Functor have a quantified coercible constraint?

[Carter Schonwald]

Thx for  the link.  I’ll take a look at your suggested reading.

What are ways I could help progress whatever’s needed to get to a nice
ending?

On Mon, Jan 4, 2021 at 9:00 AM Richard Eisenberg <rae at richarde.dev> wrote:

>
>
> On Jan 3, 2021, at 1:02 PM, Carter Schonwald <carter.schonwald at gmail.com>
> wrote:
>
> This limitation is a misfeature, how can we make this get addressed sooner
> rather than later? Is this somewhere where Eg Haskell foundation or
> something could help?
>
>
> Lifting the limitation would be nice, but it's a lot of work. First, we
> need an updated theory for Core, with a type safety proof. This proof is
> essential: it's what our safety as a language depends on. Then, we'd need
> to implement it. I'm more worried about the former than the latter.
>
> > i think its worth emphasizing that ghc today uses a simplification of
> the original 2011 paper...
>
> Yes, that was originally true, but the current formulation goes beyond the
> 2011 paper in some respects. See section 7.1 of
> https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf.
>
> Roman writes:
>
> > I think it's important we keep the definitions of Functor and other
> fundamental classes understandable by newcomers, and this change would
> make the definition look scary for a marginal benefit.
>
> This is tough. I've considered a Functor definition like the one Carter
> proposes before. I would personally rather come up with the best definition
> first, then figure out how to make it palatable to newcomers second. For
> example, we could write (today)
>
> > type Representational f = forall a b. Coercible a b => Coercible (f a)
> (f b)
>
> and then the class constraint looks more pleasant. Or we could create ways
> of suppressing confusing information. Or there are other solutions.
> Depending on the benefit of the change (here or elsewhere), I would
> advocate holding off on making the change until we can support it without
> disrupting the newcomer story. But I wouldn't want to abandon the idea of
> an improvement a priori just because of a disruption to the newcomer
> experience.
>
> Richard
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210104/82e8f08d/attachment.html>