Misleading strictness annotations in Data.List.NonEmpty

[David Feuer]

The first one. Neither twiddles nor bangs are useful or add clarity.

On Fri, Jan 8, 2021, 11:53 AM Keith <keith.wygant at gmail.com> wrote:

> 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
> <john.ericson at obsidian.systems> 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 <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
>>>
>>
>> _______________________________________________
>> Libraries mailing listLibraries at haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
> 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/20210108/e4d90647/attachment.html>