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