Misleading strictness annotations in Data.List.NonEmpty

Currently: head ~(a :| _) = a tail ~(_ :| as) = as But head and tail are both strict. At best the '~'s have no effect. Should I open a PR to change it to head (a :| _) = a tail (_ :| as) = as or maybe even more clearly head !(a :l _) = a tail !(_ :| as) = as ? --Keith Sent from my phone with K-9 Mail. On January 4, 2021 2:40:58 PM UTC, John Ericson wrote:

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 mailto:rae@richarde.dev> wrote:

...

On Jan 3, 2021, at 1:02 PM, Carter Schonwald mailto:carter.schonwald@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries