Misleading strictness annotations in Data.List.NonEmpty

Keith keith.wygant at gmail.com
Fri Jan 8 16:52:33 UTC 2021


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 
>> <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/20210108/2dc1cc62/attachment.html>


More information about the Libraries mailing list