can/should Functor have a quantified coercible constraint?

[John Ericson]

I talked to Carter a bit on IRC for my progress on that front, but I 
thought maybe this would be a good time to mention this more widely

- The constraint side is iffy. Local constraints and constraint kinds 
make it hard to have some sort of codata guardedness / cotermination 
checking argument for higher order coercion "instances" that doesn't 
also need to apply to the constraint system at large, which makes it 
quite laborious to increase expressive power without trade-offs like no 
local quantified constraints. (Yay mission creep.)

- The core side looks good. Cale and I pretty confident in the 
"coercions as fixed points of products", with {0, 1, multiplication, and 
exponentiation, limits} passing my cardinality sniff test that coercions 
still have no computational content and thus can be erased.

- Additionally, I am less but decently confident (though I haven't 
talked to Cale about this) that the existing role admissibility solver 
can be repurposed to produce those (to-be-erased) terms rather than just 
merely deciding the admissibility of (opaque) axiomatic coercions. This 
change would have no expressive power implications one way or the other, 
but complete the "theory refactor" so that the "sans-nth" version could 
be said to work end to end.

So tl;dr I /can't/ actually do anything to help Carter's problem at the 
moment, but I think I can get David's 
https://github.com/ghc-proposals/ghc-proposals/pull/276 over the finish 
line, with the side benefit of loosening things up and getting us closer 
so the higher-order roles problem seems less out of reach.

I have revised my "progress report" wildly since I started thinking 
about these things, but with the latest ratchet back, I think I finally 
have a stable prediction.

Cheers,

John

On 1/4/21 9:12 AM, Carter Schonwald wrote:
> 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 
> <mailto:rae at richarde.dev>> wrote:
>
>
>
>>     On Jan 3, 2021, at 1:02 PM, Carter Schonwald
>>     <carter.schonwald at gmail.com <mailto: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
>     <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
>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210104/d65a0027/attachment.html>